user agent added

leanprover-community · Sep 16, 2024 · 89d324d · 89d324d
1 parent 4de5762
commit 89d324d
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -41,15 +41,15 @@ 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!
 
 def getMoogleQueryJson (s : String) (num_results : Nat := 6) : IO <| Array Json := do
   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}"