configurable useragent

LeanSearchClient/Basic.lean

@@ -14,3 +14,8 @@ register_option loogle.queries : Nat :=
   { defValue := 6
     group := "loogle"
     descr := "Number of results requested from loogle (default 6)" }
+
+register_option leansearchclient.useragent : String :=
+  { defValue := "LeanSearchClient"
+    group := "leansearchclient"
+    descr := "Username for leansearchclient" }

LeanSearchClient/LoogleSyntax.lean

@@ -50,11 +50,11 @@ inductive LoogleResult where
   deriving Inhabited, Repr
 
 def getLoogleQueryJson (s : String) (num_results : Nat := 6) :
-  IO <| LoogleResult:= do
+  CoreM <| LoogleResult:= do
   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", "--user-agent", "LeanSearchClient",  q]}
+  let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", "--user-agent", ← useragent,  q]}
   match Json.parse s.stdout with
   | Except.error e =>
     IO.throwServerError s!"Could not parse JSON from {s.stdout}; error: {e}"

LeanSearchClient/Syntax.lean

@@ -37,19 +37,22 @@ namespace LeanSearchClient
 
 open Lean Meta Elab Tactic Parser Term
 
-def getLeanSearchQueryJson (s : String) (num_results : Nat := 6) : IO <| Array Json := do
+def useragent : CoreM String :=
+  return leansearchclient.useragent.get (← getOptions)
+
+def getLeanSearchQueryJson (s : String) (num_results : Nat := 6) : CoreM <| Array Json := do
   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", "--user-agent", "LeanSearchClient", q]}
+  let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", "--user-agent", ← useragent, 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
+def getMoogleQueryJson (s : String) (num_results : Nat := 6) : CoreM <| 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",  "--user-agent", "LeanSearchClient", "--data", data.pretty]}
+  let s ← IO.Process.output {cmd := "curl", args := #[apiUrl, "-H", "content-type: application/json",  "--user-agent", ← useragent, "--data", data.pretty]}
   match Json.parse s.stdout with
   | Except.error e =>
     IO.throwServerError s!"Could not parse JSON from {s.stdout}; error: {e}"