Skip to content

Commit 89d324d

Browse files
user agent added
1 parent 4de5762 commit 89d324d

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

LeanSearchClient/LoogleSyntax.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ def getLoogleQueryJson (s : String) (num_results : Nat := 6) :
5454
let apiUrl := "https://loogle.lean-lang.org/json"
5555
let s' := System.Uri.escapeUri s
5656
let q := apiUrl ++ s!"?q={s'}"
57-
let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", q]}
57+
let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", "--user-agent", "LeanSearchClient", q]}
5858
match Json.parse s.stdout with
5959
| Except.error e =>
6060
IO.throwServerError s!"Could not parse JSON from {s.stdout}; error: {e}"

LeanSearchClient/Syntax.lean

+2-2
Original file line numberDiff line numberDiff line change
@@ -41,15 +41,15 @@ def getLeanSearchQueryJson (s : String) (num_results : Nat := 6) : IO <| Array J
4141
let apiUrl := "https://leansearch.net/api/search"
4242
let s' := System.Uri.escapeUri s
4343
let q := apiUrl ++ s!"?query={s'}&num_results={num_results}"
44-
let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", q]}
44+
let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", "--user-agent", "LeanSearchClient", q]}
4545
let js := Json.parse s.stdout |>.toOption |>.get!
4646
return js.getArr? |>.toOption |>.get!
4747

4848
def getMoogleQueryJson (s : String) (num_results : Nat := 6) : IO <| Array Json := do
4949
let apiUrl := "https://www.moogle.ai/api/search"
5050
let data := Json.arr
5151
#[Json.mkObj [("isFind", false), ("contents", s)]]
52-
let s ← IO.Process.output {cmd := "curl", args := #[apiUrl, "-H", "content-type: application/json", "--data", data.pretty]}
52+
let s ← IO.Process.output {cmd := "curl", args := #[apiUrl, "-H", "content-type: application/json", "--user-agent", "LeanSearchClient", "--data", data.pretty]}
5353
match Json.parse s.stdout with
5454
| Except.error e =>
5555
IO.throwServerError s!"Could not parse JSON from {s.stdout}; error: {e}"

0 commit comments

Comments
 (0)