From 89d324d94b50ca802643d46dd6cfe31070a990f4 Mon Sep 17 00:00:00 2001 From: Siddhartha Gadgil Date: Mon, 16 Sep 2024 18:25:26 +0530 Subject: [PATCH] user agent added --- LeanSearchClient/LoogleSyntax.lean | 2 +- LeanSearchClient/Syntax.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/LeanSearchClient/LoogleSyntax.lean b/LeanSearchClient/LoogleSyntax.lean index 1e5d2e2..00cefc3 100644 --- a/LeanSearchClient/LoogleSyntax.lean +++ b/LeanSearchClient/LoogleSyntax.lean @@ -54,7 +54,7 @@ def getLoogleQueryJson (s : String) (num_results : Nat := 6) : let apiUrl := "https://loogle.lean-lang.org/json" let s' := System.Uri.escapeUri s let q := apiUrl ++ s!"?q={s'}" - let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", q]} + let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", "--user-agent", "LeanSearchClient", q]} match Json.parse s.stdout with | Except.error e => IO.throwServerError s!"Could not parse JSON from {s.stdout}; error: {e}" diff --git a/LeanSearchClient/Syntax.lean b/LeanSearchClient/Syntax.lean index 49918e1..be0be41 100644 --- a/LeanSearchClient/Syntax.lean +++ b/LeanSearchClient/Syntax.lean @@ -41,7 +41,7 @@ def getLeanSearchQueryJson (s : String) (num_results : Nat := 6) : IO <| Array J let apiUrl := "https://leansearch.net/api/search" let s' := System.Uri.escapeUri s let q := apiUrl ++ s!"?query={s'}&num_results={num_results}" - let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", q]} + let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", "--user-agent", "LeanSearchClient", q]} let js := Json.parse s.stdout |>.toOption |>.get! return js.getArr? |>.toOption |>.get! @@ -49,7 +49,7 @@ def getMoogleQueryJson (s : String) (num_results : Nat := 6) : IO <| Array Json let apiUrl := "https://www.moogle.ai/api/search" let data := Json.arr #[Json.mkObj [("isFind", false), ("contents", s)]] - let s ← IO.Process.output {cmd := "curl", args := #[apiUrl, "-H", "content-type: application/json", "--data", data.pretty]} + let s ← IO.Process.output {cmd := "curl", args := #[apiUrl, "-H", "content-type: application/json", "--user-agent", "LeanSearchClient", "--data", data.pretty]} match Json.parse s.stdout with | Except.error e => IO.throwServerError s!"Could not parse JSON from {s.stdout}; error: {e}"