LeanSearch

Stream: general

[Jiang Jiedong]

This is the discussion thread of LeanSearch (https://leansearch.net/)
Looking forward to your feedback!

[Rida Hamadani]

I love the "Informal Statement" section of the search, it gave accurate statements for the few tests that I did. Thank you for making this!

[Rémy Degenne]

Suggestion: from the list of results, it took me a while to find how I could go interact with it. I finally found that the number in the left column is a link to the Mathlib docs, but that number is small and the link is not easy to notice.
Could the whole formal statement box be made into a link?

[Rida Hamadani]

This is the first inaccurate statement that I've found:
image.png

Here what is meant by the theorem is that a complete graph is regular of degree equal to the number of vertices minus one, which is pretty far from the informal statement.

Of course it is expected from a LLM to give some inaccurate statements, is there a place to submit feedback over such statements?

[Jason Rute]

The one thing I’m worried about projects like this, including Moogle.ai (which is great!), is that they have a tendency to fizzle out as the creators stop supporting them, so we get hooked and let down when they die. (Last I checked Moogle.ai hasn’t kept up with changes in Lean.). But I look forward to trying it!

[Jeremy Avigad]

I just tried it on a couple of things I was looking for last night: "the orbit stabilizer theorem" and "decompose List.range of a successor". The answers I got were excellent; the suggestions were all relevant and the things I wanted were at the top.

[Eric Wieser]

Just to check; this only searches theorems and not definitions?

[Jiang Jiedong]

Rémy Degenne said:

Could the whole formal statement box be made into a link?

Yes, that's a great UI suggestion! We will try to modify the link in the next version.

[Siddhartha Gadgil]

This is very nice. Thanks.

However, one thing that will improve its value to me is if it searches for definitions as well as theorems. For example, responses to "Remove an element from a list" do not include List.erase but only theorems about it.

[Jiang Jiedong]

Eric Wieser said:

Just to check; this only searches theorems and not definitions?

Ah yes for this version. Soon there will be a major update to include all definitions and instances. It's already on the schedule.

[Siddhartha Gadgil]

(deleted)

[Jiang Jiedong]

Rida Hamadani said:

is there a place to submit feedback over such statements?

I will discuss with the engineering team about this. It is valuable to collect human-corrected data, but it also requires some engineering work behind it.

[Luigi Massacci]

Jason Rute said:

The one thing I’m worried about projects like this, including Moogle.ai (which is great!), is that they have a tendency to fizzle out as the creators stop supporting them, so we get hooked and let down when they die. (Last I checked Moogle.ai hasn’t kept up with changes in Lean.). But I look forward to trying it!

Moogle is scheduled to update in a some weeks (I asked). However I agree that it’s nice to have a similar tool run by a university lab, as I imagine it might be more likely to last, or at the very least to be more easily handed off to someone else in the future if need be (though of course I wish the best of luck to everyone at Morph labs!)

[Luigi Massacci]

Also since there are more details available about the implementation it should be more easy to duplicate too if necessary

[Shreyas Srinivas]

In the long run we need open models with openly accessible APIs. Otherwise we are dependent on what the investors in a company like.

[Siddhartha Gadgil]

Another request: can we have an API for LeanSearch to use in other programs?

[Kim Morrison]

Siddhartha Gadgil said:

Another request: can we have an API for LeanSearch to use in other programs?

Marc has been thinking about how to get the results of Loogle and Moogle "closer to the code" via some support from the VSCode extension. Minimising the disruption / change of focus away from VSCode required to ask a question seems very important for making search tools useful.

[Jiang Jiedong]

We would be happy to make LeanSearch completely open-sourced after the paper is published.

[Jiang Jiedong]

@Siddhartha Gadgil @Kim Morrison
We are happy to provide the API; however, there are cost and safety concerns.

We are very excited about the possibility of integrating our search engine into VSCode extensions and would be very happy to provide the API for it. Additionally, for any research use, we would also be happy to provide our API. Please contact me if you wish to use it.

[Shreyas Srinivas]

I have been wondering about the extension itself becoming rather complicated. Does it make sense to split these vscode search tools into their own extensions and make an extension pack? So people can either install the lot in one go or pick and choose which extensions they want and in case of payment, which ones they wish to pay for.

[Siddhartha Gadgil]

Jiang Jiedong said:

Siddhartha Gadgil Kim Morrison
We are happy to provide the API; however, there are cost and safety concerns.

We are very excited about the possibility of integrating our search engine into VSCode extensions and would be very happy to provide the API for it. Additionally, for any research use, we would also be happy to provide our API. Please contact me if you wish to use it.

Thanks @Jiang Jiedong. I will contact you and ask for API access once I have a concrete use case (should be not too far in the future).

[Jiang Jiedong]

Shreyas Srinivas said:

So people can either install the lot in one go or pick and choose which extensions they want and in case of payment, which ones they wish to pay for.

We do not have enough people to make it into a separate VSCode extension...

[Shreyas Srinivas]

I believe it is not necessary for your team to do this as long as an API is on offer. The extension is merely a front end to your search engine. In principle it can be embedded in vscode even without extra effort on your part for an API, as a webview. This is essentially what the extension's Loogle view and moogle's extension offer anyway

[Daniel Weber]

I'm getting "Error: No API found". What could be the problem?

[Jason Rute]

I find the interface a bit hard to use on a phone. (I guess most people use laptops but I find myself on my phone a lot looking stuff up and chatting on here and PA.SX.) Also, it is strange you click on the number to go to mathlib’s docs. I think if you adopted an interface more like Moogle or the other search which came out yesterday, where you click on the theorem identifier it would be better.

[Jason Rute]

But, I really like the informal statement aspect. That is a big value add.

[Jason Rute]

Also, I wish this (or Moogle or the other new search engine or all three) would be added to mathlib’s #docs. (With Moogle you can just call it with a URL with the query in the URL like google. I don’t know how you would call this one right now.)

[Jiang Jiedong]

Daniel Weber said:

I'm getting "Error: No API found". What could be the problem?

Could you please more information? e.g. screenshots and information about your browser, ...

[Victor Liu]

Damn, I stumbled upon the paper on this a few days ago while looking up semantic search mathlib4 and I was wondering why I couldn't find the service, turns out it wasn't released yet :joy:
Thank you so much for this. As someone who is new to Lean and have a ton of trouble finding everything I need, this is a true lifesaver. I was trying to use frontier LLMs to find theorems in Lean but it seems like they are not sufficiently up to date on Mathlib4. However, this provides me exactly the tool I needed. :heart:

[Victor Liu]

Sometimes, I search many different queries in rapid succession, and would like to go back to the previous ones. It would be greatly appreciated if we could store previous few queries to be able to see them again. This could be adjusted in settings to reduce lag.

[Asei Inoue]

Lean Search is down? "503 Service Temporarily Unavailable" displayed.
https://leansearch.net/

[Asei Inoue]

@Jiang Jiedong

[Guoxiong Gao]

Asei Inoue said:

Lean Search is down? "503 Service Temporarily Unavailable" displayed.
https://leansearch.net/

Yes, the issue is on the server side. Due to server reallocation, we encountered a problem that has temporarily made the service unavailable. We are working to resolve this issue as quickly as possible. I will post an update in this channel once it is fixed. Thank you very much for pointing it out.

[Guoxiong Gao]

The issue has been fixed. If you encounter any further problems, please reach out to me or @Jiang Jiedong . We're happy to help!

[Tony Beta Lambda]

A suggestion: should we make the search case-insensitive? Searching for "Caylay-Hamilton" gives the expected results but a lower case "caylay-hamilton" will lead you to the wonderful world of modular forms.

[Yaël Dillies]

That wouldn't match the way the #docs work, namely lowercase matches lowercase and uppercase, uppercase matches anything

[Jiang Jiedong]

Tony Beta Lambda said:

A suggestion: should we make the search case-insensitive? Searching for "Caylay-Hamilton" gives the expected results but a lower case "caylay-hamilton" will lead you to the wonderful world of modular forms.

Hi, thank you for your suggestion! Currently, we use a large embedding model to turn a query into a semantic vector to find the most relevant theorems. So it depends on whether this embedding model thinks "Caylay-Hamilton" and "caylay-hamilton" are semantically near each other. Sometimes the upper-cased word does have a completely different meaning compared with the lower-cased one. I believe using the case that is common in mathematical literature gives the best result.

Maybe what we can do is a button that enables you to toggle on/off case sensitivity by turning all input into lower-case.

[Xiyu Zhai]

I'm a newbie. From a MLSYS point of view, I wonder what's the minimal computation that is needed to do search. Is it possible to have a small locally runnable implementation?

[Tony Beta Lambda]

Jiang Jiedong said:

I believe using the case that is common in mathematical literature gives the best result.

Maybe what we can do is a button that enables you to toggle on/off case sensitivity by turning all input into lower-case.

Agreed, although I can't seem to think of an example where differently cased words mean significantly different things in math :)

[Evgenia Karunus]

I believe the site is dead again on https://leansearch.net?

---

Update: reloaded in a few minutes and it worked for me, I think the service is intermittent.

[Evgenia Karunus]

Some theorem links give me 404 when I click on them, for example div_pos one.
I imagine that's because documentation updated, and there is no such theorem anymore.
Might it be sensible to link people to the github repo at a particular commit instead (the commit you gathered theorems from), if it's technically feasible?

image.png
image.png

[Jiang Jiedong]

Oh thank you for the feedback! This is a very good idea!

Evgenia Karunus said:

Might it be sensible to link people to the github repo at a particular commit instead (the commit you gathered theorems from), if it's technically feasible?

[Daniel Weber]

I don't think the website is versioned, but what about using the same mechanism as docs#div_pos (https://leanprover-community.github.io/mathlib4_docs/find/?pattern=div_pos#doc) ?

[Jiang Jiedong]

We are sorry the service is temporarily offline due to a major update. It will operate again once the update is finished. The update process should be finished in less than 24 hours if everything goes well.

[Guo Zixun]

Thanks for the suggestion, we will adopt it in this upgrade.

Daniel Weber said:

I don't think the website is versioned, but what about using the same mechanism as docs#div_pos (https://leanprover-community.github.io/mathlib4_docs/find/?pattern=div_pos#doc) ?

[Kim Morrison]

What is the suggested workflow if I would like to be using this / trying it out, but don't want to leave VSCode?

[Evgenia Karunus]

Congrats with the release, happy the json api works now!

Some thoughts about the new UI - in the old UI, I was able to read 5 or so theorems without scrolling after I click "search", now I see 1.5 theorems.
Also - I was able to read the description of the theorem without clicking on anything (without compromising cleanliness/compactness!).
And I liked being able to read the theorem name together with its type on the same line.
I also enjoyed the fact that you saw the rank & could click on it (though I understand from the comments above that some people didn't immediately see it as a link). It was clear what exactly is clickable in the interface and what is not.
I really enjoyed how clean/easy to read/concise the old interface was, maybe it's possible to integrate new functionality without compromising the compactness/simplicity of the old UI.

Mild nitpick - in theorem statements, we get empty spaces like this "∀ {f f' : ℝ → ℝ} {a b : ℝ}, ContinuousOn f (Icc a b) → (∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x) → ∀ {B B' : ℝ → ℝ}, f a ≤ B a → ContinuousOn B (Icc a b) → (∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x) → (∀ x ∈ Ico a b, f x = B x → f' x < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Icc a b → f x ≤ B x", maybe it makes sense to congeal multiple spaces into one space, or even into newlines.

[Filippo A. E. Nuccio]

The release is great, thanks! I have a minor comment on the name. The website is called `Mathlib 4 Search (according to the browser tab), the url says leansearch, the title of the page is "Lean Search" and the description begins with "Find theorems in Mathlib4...". Would it be possible to be more uniform (probably towards Mathlib)?

[Siddhartha Gadgil]

Evgenia Karunus said:

Congrats with the realease, happy the json api works now!

@Jiang Jiedong Where is the JSON API mentioned in the message documented?

[Jiang Jiedong]

Siddhartha Gadgil said:

Jiang Jiedong Where is the JSON API mentioned in the message documented?

You can find an example using the API of LeanSearch here.

[Jiang Jiedong]

Filippo A. E. Nuccio said:

Would it be possible to be more uniform (probably towards Mathlib)?

Thank you! We will probably make it more consistent in the next update. But I am quite fond of the name LeanSearch. :octopus:

I remember that there is another search tool called "search-mathlib". So we will probably try to avoid creating any confusion.

[Jiang Jiedong]

Kim Morrison said:

What is the suggested workflow if I would like to be using this / trying it out, but don't want to leave VSCode?

Maybe a potential solution is to make it into a vscode extension. Or like loogle, integrated as a part of the Lean vscode extension.

I believe it would be fantastic if we could have such a vscode extension. However, we don't have enough personnel to work on this project...

[Siddhartha Gadgil]

Jiang Jiedong said:

Siddhartha Gadgil said:

Jiang Jiedong Where is the JSON API mentioned in the message documented?

You can find an example using the API of LeanSearch here.

Thanks. I am going to start using this immediately.

[Siddhartha Gadgil]

Jiang Jiedong said:

Kim Morrison said:

What is the suggested workflow if I would like to be using this / trying it out, but don't want to leave VSCode?

Maybe a potential solution is to make it into a vscode extension. Or like loogle, integrated as a part of the Lean vscode extension.

I believe it would be fantastic if we could have such a vscode extension. However, we don't have enough personnel to work on this project...

An option is to have a Lean command that gives these options in the InfoView calling the API (maybe with TryThese as an option).

I will be happy to implement this in a day or two.

[Xavier Généreux]

Thank you for the tool!
One question: With this query

Positive and Negative Inequality: A positive number is not equal to its negative counterpart, meaning that if a number is greater than zero, it cannot be equal to the same number multiplied by negative one.

I get suggested the following theorems:

Int.neg_ne_of_pos
∀ {a b : ℤ}, 0 < a → 0 < b → -a ≠ b

which does not seem to exist. Am I missing something?
image.png

[Kim Morrison]

This would be awesome. We should have #leansearch, #moogle, etc.

[Siddhartha Gadgil]

@Jiang Jiedong @Kim Morrison I have made a first implementation for feedback and format.

The current interface gives a command with a "TryThis" widget that allows one to replace the command with a "#check" statement. To avoid repeatedly calling, the API is called only when the input ends with a "." or "?". The following is an illustration:

leansearch.gif

The code is at https://github.com/siddhartha-gadgil/MetaExamples/blob/main/MetaExamples/LeanSearch.lean. It is a very small amount of code so can just be pasted where needed. It is included below

import Lean
import Cache.IO
import Mathlib
open Lean Meta Elab Tactic Cache.IO

def getQueryJson (s: String)(num_results : Nat := 12) : IO <| Array Json := do
  let apiUrl := "https://leansearch.net/api/search"
  let s' := s.replace " " "%20"
  let q := apiUrl++ s!"?query={s'}&num_results={num_results}"
  let s ← runCurl #["-X", "GET", q]
  let js := Json.parse s |>.toOption |>.get!
  return js.getArr? |>.toOption |>.get!

def getCommandSuggestion (js: Json) : Option TryThis.Suggestion :=
  match js.getObjValAs? String "formal_name" with
  | Except.ok name =>
      let type? := js.getObjValAs? String "formal_type" |>.toOption
      let doc? := js.getObjValAs? String "docstring" |>.toOption
      let doc? := doc?.filter fun s => s != ""
      let docurl? := js.getObjValAs? String "doc_url" |>.toOption
      let docurl := (docurl?.map fun s => s!" (link: {s})").getD ""
      some {suggestion := s!"#check {name}", postInfo? := type?.map fun s => s!" -- {s}", preInfo? := doc?.map fun doc => s!"/- {doc}{docurl}-/\n"}
  | _ => none

def getQueryCommandSuggestions (s: String)(num_results : Nat := 6) :
  IO <| Array TryThis.Suggestion := do
    let jsArr ← getQueryJson s num_results
    return jsArr.filterMap getCommandSuggestion

open Command
syntax (name := lean_search_cmd) "#lean_search" str : command
@[command_elab lean_search_cmd] def leanSearchImpl : CommandElab :=
  fun stx => Command.liftTermElabM do
  match stx with
  | `(command| #lean_search $s) =>
    let s := s.getString
    if s.endsWith "." || s.endsWith "?" then
      let suggestions ← getQueryCommandSuggestions s
      TryThis.addSuggestions stx suggestions (header:= "Lean Search Results")
  | _ => throwUnsupportedSyntax

[Siddhartha Gadgil]

A non-lean question: the "gif" above is not animating in preview while ones I posted earlier did. Does anyone know why?

[Kim Morrison]

Suggestions:

• inline runCurl, so this could even be standalone from Mathlib
• Since "Try this:" can show arbitary html, how about a hyperlink with the link, rather than the link text?
• Space after the docurl?
• Maybe put the #check before the doc-string?
• Do we actually need quotes here? I wonder if we can tell the parser to just take anything up to the newline.
• The behaviour requiring "." or "?" is really confusing, and we need a better solution here. Debouncing? Print a warning if the string doesn't end that way?

[Kim Morrison]

(this is really great, looking forward to using it all the time!)

[Siddhartha Gadgil]

@Kim Morrison I have not inlined getCurl because I was worried about system independence (e.g. windows) and expected that cache has handled this. If you can suggest a robust way without Mathlib dependency I would be happy to do this.

I will work on the other suggestions. I did not know arbitrary HTML works in the widget (I guess that is logical as the Infoview is a browser).

[Kim Morrison]

Nope, Cache just assumes it is there.

[Siddhartha Gadgil]

I see. Then I too will assume this.

I also need help/references for the html link. Naively putting it as part of a string did not work. Is there something in which it should be enclosed?

[Johan Commelin]

I think the ProofWidget package provides a little DSL for building interactive things. I guess links are a very minimalistic form of interaction, but it might still be useful to pass through that API?

[Siddhartha Gadgil]

I implemented the easy suggestions. Here is a new animation:
leansearch-2.gif

Implemented:

• Warning if the sentence does not end with "." or "?"
• Documentation after #check
• Inlined curl

I do not know how to implement (but will continue searching):

• HTML links in TryThis.
• A parser that works without quotes up to end of the line.

For easy experimentation, here is the code to paste somewhere local (the webview will not handle curl).

import Lean
import Mathlib
open Lean Meta Elab Tactic

def getQueryJson (s: String)(num_results : Nat := 12) : IO <| Array Json := do
  let apiUrl := "https://leansearch.net/api/search"
  let s' := s.replace " " "%20"
  let q := apiUrl++ s!"?query={s'}&num_results={num_results}"
  let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", q]}
  let js := Json.parse s.stdout |>.toOption |>.get!
  return js.getArr? |>.toOption |>.get!

def getCommandSuggestion (js: Json) : Option TryThis.Suggestion :=
  match js.getObjValAs? String "formal_name" with
  | Except.ok name =>
      let type? := js.getObjValAs? String "formal_type" |>.toOption
      let doc? := js.getObjValAs? String "docstring" |>.toOption
      let doc := doc?.getD ""
      let docurl? := js.getObjValAs? String "doc_url" |>.toOption
      let docurl := (docurl?.map fun s => s!"[docs](s)").getD ""
      some {suggestion := s!"#check {name}", postInfo? := type?.map fun s => s!" -- {s}" ++ s!"\n/- {doc}{docurl}-/\n"}
  | _ => none

def getQueryCommandSuggestions (s: String)(num_results : Nat := 6) :
  IO <| Array TryThis.Suggestion := do
    let jsArr ← getQueryJson s num_results
    return jsArr.filterMap getCommandSuggestion

open Command
syntax (name := lean_search_cmd) "#lean_search" str : command
@[command_elab lean_search_cmd] def leanSearchImpl : CommandElab :=
  fun stx => Command.liftTermElabM do
  match stx with
  | `(command| #lean_search $s) =>
    let s := s.getString
    if s.endsWith "." || s.endsWith "?" then
      let suggestions ← getQueryCommandSuggestions s
      TryThis.addSuggestions stx suggestions (header:= "Lean Search Results")
    else
      logWarning "Lean search query should end with a full stop (period) or a question mark."
  | _ => throwUnsupportedSyntax

[Kim Morrison]

I'm not sure how cancelling of commands works, if at all. Perhaps an experiment is worthwhile to see if just adding a 200ms delay before calling curl suffices to avoid sending a request on every keystroke?

[Siddhartha Gadgil]

I will work on some Task based polling to avoid frequent calls. Every time the elaborator is called the call time is noted as well as the prompt. The query goes only if enough time has passed after the last call.

[Siddhartha Gadgil]

Siddhartha Gadgil said:

I will work on some Task based polling to avoid frequent calls. Every time the elaborator is called the call time is noted as well as the prompt. The query goes only if enough time has passed after the last call.

I retract this. Something has to trigger the elaborator to show stuff after it is computed in the background. It can be a change somewhere else but that will be fiddly. It will also go against trying to cache more to avoid re-evaluating.

For now, I feel having a clear warning to end with "." or "?" or some other terminator seems reasonably ergonomic and is easy.

[Patrick Massot]

About widgets showing arbitrary html: this is indeed nice, but please try to emit data in a structured way and then have the widget react code produce html. This way your widget can easily be implemented in other editors where the infoView is not a webpage.

[Siddhartha Gadgil]

As of now I have no idea how to have the widget emit arbitrary html (I tried simply as a string and nothing happened).

[Siddhartha Gadgil]

I will try to give the data in a more structured form.

[Siddhartha Gadgil]

image.png

The above is the modified view which I hope is more structured.

[Jiang Jiedong]

Xavier Généreux said:

Int.neg_ne_of_pos

That's probably because, in the latest version of Mathlib, this theorem has changed its name or has been removed.

[Kim Morrison]

Don't worry about the html, I guess. But @Patrick Massot's point is a good one: you should parse the JSON to a custom structure, and separately transform that structure to a TryThis.Suggestion, so that it is possible to consume it other ways.

[Siddhartha Gadgil]

I have refactored the code to separate the http query and extraction from JSON from generating and using the suggestion. Here is the new version.

import Lean
import Mathlib
open Lean Meta Elab Tactic Parser

def getQueryJson (s: String)(num_results : Nat := 12) : IO <| Array Json := do
  let apiUrl := "https://leansearch.net/api/search"
  let s' := s.replace " " "%20"
  let q := apiUrl++ s!"?query={s'}&num_results={num_results}"
  let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", q]}
  let js := Json.parse s.stdout |>.toOption |>.get!
  return js.getArr? |>.toOption |>.get!

structure SearchResult where
  name : String
  type? : Option String
  docString? : Option String
  doc_url? : Option String
  kind? : Option String

namespace SearchResult

def ofJson? (js: Json) : Option SearchResult :=
  match js.getObjValAs? String "formal_name" with
  | Except.ok name =>
      let type? := js.getObjValAs? String "formal_type" |>.toOption
      let doc? := js.getObjValAs? String "docstring" |>.toOption
      let doc? := doc?.filter fun s => s != ""
      let docurl? := js.getObjValAs? String "doc_url" |>.toOption
      let kind? := js.getObjValAs? String "kind" |>.toOption
      some {name := name, type? := type?, docString? := doc?, doc_url? := docurl?, kind? := kind?}
  | _ => none

def query (s: String)(num_results : Nat := 12) :
    IO <| Array SearchResult := do
  let jsArr ← getQueryJson s num_results
  return jsArr.filterMap ofJson?

def toCommandSuggestion (sr : SearchResult) : TryThis.Suggestion :=
  let data := match sr.docString? with
    | some doc => s!"· Description: {doc}\n"
    | none => ""
  let data := data ++ match sr.type? with
    | some type => s!"· Type: {type}\n"
    | none => ""
  let data := data ++ match sr.doc_url? with
    | some docurl => s!"· URL: {docurl}\n"
    | none => ""
  {suggestion := s!"#check {sr.name}", postInfo? := sr.type?.map fun s => s!" -- {s}" ++ s!"\n{data}"}

end SearchResult

def getQueryCommandSuggestions (s: String)(num_results : Nat := 12) :
  IO <| Array TryThis.Suggestion := do
    let searchResults ←  SearchResult.query s num_results
    return searchResults.map SearchResult.toCommandSuggestion

open Command
syntax (name := lean_search_cmd) "#lean_search" str : command
@[command_elab lean_search_cmd] def leanSearchImpl : CommandElab :=
  fun stx => Command.liftTermElabM do
  match stx with
  | `(command| #lean_search $s) =>
    let s := s.getString
    if s.endsWith "." || s.endsWith "?" then
      let suggestions ← getQueryCommandSuggestions s
      TryThis.addSuggestions stx suggestions (header:= "Lean Search Results")
    else
      logWarning "Lean search query should end with a full stop (period) or a question mark."
  | _ => throwUnsupportedSyntax

[Kim Morrison]

I suggest removing import Mathlib here, or at least making sure that it works after commenting it out.

[Siddhartha Gadgil]

I tested that. It works in one sense and not another:

• The code works fine to generate the TryMe etc and clicking replaces (so all new code is fine).
• But usually when we replace by #check ... the theorem is not in scope so gives an error.

So Mathlib is needed not for this code but at the user end.

[Kim Morrison]

The type is displayed twice, once as a -- on the #check line, then again as a bullet.

[Kim Morrison]

Suggest getting rid of the URL entirely. It's useless?

[Siddhartha Gadgil]

Yes. Both seemed reasonable places for the type.
If I get rid of the URL, then there is no need to have headers. Let me make the changes and post for comments.

[Kim Morrison]

How about we also make it parse as term? And "Try this:" just inserts the identifier.

[Kim Morrison]

It could also parse as a tactic and give three suggestions apply foo, have := foo and rw [foo].

[Siddhartha Gadgil]

Kim Morrison said:

How about we also make it parse as term? And "Try this:" just inserts the identifier.

I will make another elaborator to parse as a term. The one issue is that we have to return something from the elaborator before the TryMe is used to choose. It seems that sorry Prop is a reasonable fallback. More precisely, if the type is known then sorry type else sorry Prop.

[Siddhartha Gadgil]

I will also make the tactics version.

[Kim Morrison]

@Jiang Jiedong, could you remove all the .proof_n results? As far as I can see they are just noise.

[Siddhartha Gadgil]

Here is the info view cleaned up version of the command elaborator. Seems that this is enough info.
image.png

[Jiang Jiedong]

Kim Morrison said:

Jiang Jiedong, could you remove all the .proof_n results? As far as I can see they are just noise.

Thank you for your advice. We will definitely remove them in the next update.

[Kim Morrison]

Looks really nice! Just the right amount of info now.

[Kim Morrison]

So where do we put this? I think either a separate repo imported into Mathlib, or just Mathlib, work fine. I have a slight preference for a separate repo, to be honest.

(For slightly "meta" reasons. We need to get good at using separate repos, and if it's annoying at first, we will learn how to make it better.)

[Siddhartha Gadgil]

Separate repo sounds good.

I am now working on the term and tactic versions. Once they are done I will make the repo.

[Siddhartha Gadgil]

For terms here is the view of suggestions. I am also giving the type as a suggestion and the term with type given explicitly.
image.png

I added the other options because of misdiagnosing some low level errors (now fixed). I can remove them. I will anyway add configuration options so that they are not shown by default.

[Siddhartha Gadgil]

And the tactics infoview:
image.png

[Siddhartha Gadgil]

I modified the term suggestions a bit as it will be useful for the user to know the type. I will do the same for the tactics.
image.png

[Kim Morrison]

I think it's essential for both views that there is only one bullet symbol per result

[Kim Morrison]

otherwise it is impossible to interpret quickly

[Siddhartha Gadgil]

Sure.

[Kim Morrison]

I still don't understand why you are showing three different things per result for term mode.

[Siddhartha Gadgil]

There is only one bullet point per clickable result.

[Kim Morrison]

?

[Kim Morrison]

No, there is FrequentlyOdd, then its type, then the term with a type ascription.

[Kim Morrison]

That's three bullet points per result.

[Kim Morrison]

In term mode I think there should only be one clickable thing per search result.

[Siddhartha Gadgil]

I mean clicking on each bullet point gives a different results. Per search result there are three (just as there are 4 for tactics).

[Siddhartha Gadgil]

I do agree about the term mode.

[Siddhartha Gadgil]

I will switch back. I did this because of a low level error which I thought could be avoided by giving the type explicitly. But that was for a different reason.

[Kim Morrison]

For the tactic mode result it is essential that if we are given four alternatives that they are grouped together in some way

[Kim Morrison]

This is what I meant by "one bullet per result" (result meaning search result, not clickable action)

[Siddhartha Gadgil]

So here is the new version for terms.
image.png

[Siddhartha Gadgil]

To group tactics (which I agree should be done) I will have to look at the implementation of TryThis.addSuggestions.

[Siddhartha Gadgil]

There was a quick option. Does it seem okay to start with (till better widget code is written).

image.png

[Siddhartha Gadgil]

Actually addSuggestions is not much code. I will also work on a less hacky solution.

[Kim Morrison]

Somewhere out there there is a modification to this code that actually tries the tactics in the background and only reports the ones that worked. I forget who did this.

[Siddhartha Gadgil]

Kim Morrison said:

Somewhere out there there is a modification to this code that actually tries the tactics in the background and only reports the ones that worked. I forget who did this.

Will add this feature. I have done this sort of things a few times.

[Siddhartha Gadgil]

Indeed such a check is an example in the same repository where the lean_search code currently lives: https://github.com/siddhartha-gadgil/MetaExamples/blob/main/MetaExamples/CheckTactic.lean

[Siddhartha Gadgil]

The above actually checks if the goal is closed. I mean a mild modification of that.

[Julian Berman]

(Thank you for making this structured in a way we can use in Neovim land as well Siddhartha! I can confirm it already does something pretty reasonable:

Screenshot-2024-09-10-at-11.12.07.png

and whenever we have something we know we need anyhow I think I can make it look essentially the same as your VSCode screenshot.)

[Siddhartha Gadgil]

The filter seems to work though probably some cases are still wrong. Here is the view of suggested tactics in an example (I clicked many that passed the filter and they worked).
image.png

[Siddhartha Gadgil]

As my day gets over (in India), here is the code so far. Tomorrow I will put in a separate repository and try to make a few improvements.

import Lean
import Mathlib
open Lean Meta Elab Tactic Parser Term

def getQueryJson (s: String)(num_results : Nat := 12) : IO <| Array Json := do
  let apiUrl := "https://leansearch.net/api/search"
  let s' := s.replace " " "%20"
  let q := apiUrl++ s!"?query={s'}&num_results={num_results}"
  let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", q]}
  let js := Json.parse s.stdout |>.toOption |>.get!
  return js.getArr? |>.toOption |>.get!

structure SearchResult where
  name : String
  type? : Option String
  docString? : Option String
  doc_url? : Option String
  kind? : Option String

namespace SearchResult

def ofJson? (js: Json) : Option SearchResult :=
  match js.getObjValAs? String "formal_name" with
  | Except.ok name =>
      let type? := js.getObjValAs? String "formal_type" |>.toOption
      let doc? := js.getObjValAs? String "docstring" |>.toOption
      let doc? := doc?.filter fun s => s != ""
      let docurl? := js.getObjValAs? String "doc_url" |>.toOption
      let kind? := js.getObjValAs? String "kind" |>.toOption
      some {name := name, type? := type?, docString? := doc?, doc_url? := docurl?, kind? := kind?}
  | _ => none

def query (s: String)(num_results : Nat := 12) :
    IO <| Array SearchResult := do
  let jsArr ← getQueryJson s num_results
  return jsArr.filterMap ofJson?

def toCommandSuggestion (sr : SearchResult) : TryThis.Suggestion :=
  let data := match sr.docString? with
    | some doc => s!"{doc}\n"
    | none => ""
  {suggestion := s!"#check {sr.name}", postInfo? := sr.type?.map fun s => s!" -- {s}" ++ s!"\n{data}"}

def toTermSuggestion (sr: SearchResult) : TryThis.Suggestion :=
  match sr.type? with
  | some type => {suggestion := sr.name, postInfo? := some s!" (type: {type})"}
  | none => {suggestion := sr.name}

def toTacticSuggestions (sr: SearchResult) : Array TryThis.Suggestion :=
  match sr.type? with
  | some type => #[{suggestion := s!"apply {sr.name}"},
        {suggestion := s!"have : {type} := {sr.name}"},
        {suggestion := s!"rw [{sr.name}]"},
        {suggestion := s!"rw [← {sr.name}]" }]
  | none => #[]

end SearchResult

def getQueryCommandSuggestions (s: String)(num_results : Nat := 12) :
  IO <| Array TryThis.Suggestion := do
    let searchResults ←  SearchResult.query s num_results
    return searchResults.map SearchResult.toCommandSuggestion

def getQueryTermSuggestions (s: String)(num_results : Nat := 12) :
  IO <| Array TryThis.Suggestion := do
    let searchResults ←  SearchResult.query s num_results
    return searchResults.map SearchResult.toTermSuggestion

def getQueryTacticSuggestionGroups (s: String)(num_results : Nat := 12) :
  IO <| Array (String ×  Array TryThis.Suggestion) := do
    let searchResults ←  SearchResult.query s num_results
    return searchResults.map fun sr =>
      let fullName := match sr.type? with
        | some type => s!"{sr.name} (type: {type})"
        | none => sr.name
      (fullName, sr.toTacticSuggestions)

def defaultTerm (expectedType? : Option Expr) : MetaM Expr := do
  match expectedType? with
  | some type =>
    if !type.hasExprMVar then
      mkAppM ``sorryAx #[type, mkConst ``false]
    else
      return mkConst ``True.intro
  | none => return mkConst ``True.intro

def checkTactic (target: Expr)(tac: Syntax):
  TermElabM (Option Nat) :=
    withoutModifyingState do
    try
      let goal ← mkFreshExprMVar target
      let (goals, _) ←
        withoutErrToSorry do
        Elab.runTactic goal.mvarId! tac
          (← read) (← get)
      return some goals.length
    catch _ =>
      return none

open Command
syntax (name := lean_search_cmd) "#lean_search" str : command
@[command_elab lean_search_cmd] def leanSearchImpl : CommandElab :=
  fun stx => Command.liftTermElabM do
  match stx with
  | `(command| #lean_search $s) =>
    let s := s.getString
    if s.endsWith "." || s.endsWith "?" then
      let suggestions ← getQueryCommandSuggestions s
      TryThis.addSuggestions stx suggestions (header:= "Lean Search Results")
    else
      logWarning "Lean search query should end with a full stop (period) or a question mark."
  | _ => throwUnsupportedSyntax

syntax (name := lean_search_term) "lean_search#" str : term
@[term_elab lean_search_term] def leanSearchTermImpl : TermElab :=
  fun stx expectedType? => do
  match stx with
  | `(lean_search# $s) =>
    let s := s.getString
    if s.endsWith "." || s.endsWith "?" then
      let suggestions ← getQueryTermSuggestions s
      TryThis.addSuggestions stx suggestions (header:= "Lean Search Results")
    else
      logWarning "Lean search query should end with a full stop (period) or a question mark."
    defaultTerm expectedType?
  | _ => throwUnsupportedSyntax

syntax (name := lean_search_tactic) "lean_search?" str : tactic
@[tactic lean_search_tactic] def leanSearchTacticImpl : Tactic :=
  fun stx => withMainContext do
  match stx with
  | `(tactic|lean_search? $s) =>
    let s := s.getString
    if s.endsWith "." || s.endsWith "?" then
      let target ← getMainTarget
      let suggestionGroups ← getQueryTacticSuggestionGroups s
      for (name, sg) in suggestionGroups do
        let sg ←  sg.filterM fun s =>
          let sugTxt := s.suggestion
          match sugTxt with
          | .string s => do
            logInfo m!"Checking tactic: {s}"
            logInfo m!"Target: {← getMainTarget}"
            let stx? := runParserCategory (← getEnv) `tactic s
            match stx? with
            | Except.ok stx =>
              let n? ← checkTactic target stx
              return n?.isSome
            | Except.error e =>
              logInfo m!"Error: {e} while obtaining syntax tree"
              pure false
          | _ => pure false
        TryThis.addSuggestions stx sg (header:= s!"From: {name}")
    else
      logWarning "Lean search query should end with a full stop (period) or a question mark."
  | _ => throwUnsupportedSyntax

/-!
# Lean Search Examples

An example of using the leansearch API. The search is triggered when the sentence ends with a full stop (period) or a question mark.
-/

#lean_search "There are infinitely many odd numbers"

example := lean_search# "There are infinitely many odd numbers"

example : 3 ≤ 5 := by
  lean_search? "If a natural number n is less than m, then the successor of n is less than the successor of m"
  sorry

[Kim Morrison]

Suggestions:

• Just use #lean_search in all three positions. In each case it is transient, and about to disappear again. I appreciate this is not consonant with exact? and simp?, but the benefit is a user not having to learn (or distinguish) the punctuation required in different locations.
• Change lean_search to leansearch to match the URL?
• Can we add to the warning the text "Note this command sends your query to an external service at https://leansearch.net/." This both warns users about potential privacy / data use issues, and gives more visibility to the people providing the backend!
• Reduce the default number of results, perhaps?

[Kim Morrison]

Siddhartha Gadgil said:

Kim Morrison said:

Somewhere out there there is a modification to this code that actually tries the tactics in the background and only reports the ones that worked. I forget who did this.

Will add this feature. I have done this sort of things a few times.

Oops, my apologies for saying "I forget who did this" to the person who did this!!! :woman_facepalming:

[Siddhartha Gadgil]

@Kim Morrison Thanks for all the suggestions. I agree with them and have implemented them. I have also made the number of results configurable, but have a dummy for now so things can work in a single file, pasted below.

I will create a separate repository not dependent on Mathlib for this. Should I add you as a collaborator? To keep in sync with toolchain updates I assume someone from the FRO should have access.

import Lean
import Mathlib
-- import MetaExamples.Basic -- commented out for single file testing
open Lean Meta Elab Tactic Parser Term

def getQueryJson (s: String)(num_results : Nat := 6) : IO <| Array Json := do
  let apiUrl := "https://leansearch.net/api/search"
  let s' := s.replace " " "%20"
  let q := apiUrl++ s!"?query={s'}&num_results={num_results}"
  let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", q]}
  let js := Json.parse s.stdout |>.toOption |>.get!
  return js.getArr? |>.toOption |>.get!

structure SearchResult where
  name : String
  type? : Option String
  docString? : Option String
  doc_url? : Option String
  kind? : Option String

-- def queryNum : CoreM Nat := do
--   return leansearch.queries.get (← getOptions)

def queryNum : CoreM Nat := do -- fallback for single file testing
  return 6

namespace SearchResult


def ofJson? (js: Json) : Option SearchResult :=
  match js.getObjValAs? String "formal_name" with
  | Except.ok name =>
      let type? := js.getObjValAs? String "formal_type" |>.toOption
      let doc? := js.getObjValAs? String "docstring" |>.toOption
      let doc? := doc?.filter fun s => s != ""
      let docurl? := js.getObjValAs? String "doc_url" |>.toOption
      let kind? := js.getObjValAs? String "kind" |>.toOption
      some {name := name, type? := type?, docString? := doc?, doc_url? := docurl?, kind? := kind?}
  | _ => none

def query (s: String)(num_results : Nat) :
    IO <| Array SearchResult := do
  let jsArr ← getQueryJson s num_results
  return jsArr.filterMap ofJson?

def toCommandSuggestion (sr : SearchResult) : TryThis.Suggestion :=
  let data := match sr.docString? with
    | some doc => s!"{doc}\n"
    | none => ""
  {suggestion := s!"#check {sr.name}", postInfo? := sr.type?.map fun s => s!" -- {s}" ++ s!"\n{data}"}

def toTermSuggestion (sr: SearchResult) : TryThis.Suggestion :=
  match sr.type? with
  | some type => {suggestion := sr.name, postInfo? := some s!" (type: {type})"}
  | none => {suggestion := sr.name}

def toTacticSuggestions (sr: SearchResult) : Array TryThis.Suggestion :=
  match sr.type? with
  | some type => #[{suggestion := s!"apply {sr.name}"},
        {suggestion := s!"have : {type} := {sr.name}"},
        {suggestion := s!"rw [{sr.name}]"},
        {suggestion := s!"rw [← {sr.name}]" }]
  | none => #[]

end SearchResult

def getQueryCommandSuggestions (s: String)(num_results : Nat) :
  IO <| Array TryThis.Suggestion := do
    let searchResults ←  SearchResult.query s num_results
    return searchResults.map SearchResult.toCommandSuggestion

def getQueryTermSuggestions (s: String)(num_results : Nat) :
  IO <| Array TryThis.Suggestion := do
    let searchResults ←  SearchResult.query s num_results
    return searchResults.map SearchResult.toTermSuggestion

def getQueryTacticSuggestionGroups (s: String)(num_results : Nat) :
  IO <| Array (String ×  Array TryThis.Suggestion) := do
    let searchResults ←  SearchResult.query s num_results
    return searchResults.map fun sr =>
      let fullName := match sr.type? with
        | some type => s!"{sr.name} (type: {type})"
        | none => sr.name
      (fullName, sr.toTacticSuggestions)

def defaultTerm (expectedType? : Option Expr) : MetaM Expr := do
  match expectedType? with
  | some type =>
    if !type.hasExprMVar then
      mkAppM ``sorryAx #[type, mkConst ``false]
    else
      return mkConst ``True.intro
  | none => return mkConst ``True.intro

def checkTactic (target: Expr)(tac: Syntax):
  TermElabM (Option Nat) :=
    withoutModifyingState do
    try
      let goal ← mkFreshExprMVar target
      let (goals, _) ←
        withoutErrToSorry do
        Elab.runTactic goal.mvarId! tac
          (← read) (← get)
      return some goals.length
    catch _ =>
      return none

open Command
syntax (name := leansearch_cmd) "#leansearch" str : command
@[command_elab leansearch_cmd] def leanSearchImpl : CommandElab :=
  fun stx => Command.liftTermElabM do
  match stx with
  | `(command| #leansearch $s) =>
    let s := s.getString
    if s.endsWith "." || s.endsWith "?" then
      let suggestions ← getQueryCommandSuggestions s (← queryNum)
      TryThis.addSuggestions stx suggestions (header:= "Lean Search Results")
    else
      logWarning "Lean search query should end with a full stop (period) or a question mark. Note this command sends your query to an external service at https://leansearch.net/."
  | _ => throwUnsupportedSyntax

syntax (name := leansearch_term) "#leansearch" str : term
@[term_elab leansearch_term] def leanSearchTermImpl : TermElab :=
  fun stx expectedType? => do
  match stx with
  | `(#leansearch $s) =>
    let s := s.getString
    if s.endsWith "." || s.endsWith "?" then
      let suggestions ← getQueryTermSuggestions s (← queryNum)
      TryThis.addSuggestions stx suggestions (header:= "Lean Search Results")
    else
      logWarning "Lean search query should end with a full stop (period) or a question mark. Note this command sends your query to an external service at https://leansearch.net/."
    defaultTerm expectedType?
  | _ => throwUnsupportedSyntax

syntax (name := leansearch_tactic) "#leansearch" str : tactic
@[tactic leansearch_tactic] def leanSearchTacticImpl : Tactic :=
  fun stx => withMainContext do
  match stx with
  | `(tactic|#leansearch $s) =>
    let s := s.getString
    if s.endsWith "." || s.endsWith "?" then
      let target ← getMainTarget
      let suggestionGroups ←
          getQueryTacticSuggestionGroups s (← queryNum)
      for (name, sg) in suggestionGroups do
        let sg ←  sg.filterM fun s =>
          let sugTxt := s.suggestion
          match sugTxt with
          | .string s => do
            logInfo m!"Checking tactic: {s}"
            logInfo m!"Target: {← getMainTarget}"
            let stx? := runParserCategory (← getEnv) `tactic s
            match stx? with
            | Except.ok stx =>
              let n? ← checkTactic target stx
              return n?.isSome
            | Except.error e =>
              logInfo m!"Error: {e} while obtaining syntax tree"
              pure false
          | _ => pure false
        TryThis.addSuggestions stx sg (header:= s!"From: {name}")
    else
      logWarning "Lean search query should end with a full stop (period) or a question mark. Note this command sends your query to an external service at https://leansearch.net/."
  | _ => throwUnsupportedSyntax


/-!
# Lean Search Examples

An example of using the leansearch API. The search is triggered when the sentence ends with a full stop (period) or a question mark.
-/

#leansearch "There are infinitely many odd numbers"

example := #leansearch "There are infinitely many odd numbers"

example : 3 ≤ 5 := by
  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m"
  sorry

[Kim Morrison]

Exciting!

@Jesse Michael Han, I see that

curl 'https://www.moogle.ai/api/search' -H 'content-type: application/json'  --data-raw '[{"isFind":false,"contents":"infinitely many primes"}]'

works. Are we okay to send queries to that from an in-VSCode command?

If so, #moogle can hopefully use the same infrastructure.

[Kim Morrison]

Awesome, I love that the tactic suggestions are filtered by applicability!

[Jesse Michael Han]

yes! we are actually about to add support for it in a form factor similar to Loogle in the official VSCode extension as well

[Jesse Michael Han]

(updates to the search index and search quality coming soon too)

[Kim Morrison]

@Siddhartha Gadgil. There are still some stray logInfo.

[Siddhartha Gadgil]

Kim Morrison said:

Siddhartha Gadgil. There are still some stray logInfo.

Oops. I will clean up and also create the new repository.

[Kim Morrison]

I suggest the following order of operations:

• create a repo under your account
• add at least me with admin access
• make a PR to add this to Mathlib's imports
• discussion ensues...!
• assuming that we decide to proceed (I hope so), we can later migrate the repo to leanprover-community if that works for you.

[Siddhartha Gadgil]

Kim Morrison said:

I suggest the following order of operations:

• create a repo under your account
• add at least me with admin access
• make a PR to add this to Mathlib's imports
• discussion ensues...!
• assuming that we decide to proceed (I hope so), we can later migrate the repo to leanprover-community if that works for you.

Perfect.

[Siddhartha Gadgil]

@Kim Morrison

• I created a repository at https://github.com/siddhartha-gadgil/LeanSearchClient.git and invited you as a collaborator (I assume I can make you an admin only once you accept).
• I have made a pull request: https://github.com/leanprover-community/mathlib4/pull/16695

I am waiting CI but locally stuff is running fine.

[Kim Morrison]

(you linked to the PR twice, first link should be the repo)

[Kim Morrison]

I've initiated a discussion amongst the mathlib maintainers about the PR, specifically about allowing a new dependency. I think this one is quite low stakes, so hope that it will be okay.

[Siddhartha Gadgil]

I moved the examples file to test/ and now CI is giving the error:

Test failed: `lake env lean ./test/LeanSearchExamples.lean` produced:
Error: ./test/LeanSearchExamples.lean:6:0: error: unknown module prefix 'LeanSearchClient'

But things run file locally. This may be a CI configuration issue.

[Anand Rao Tadipatri]

leansearch_interactivecode_demo.png
I've opened a PR to display the suggestions as clickable and hoverable expressions in the infoview: https://github.com/siddhartha-gadgil/LeanSearchClient/pull/1.

[Anand Rao Tadipatri]

A potential downside is that only suggestions that elaborate within the current scope get displayed, and the rest get discarded.

[Siddhartha Gadgil]

@Anand Rao Tadipatri It looks very nice but adds to the complexity especially of dependencies. If Mathlib is to depend on LeanSearchClient which depends on ProofWidgets we can easily have version clashes.

It is not obvious to me that the extra info is that useful to a user. A user is looking for a theorem and should be able to see from the name and type whether the theorem is useful.

For now I will leave the PR pending and once the discussion for the simpler form takes off this can be discussed based on that conversation.

[Kim Morrison]

We're going to have to learn to deal with diamond dependencies one day, but I guess not today. :-)

[Kim Morrison]

Siddhartha Gadgil said:

I moved the examples file to test/ and now CI is giving the error:

Test failed: `lake env lean ./test/LeanSearchExamples.lean` produced:
Error: ./test/LeanSearchExamples.lean:6:0: error: unknown module prefix 'LeanSearchClient'

But things run file locally. This may be a CI configuration issue.

Could you push or PR something so I can look?

[Siddhartha Gadgil]

The same PR https://github.com/leanprover-community/mathlib4/pull/16695 is now broken and gives the error message I mentioned.

[Siddhartha Gadgil]

The previous commit on that was fine.

[Kim Morrison]

I'm cleaning up now.

[Kim Morrison]

Will push shortly

[Kim Morrison]

@Siddhartha Gadgil, https://github.com/siddhartha-gadgil/LeanSearchClient/pull/2

[Siddhartha Gadgil]

Thanks. I have merged the PR, updated the Mathlib PR to use the newer version and pushed.

[Kim Morrison]

Let's remove the test file in Mathlib, now that CI is running that same test upstream.

[Siddhartha Gadgil]

Sounds good. Will do so.

[Siddhartha Gadgil]

I have removed and pushed. Hope CI runs fine now.

[Kim Morrison]

Okay, we should work out where this should be imported.

[Kim Morrison]

Let's add this in Mathlib.Tactic.Common.

[Kim Morrison]

Otherwise, I think we are okay. (Discussion amongst maintainers was positive.)

[Siddhartha Gadgil]

Kim Morrison said:

Let's add this in Mathlib.Tactic.Common.

Do you mean so that the command is available without import LeanSearchClient?

[Kim Morrison]

yes

[Siddhartha Gadgil]

I will add this.

[Siddhartha Gadgil]

Added and pushed.

[Kim Morrison]

Merged!

[Kim Morrison]

As soon as it lands and I've tested it on branch#master, I propose moving it to leanprover-community and updating the lakefile.

[Kim Morrison]

Then #loogle and #moogle? :-)

[Siddhartha Gadgil]

Kim Morrison said:

As soon as it lands and I've tested it on branch#master, I propose moving it to leanprover-community and updating the lakefile.

Fine with me. I believe that I need to be made a member of leanprover-community to transfer it. If there is some other way that is also fine.

[Siddhartha Gadgil]

Kim Morrison said:

Then #loogle and #moogle? :-)

Sure, if they provide JSON APIs.

[Kim Morrison]

One step we missed: #16717

[Kim Morrison]

@Siddhartha Gadgil, see my message above about the Moogle API endpoint, and Jesse's response approving that we use it.

[Siddhartha Gadgil]

Kim Morrison said:

Siddhartha Gadgil, see my message above about the Moogle API endpoint, and Jesse's response approving that we use it.

I will work on this. I think the type is useful to users so I will pick that from the environment (moogle does not seem to provide it). Otherwise the code can be mostly the same (should use a common abstraction for the core of search results).

[Joachim Breitner]

Siddhartha Gadgil said:

Kim Morrison said:

Then #loogle and #moogle? :-)

Sure, if they provide JSON APIs.

Loogle does: https://loogle.lean-lang.org/json?q=List%20?a%20-%3E%20(?a%20-%3E%20?b)%20-%3E%20List%20?b

(Although for loogle I hope that eventually it can just run locally, so that it works offline, uses the precise version that you are using, and can index more than just mathlib.)

[Siddhartha Gadgil]

The#moogle cases are implemented and a PR is at https://github.com/siddhartha-gadgil/LeanSearchClient/pull/3 (PR for the client still).

[Siddhartha Gadgil]

The names are a bit asymetrical (default name for leansearch). I will fix this.

[Siddhartha Gadgil]

Names are now symmetric. I think it is ready to merge.

[Kim Morrison]

Left some minor comments.

[Kim Morrison]

The bigger refactor would be to combine the 6 elaboration functions into 1, with suitable switching.

[Kim Morrison]

e.g. pulling out the "if ends with . or ?, else warning" could be abstracted into a single function.

[Kim Morrison]

Not essential, but the code duplication costs in the long run.

[Siddhartha Gadgil]

I have made the minor changes. I will gradually get rid of the code duplication - there are too many pairs of functions among other things.

[Siddhartha Gadgil]

@Kim Morrison I have avoided many methods that were pairs for the two cases. Some duplication remains - for example the if statements but may be a bit complex to remove as the types are different and need various typeclasses (to allow throw, TryThis etc).

If things seem fine please merge. I will make a fresh PR on Mathlib updating this dependency.

[Kim Morrison]

I've merged.

[Kim Morrison]

You shouldn't need to make a PR to mathlib. It automatically bumps its dependencies every few hours.

[Kim Morrison]

I updated the github organization in the lakefile at #16750

[Siddhartha Gadgil]

Once this lands it may be worth posting about the new commands in "announce". I can do so following the README.

[Kim Morrison]

Definitely!

[Kim Morrison]

Are you planning on doing #loogle too? If we even get a locally running #loogle of course we'll then remove it.

[Kim Morrison]

(If so, it would be good to include the "help text" from loogle.com in the incomplete input warning.)

[Siddhartha Gadgil]

Yes, I will do loogle too. I assume you mean the text at the top: "You can use Loogle from witin the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot."

[Kim Morrison]

No, I meant the entire usage text (5 bullet points)

[Siddhartha Gadgil]

Sure. I will include it.

[Siddhartha Gadgil]

Just to clarify, here is what I see on the loogle website:

## Usage
Loogle finds definitions and lemmas in various ways:

1. By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
woould find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

Shall I include all of this?

[Kim Morrison]

I think so.

[Siddhartha Gadgil]

@Kim Morrison I implemented the loogle search on a branch, and I feel the same interface does not work well at all.

The main difference is for natural language queries "there are no stupid questions" - anything has some answer, at worst not a useful one. On the other hand most Loogle queries are simply wrong syntax. So one really has to be able to interact well with the error messages.

For example on Loogle I typed "List ?a → (?a → ?b) → List b" and got the error "unknown identifier 'b'". From that it is easy to see that the query should be ""List ?a → (?a → ?b) → List ?b".

I can of course include the error message but the code will be different in many places from the other two. I would be happy to do this given a documented JSON API if the loogle developers would like such an interface.

[Shreyas Srinivas]

@Siddhartha Gadgil I used the API as is last year, there are only four fields in the output

[Shreyas Srinivas]

You can see them all here: https://loogle.lean-lang.org/json?q=Real.sin

[Siddhartha Gadgil]

I saw the fields. But these are the four fields in the case of success.

[Shreyas Srinivas]

and these for the error case : https://loogle.lean-lang.org/json?q=nonsense

[Shreyas Srinivas]

I think I got all the success and error cases by clicking on the examples in the error page and then manipulating them to get the error cases.
https://loogle.lean-lang.org/json?q=|-+tsum+_+%3D+_+*+*tsum+_

[Siddhartha Gadgil]

I see.
The point remains that Loogle is a different sort of beast from the natural language searches. So there will have to be a discussion on the interface and the code copied and modified.

[Siddhartha Gadgil]

Happy to do this if people find it useful (even if temporarily, i.e., till the proper local loogle comes along).

[Shreyas Srinivas]

For implementing the loogle extension I followed the principle that there are either "hits" or "suggestions". I treated everything else as a generic error

[Shreyas Srinivas]

https://github.com/Shreyas4991/loogle-lean/blob/main/src/loogle-api.ts

[Shreyas Srinivas]

Sorry this one: https://github.com/Shreyas4991/loogle-lean/blob/main/src/loogle-interface.ts

[Siddhartha Gadgil]

The core abstraction is also different here. In the other cases I had a SearchResult structure. Now I should have an inductive type for the two cases.

[Siddhartha Gadgil]

The above info is enough to implement. Thanks.

[Siddhartha Gadgil]

I will simply wait for a consensus on whether this is worthwhile.

[Shreyas Srinivas]

Specifically the function you want to look for is loogle-interface.ts is processLoogleJson

[Jireh Loreaux]

I would definitely appreciate #loogle. I use it far more than the natural language searches.

[Siddhartha Gadgil]

Jireh Loreaux said:

I would definitely appreciate #loogle. I use it far more than the natural language searches.

Will implement now and ask for feedback on the interface.

[Shreyas Srinivas]

@Siddhartha Gadgil : since I have some experience with the loogle API, I could make a PR to your repository if it is welcome

[Siddhartha Gadgil]

Shreyas Srinivas said:

Siddhartha Gadgil : since I have some experience with the loogle API, I could make a PR to your repository if it is welcome

I am halfway through the implementation since it is mostly copy-paste and modify. Once I have a first draft up feel free to suggest and/or PR improvements.

[Mauricio Collares]

Jireh Loreaux said:

I would definitely appreciate #loogle. I use it far more than the natural language searches.

AFAIK you can run loogle locally (but #loogle is a good idea nonetheless)

[Shreyas Srinivas]

Inside tactic mode, would loogle do substantially better than refine?

[Henrik Böving]

Mauricio Collares said:

Jireh Loreaux said:

I would definitely appreciate #loogle. I use it far more than the natural language searches.

AFAIK you can run loogle locally (but #loogle is a good idea nonetheless)

Running loogle locally is possible but it does take a bit to spin up its search cache so starting it up with #loogle is going to have quite a bit of latency depending on how good your machine is. I think if local loogle becomes a thing that people want to use we would need something like a loogle daemon that you can send queries to.

[Siddhartha Gadgil]

As it is a couple of hours to implement, it seems the best option is to just implement #loogle and see what parts are used. Its use is also transient so code rot is not a real danger.

[Shreyas Srinivas]

I use my extension largely to do a quick search and in-place insert as well as a quick mathlib doc search

[Shreyas Srinivas]

A loogle command in tactics will probably do similar things. What's nice about exact? simp? etc is that they also take local context into account

[Henrik Böving]

Siddhartha Gadgil said:

As it is a couple of hours to implement, it seems the best option is to just implement #loogle and see what parts are used. Its use is also transient so code rot is not a real danger.

There are advantages to having a local loogle that a web loogle cannot provide though. For example you can search your own libraries/forks etc. and also at versions that upstream loogle does not currently have. So in general there is a motivation to have local loogle, it's just not something that someone has done because it's not easy

[Siddhartha Gadgil]

The command syntax is implemented. I have three different outputs for three cases:

• Success: a TryThis as with the other search engines.
• Error and no suggestions: Error message and loogle instructions
• Error with suggestions: Error message, loogle instruction and a TryThis for a #loogle command for each suggestion.

The lean code giving these cases is:

#loogle "List ?a → ?b" go

#loogle "nonsense" go

#loogle "?a → ?b" go

Here are screenshots of part of the infoview in the three cases.
image.png

image.png

image.png

@Jireh Loreaux @Shreyas Srinivas any suggestions about the interface. The other cases are essentially copy-paste from this (and the earlier code).

[Shreyas Srinivas]

1. Is the loogle usage Info presented every time?

[Shreyas Srinivas]

2. I think I have an idea to unify these interfaces with a single client side API

[Shreyas Srinivas]

3. You might want to show the declaration type in a new line. How does it work for theorem names?

[Shreyas Srinivas]

Especially ones with long type signatures?

[Shreyas Srinivas]

4. I love the idea of waiting for a "go" at the end before a search begins

[Siddhartha Gadgil]

Shreyas Srinivas said:

3. You might want to show the declaration type in a new line. How does it work for theorem names?

I feel that looks like "#check". In any case that aspect was discussed extensively for #leansearch. The failure cases are what are different here.

Not to say one cannot discuss formatting common to all cases. But maybe that is best done once the features are announced.

[Siddhartha Gadgil]

For now we can focus on where loogle differs from the others.

[Siddhartha Gadgil]

By the way, the "go" is a replacement for ending with "." or "?" which makes sense for natural language but not loogle.

[Shreyas Srinivas]

A good test for error with suggestions is "sin"

[Shreyas Srinivas]

Because there are many sin functions

[Shreyas Srinivas]

Also "Measurable"

[Siddhartha Gadgil]

Shreyas Srinivas said:

A good test for error with suggestions is "sin"

Thanks for this. I wanted a good test. Here is the result:
image.png

[Siddhartha Gadgil]

The clicking worked, so perhaps this feature is useful.

[Siddhartha Gadgil]

For example, after a click:
image.png

[Shreyas Srinivas]

Another test is to disconnect the wifi and try it

[Siddhartha Gadgil]

Shreyas Srinivas said:

Another test is to disconnect the wifi and try it

To test what?

[Shreyas Srinivas]

The error message and latency will tell you whether curl is correctly set up

[Siddhartha Gadgil]

Fair enough, but I will leave that system level testing to the experts. I am just making a "curl" command assuming it works.

[Shreyas Srinivas]

I am talking about the command is called from the program. Max retries, timeouts, etc can be configured

[Siddhartha Gadgil]

Shreyas Srinivas said:

I am talking about the command is called from the program. Max retries, timeouts, etc can be configured

For this and the other parts too, I welcome PRs once the main logic is stable to make this robust. It is not something I will manage particularly well.

[Jireh Loreaux]

Thanks @Siddhartha Gadgil, I will have a look later today!

[Joachim Breitner]

#loogle "nonsense" go

This syntax is groublesome, since loogle queries often contain quotes itself. Why not

#loogle List ?a → ?b go

where everything until go becomes the query?

Else you can also embed loogle’s syntax parser in your command:
https://github.com/nomeata/loogle/blob/master/Loogle/Find.lean#L255-L264

[Shreyas Srinivas]

Reading the code, I think we can have one command and some optional arguments that then searches and returns results from one or more search engines. This can exist along side the service specific commands

[Siddhartha Gadgil]

Joachim Breitner said:

#loogle "nonsense" go

This syntax is groublesome, since loogle queries often contain quotes itself. Why not

#loogle List ?a → ?b go

where everything until go becomes the query?

Else you can also embed loogle’s syntax parser in your command:
https://github.com/nomeata/loogle/blob/master/Loogle/Find.lean#L255-L264

The simple answer is I don't know how to write a parser for what you suggest. If you have sample code I can try

[Shreyas Srinivas]

@Joachim Breitner : In this case, it seems sufficient to accept a term and convert it to a faithful string representation

[Joachim Breitner]

The simple answer is I don't know how to write a parser for what you suggest. If you have sample code I can try

As linked, it’s just

syntax turnstyle := patternIgnore("⊢ " <|> "|- ")
syntax find_filter := (turnstyle term) <|> term
syntax find_filters := find_filter,*

(although of course could be extended in the future, but then we can update the code.)

[Jireh Loreaux]

@Shreyas Srinivas one downside of a single command: users may not want to share their queries with all searches (e.g., maybe they trust Loogle but not Moogle, etc.). I'm fairly certain this would be true for some people.

[Shreyas Srinivas]

In my idea, you'll have something like #search loogle "something" or #search all "something"

[Shreyas Srinivas]

or even #search [loogle, leansearch] "something"

[Patrick Massot]

It makes me think @Damien Thomine wanted to know how to ask Loogle for something whose assumption contains something. And indeed we noticed that term turnstyle didn’t seem to work.

[Joachim Breitner]

Yes, the turnstyle means “don’t look in subexpressions”, and is maybe not the best symbol given that people expect stuff to the left of it. But off-topic in this already long topic :-)

[Shreyas Srinivas]

I think I can refactor this code and make it more systematic and provide a uniform front facing API

[Shreyas Srinivas]

And also separate the service specific aspects

[Shreyas Srinivas]

@Siddhartha Gadgil : Is this welcome?

[Shreyas Srinivas]

Also is the loogle thing merged?

[Shreyas Srinivas]

I don't see it yet

[Siddhartha Gadgil]

It is on a branch called loogle

[Siddhartha Gadgil]

Shreyas Srinivas said:

Siddhartha Gadgil : Is this welcome?

I am getting dinner. Will reply in a bit

[Siddhartha Gadgil]

@Shreyas Srinivas I don't know if you have looked at the code but it does separate to some extent the server queries and the elaboration. For example, the following is part of the code:

declare_syntax_cat search_cmd
syntax "#leansearch" : search_cmd
syntax "#moogle" : search_cmd

syntax (name := search_cmd) search_cmd str : command

I am sure more streamlining can be done and PRs improving the code (without changing behaviour) are always welcome. The bigger streamlining is avoiding duplication between the command, term and tactic elaborators. I did not try this because it seemed to involve monad polymorphim with signature including MonadLog and maybe a typeclass that says we can lift from MetaM. Anyone who can do this correctly is welcome to PR.

As for syntax, we definitely do not want a common search for leansearch/moogle and loogle as the queries are very different. What I have done (as in the code above) is not very different from #search moogle and #search leansearch. Yes, the "all" option is not there but especially in term/tactic a single word is more readable.

For loogle I will work on @Joachim Breitner's suggestion and try to use the same syntax as #find.

[Joachim Breitner]

(NB: It’s not the same syntax as #find. Loogle evolved out of #find, hence find_filters in the name above, but it should really be loogle_filters instead.)

[Siddhartha Gadgil]

I will call it loogle_filters.

As you are here @Joachim Breitner what is the recommended way I get a string from this? Is Syntax.reprint fine?

[Siddhartha Gadgil]

I mean just a string to pass on to Loogle.

[Joachim Breitner]

In loogle I use this code t turn sugg into a string, not sure if’s the best way of doing it

(← PrettyPrinter.ppCategory ``Find.find_filters sugg).pretty

[Joachim Breitner]

But reprint may be just as fine

[Siddhartha Gadgil]

I used your code above and it works perfectly.

[Shreyas Srinivas]

@Siddhartha Gadgil : the syntax needn't be different with a nice API design. Firstly, loogle still accepts name queries. Further, a common search command would read the server responses and determine which results to show.

To get into more detail, what I am proposing is a code org principle, where a common client API exists with middleware for handling each service. This not only provides users a uniform interface to use them, but also in the medium term provides developers or search tools an idea for the desired shape of their API endpoints

[Shreyas Srinivas]

And there is certainly a case to be made for a common search result type with an alt parameter. For moogle and leansearch, this is their error message. For loogle this is a type with error messages and a suggestion list

[Siddhartha Gadgil]

I understand the principle, but here there are only two services and a small amount of code. Still if the code looks better I will happily accept a PR.

[Siddhartha Gadgil]

I have used common code for the success case of both Leansearch/Moogle and Loogle. The failures have a different nature.

[Siddhartha Gadgil]

So the syntax now looks like this:

#loogle List ?a → ?b go

#loogle nonsense go

#loogle ?a → ?b go

#loogle sin go

[Henrik Böving]

Does the middle part accept all common loogle things? i.e. also searching with "quotes" and having multiple constraints separated by comma?

[Shreyas Srinivas]

I will finish something by tonight. (It's 16:31 in CEST right now). Maybe that will give you a better picture of what I mean

[Siddhartha Gadgil]

Henrik Böving said:

Does the middle part accept all common loogle things? i.e. also searching with "quotes" and having multiple constraints separated by comma?

If you have a specific example I can test. But my syntax definition is the following, using Loogle's own syntax so I expect things should work the same.

syntax turnstyle := patternIgnore("⊢ " <|> "|- ")
syntax loogle_filter := (turnstyle term) <|> term
syntax loogle_filters := loogle_filter,*

syntax (name := loogle_cmd) "#loogle" loogle_filters "go" : command

[Joachim Breitner]

#loogle "sin", Real → Real, |- Real go

[Siddhartha Gadgil]

image.png

Seems fine.

[Siddhartha Gadgil]

Thanks all for the suggestions. Now the term, tactic and command modes are implemented and PRed. Some examples of Syntax are the following:

#loogle sin go
#loogle nonsense go
#loogle "sin", Real → Real, |- Real go

example : 3 ≤ 5 := by
  #loogle Nat.succ_le_succ go
  decide
example := #loogle List ?a → ?b go

• In case of success, there are code actions to replace with search results (#check ... for command search, the term for term search and whichever of apply, have, rw are valid for tactic search).
• In case of error, the Loogle instructions are given.
• In case of error with suggestions, there are also TryThis options for the suggestions.
• As with the #moogle and #leansearch commands, in tactic mode only valid tactics are shown (an advantage over a web search).

For the examples given above, here are screenshots of the infoview:

image.png

image.png

image.png

image.png

image.png

[Siddhartha Gadgil]

@Kim Morrison The automatic updating of dependencies is not happening. Maybe it does it only for those in a list and LeanSearchClient has to be added? I can just make a PR for updating.

Also #loogle is implemented and PRed. There was a fair amount of discussion and the syntax is as suggested by @Joachim Breitner (who also gave the code for the parser for this).

[Bryan Gin-ge Chen]

It looks like the automated job has been hitting an error when it tries to run lake update: error: leanprover-community/LeanSearchClient: could not materialize package: dependency has no explicit source and was not found on Reservoir. (Unfortunately, I don't know enough about how lake works to say any more.)

[Siddhartha Gadgil]

Bryan Gin-ge Chen said:

It looks like the automated job has been hitting an error when it tries to run lake update: error: leanprover-community/LeanSearchClient: could not materialize package: dependency has no explicit source and was not found on Reservoir. (Unfortunately, I don't know enough about how lake works to say any more.)

Thanks. Looks like I need to get https://github.com/leanprover-community/LeanSearchClient on Reservoir. Maybe the easiest way is to give it a star myself :shrug:

[Bryan Gin-ge Chen]

I've given it a star as well!

[Bryan Gin-ge Chen]

Seems like the workflow is still getting the same error that LeanSearchClient was not found on Reservoir...

[Jiang Jiedong]

Bryan Gin-ge Chen said:

Seems like the workflow is still getting the same error that LeanSearchClient was not found on Reservoir...

I am really sorry that LeanSearch is temporarily offline...

The engineers are trying to reboot the service now. It may take about 24 hours.

[Bryan Gin-ge Chen]

Ah, but I think this is an issue on Reservoir's side, not LeanSearch.

[Kim Morrison]

@Bryan Gin-ge Chen, multiple problems: it's also just down!

[Siddhartha Gadgil]

There was a reservoir update that did not pick up LeanSearchClient though (even though it met criteria).

[Siddhartha Gadgil]

@Kim Morrison Shall I merge the loogle code and then have a PR to manually update the dependency in Mathlib (temporarily specify the path in the lakefile and run lake update LeanSearchClient)? Since the repo is not likely to be updated often, this may be easier that fixing everything in the path.

Either way we should hold off the announcement till LeanSearch is back up.

[Kim Morrison]

Sorry, I'm confused, why is the automatic process not working?

[Kim Morrison]

(I'd prefer to fix the automatic process rather than work around it, if possible.)

[Kim Morrison]

Oh, I see, the problem is just that Reservoir has still not recognised LeanSearchClient exists at all.

[Siddhartha Gadgil]

For the automatic process to work Reservoir has to pick up the repository. It did not at first presumably because it had only one star. However, once it had three it still failed for unknown reasons. I reported this.

[Siddhartha Gadgil]

Maybe @Mac Malone can be alerted here.

[Kim Morrison]

@Mac Malone, do you know why this is? We really need an easy to find page on Reservoir "why did reservoir not find package X", and link to it from any failed search result.

[Kim Morrison]

Users are going to be pretty annoyed if they can't find out why their package doesn't appear.

[Siddhartha Gadgil]

The merging of loogle syntax is independent of this. I will go ahead if there is no issue.

[Siddhartha Gadgil]

But I will not try any manual updating. As LeanSearch is down anyway one can hope both issues get fixed over the next day or so.

[Jiang Jiedong]

The LeanSearch service has now been restored.

[Siddhartha Gadgil]

And the CI for LeanSearchClient is green again. Still awaiting Reservoir though.

[Joachim Breitner]

Could the LeanSearchClient set a custom User-Agent? Simply passing #["--user-agent", "LeanSearchClient"] to curl should suffice. Bonus points if you include the version number of LeanSearchClient and the current toolchain (Lean.versionString) in the header (not sure if there is an easy way to get the version of the current project, if not, don’t worry about it)

[Shreyas Srinivas]

does the toolchain string actually make sense?

[Shreyas Srinivas]

loogle is using its own toolchain right?

[Siddhartha Gadgil]

Joachim Breitner said:

Could the LeanSearchClient set a custom User-Agent? Simply passing #["--user-agent", "LeanSearchClient"] to curl should suffice. Bonus points if you include the version number of LeanSearchClient and the current toolchain (Lean.versionString) in the header (not sure if there is an easy way to get the version of the current project, if not, don’t worry about it)

I don't know what a custom User-Agent is. What functionality do you want (I will google meanwhile)?

[Shreyas Srinivas]

a user-agent is HTTP lingo for "tell me what kind of a client you are"

[Shreyas Srinivas]

https://reqbin.com/req/c-ekublyqq/curl-user-agent

[Siddhartha Gadgil]

Found mdn docs https://developer.mozilla.org/en-US/docs/Web/HTTP/Headers/User-Agent. Will read and try to implement.

[Shreyas Srinivas]

In practice this means inserting a string in the curl arguments list that indicates that leansearch is making the curl request. EDIT : for e.g. adding "-A \"leansearch\" " as an element in the list you build up for args

[Siddhartha Gadgil]

@Joachim Breitner I added a user agent. If you are logging at loogle there should be 3 calls with "LeanSearchClient" as the user agent.

[Joachim Breitner]

Indeed:

49.206.1.114 - - [16/Sep/2024:12:55:03 +0000] "GET /json?q=List%20%3Fa%20%E2%86%92%20%3Fa HTTP/2.0" 200 25612 "-" "LeanSearchClient"
49.206.1.114 - - [16/Sep/2024:12:55:09 +0000] "GET /json?q=List%20%3Fa%20%E2%86%92%20%3Fa HTTP/2.0" 200 25612 "-" "LeanSearchClient"
49.206.1.114 - - [16/Sep/2024:12:55:09 +0000] "GET /json?q=Nat.succ_le_succ HTTP/2.0" 200 246 "-" "LeanSearchClient"

thanks!

[Julian Berman]

Just to point it out -- that will lose editor information unless LeanSearchClient provides a way to configure the user agent as well (e.g. you won't be able to tell whether it's LeanSearchClient within VSCode vs elsewhere)

[Siddhartha Gadgil]

I have added a configurable option leansearchclient.useragent set by default to LeanSearchClient.

[Julian Berman]

That's a thing you need to set in Lean though right? That means every user using LeanSearchClient will need to set it (which still seems useful to keep, so I would keep it as a setting well), but in order to be able to set it from e.g. editor plugins, or from someone writing a client on top of LeanSearchClient for whatever reason, it I think would also need to try to optionally look at the "active" LSP client configurations (and in that case e.g. the VSCode integration can set a default value for VSCode, I can set one for neovim, etc. such that users of the editors don't need to themselves set it). Perhaps this is overcomplicating things so feel free to ignore though, or to tell me I should help find exactly where that is exposed by the Lean server (I suspect it is, but I don't know where off hand)!

[Joachim Breitner]

I think we don’t need to worry about this. It’s already useful to roughly know which loogle UI people use, I don’t mind if I don’t know which editor those users that use #loogle are using.

[Mac Malone]

Kim Morrison said:

Mac Malone, do you know why this is? We really need an easy to find page on Reservoir "why did reservoir not find package X", and link to it from any failed search result.

The problem appears to simply be that Lean Search does not appear in the first 1000 code search results. 1000 is the rate limit for a batch of results (before needing ot wait for a reset). This can be improved by Reservoir staggering its requests to obtain more results, but the better long-term solution is a form of manual registration. I have a conceptual sketch of how to do this, I just need to have the time to dedicate to it.

[Mac Malone]

Given the current Reservoir limitations, it may be worth adding a disclaimer/note to the Reservoir Inclusion Criteria to help users understand why their new package may not yet be included.

[Siddhartha Gadgil]

The issue here is that LeanCodeSearch has been added as a Mathlib dependency with the standard format (formatted @Kim Morrison) and this depends on it being in Reservoir.

[Siddhartha Gadgil]

@Mac Malone I take it that it will not be picked up soon.
@Kim Morrison Then a manual update may be the best.

[Mac Malone]

Siddhartha Gadgil said:

The issue here is that LeanCodeSearch has been added as a Mathlib dependency with the standard format (formatted Kim Morrison) and this depends on it being in Reservoir.

It is possible to provide both a Reservoir require and Git source (which it wil fallback to if it cannot find it on Reservoir).

[Siddhartha Gadgil]

@Mac Malone Currently the line in lakefile is

require "leanprover-community" / "LeanSearchClient" @ git "main"

How do I add the explicit address https://github.com/leanprover-community/LeanSearchClient?

[Mac Malone]

Append from git "https://github.com/leanprover-community/LeanSearchClient" @ "main"

[Siddhartha Gadgil]

@Mac Malone Thanks.
That seemed to work, but just to keep the lakefile clean, should I end with .git? I copied from the address bar not the git address?

[Siddhartha Gadgil]

I asked because of a change in lake-manifest, but this way seems consistent with the other entries. So I suppose without .git is correct.

[Mac Malone]

Either should work.

[Siddhartha Gadgil]

A PR is up at https://github.com/leanprover-community/mathlib4/pull/16857 just making this change and the corresponding change in the lake-manifest (by running lake update LeanSearchClient).

@Kim Morrison Can you please merge (or some other maintainer around if the change is fine)?

[Kim Morrison]

Ugh, I had really hoped that we would use this as an opportunity to unbreak Reservoir. I think it's essential that we stop working around limitations in Reservoir and instead get them fixed. :-(

[Kim Morrison]

@Mac Malone, can we at least make sure that by v4.12.0 there is a really clear error message in this use case?

[Kim Morrison]

Users are going to (are already) writing

require "leanprover-community" / "LeanSearchClient" @ git "main"

for repositories that Reservoir has failed to index.

Possible solutions:

• Reservoir actually indexes everything.
• At least one of (and ideally all four):
  • The "failed to materialize" error contains a link to a manual registration page.
  • The "failed to materialize" error contains a link to a page explaining why that project isn't available on reservoir.
  • The "failed to materialize" error shows you exactly what to write to make things work anyway right now.
  • The "failed to materialize" errors pings Reservoirs and tells it to go index the package, and tells the user to try again soon.

[Siddhartha Gadgil]

Mathlib update is failing again. Errors such as error: ././././Mathlib/Data/Nat/MaxPowDiv.lean:30:30: unexpected token 'go'; expected search_cmd are causing the build to fail. Presumably one of the other dependencies changed in a way that needs update.

I had forgotten to import the loogle syntax and updated this a couple of hours ago. Because of the build failures it is still not available (though the #leansearch and #moogle are fine).

[Kim Morrison]

This is preventing nightly-testing from compiling. :-(

[Kim Morrison]

My guess is that this is LeanSearch's fault.

[Kim Morrison]

Yes, you've made go a token, so no one downstream can use it as a function name.

[Kim Morrison]

I've reverted nightly-testing to 5f3c33d7f641d26bd013d8bb4cafcb5ccce53dc4, before loogle landed in LeanSearchClient.

[Kim Morrison]

This will break Mathlib's auto-dependency update for now.

[Kim Morrison]

@Siddhartha Gadgil, will you have a chance to have a look at this? I might be able to in about 3 hours, not sure if I'll have time tonight.

[Siddhartha Gadgil]

Oops, sorry.

[Siddhartha Gadgil]

I saw the "go" in the error but did not realize it was mine. Will replace it by "do" which is already a token I assume.

[Kim Morrison]

I would much prefer to see a debouncing solution rather than relying on a weird terminator.

[Siddhartha Gadgil]

@Kim Morrison I have replace "go" by "do_search" which I checked is nowhere is Mathlib. Not so elegant but hopefully will not break anything.

[Siddhartha Gadgil]

Sorry, just saw your email.

[Kim Morrison]

If we don't require a terminator, what actually happens to the earlier searches when you type the next keystroke. Does it get cancel, or does it live on? (Sorry, I can't remember what happens to commands calling IO... I fear that it lives on.)

[Kim Morrison]

If it got cancelled, an easy solution here would be to just wait 200ms before calling curl.

[Kim Morrison]

Actually, maybe we can do this with an IO.ref in any case.

[Kim Morrison]

When the command is called, write the current time into an IO.ref. Then wait 200ms. Now read the ref again. If it has changed in the meantime, just stop. Otherwise, proceed with the search.

[Siddhartha Gadgil]

I think it works fine. Only thing is partial syntax that is still valid triggers, but only if one pauses.

[Kim Morrison]

What works fine?

[Siddhartha Gadgil]

I will test and confirm that just dropping the terminations works.

[Siddhartha Gadgil]

The following examples work fine.

#loogle List ?a → ?a

example := #loogle List ?a → ?a


set_option loogle.queries 1

example : 3 ≤ 5 := by
  #loogle Nat.succ_le_succ
  sorry

[Siddhartha Gadgil]

And I typed it out. The default delay is enough that things were not triggered.

[Siddhartha Gadgil]

Does this syntax seem fine? I will push to LeanSearchClient.

[Siddhartha Gadgil]

I have pushed. If things are fine can you restore the auto-update?

[Siddhartha Gadgil]

@Kim Morrison I am afraid even the new Loogle syntax is breaking Mathlib. This time the culprit is the turnstile symbol which I copied from Loogle's own syntax as given by @Joachim Breitner

For the present I will simply remove Loogle syntax so that the dependency update does not keep breaking.

[Siddhartha Gadgil]

(deleted)

[Siddhartha Gadgil]

I realized that even though LoogleSyntax is not imported in Mathlib.Tactic, it can still be explicitly imported and works. So at present all syntax is available, but loogle needs an extra step.

[Daniel Weber]

The parsing still doesn't seem to work well -

import Mathlib

example : True := by
  have : =

triggers it for example (and causes it to panic)

[Shreyas Srinivas]

I think you are going to end up in a situation where loogle is flooded with requests if you don't have a terminating token

[Joachim Breitner]

You can try wrapping

syntax turnstyle := patternIgnore(nonReservedSymbol("⊢ ") <|> nonReservedSymbol("|- "))

and the same for your "go", this should then not break stuff downstream. I don't know how well it works for something you want to parse after an expression.

[Siddhartha Gadgil]

Now the "update mathlib dependency" is running fine but the lake-manifest.json has not updated.

[Daniel Weber]

Daniel Weber said:

The parsing still doesn't seem to work well -

import Mathlib

example : True := by
  have : =

triggers it for example (and causes it to panic)

Should I make an issue in the repository for this?

[Siddhartha Gadgil]

Daniel Weber said:

Daniel Weber said:

The parsing still doesn't seem to work well -

import Mathlib

example : True := by
  have : =

triggers it for example (and causes it to panic)

Should I make an issue in the repository for this?

Sure. But do you know whether it is triggered by the new syntax? Please make an issue and I will test if it is.

[Siddhartha Gadgil]

Actually, could you replace import Mathlib by import LeanSearchClient and see if you get the same error?

[Daniel Weber]

I do, yes:

import LeanSearchClient

example : True := by
  have : =

[Siddhartha Gadgil]

Please make an issue then. I will work on miniming it. Thanks for flagging.

[Daniel Weber]

Actually, even

import LeanSearchClient

apple

produces the "wrong" error message - "unexpected identifier; expected search_cmd" instead of what's produced without import LeanSearchClient, "unexpected identifier; expected command"

[Siddhartha Gadgil]

Thanks. I see now the probable cause.

[Siddhartha Gadgil]

There are parsers that begin with the search_cmd syntax category that are triggered and then give errors. This was only to avoid code duplication. Will avoid this.

[Siddhartha Gadgil]

@Daniel Weber This has been fixed in LeanSearchClient. The new dependency should make its way to Mathlib with the next update (in a couple of hours)

[Floris van Doorn]

Can you filter auxiliary theorems from the results of LeanSearch?
If I search for addition is continuous the first returned results are

#check stereoToFun.proof_4 -- ContinuousAdd ℝ
#check bernsteinApproximation.proof_1 -- ContinuousAdd ℝ
#check VectorFourier.mul_L_schwartz.proof_1 -- ContinuousAdd ℝ
#check Orientation.areaForm'.proof_4 -- ContinuousAdd ℝ
#check MeasureTheory.ComplexMeasure.equivSignedMeasure.proof_2 -- ContinuousAdd ℝ
#check VectorFourier.mul_L.proof_1 -- ContinuousAdd ℝ

and Continuous.add is not in the first 50 results.

[Jiang Jiedong]

Thank you for your feedback! We will definitely remove these generated auxiliary results in the next update.

[Floris van Doorn]

And a remark about LeanSearchClient: it should cache results from searches (at least when used as a command / used in the same context as a tactic). If I type above a #leansearch command it seems that the query gets sent many times.

[Shreyas Srinivas]

Floris van Doorn said:

And a remark about LeanSearchClient: it should cache results from searches (at least when used as a command / used in the same context as a tactic). If I type above a #leansearch command it seems that the query gets sent many times.

The requests can be reduced if a search terminator syntax is used. I recall that loogle can/(will be able to) cache search results when run locally

[Mario Carneiro]

I think caching is more reliable though at avoiding repeated requests

[Shreyas Srinivas]

Can we re-purpose the DiscrTree that simp uses, to store search results and query them

[Floris van Doorn]

Shreyas Srinivas said:

Floris van Doorn said:

And a remark about LeanSearchClient: it should cache results from searches (at least when used as a command / used in the same context as a tactic). If I type above a #leansearch command it seems that the query gets sent many times.

The requests can be reduced if a search terminator syntax is used. I recall that loogle can/(will be able to) cache search results when run locally

This doesn't help if I write on a line above a query (with terminator).

[Siddhartha Gadgil]

Floris van Doorn said:

And a remark about LeanSearchClient: it should cache results from searches (at least when used as a command / used in the same context as a tactic). If I type above a #leansearch command it seems that the query gets sent many times.

Agree. Will implement tomorrow

[Siddhartha Gadgil]

@Floris van Doorn I have implemented caching. There is only a single function that does the querying (independent of mode) so caching is done here by query.

[Kim Morrison]

@Jiang Jiedong, leansearch.net appears to be down.

[Jiang Jiedong]

@Kim Morrison Sorry that currently, the engineers are redeploying the service. Before Monday the LeanSearch service will be online again.

[Floris van Doorn]

Leansearch seems to struggle today. It was down half an hour ago, and now whenever I search for something, I get the response too fast.

[Shreyas Srinivas]

I wonder if the FRO could host one of these NLP search engines directly

[Shreyas Srinivas]

And open source the model

[Shreyas Srinivas]

We might benefit from one of the smaller locally runnable models

[Shreyas Srinivas]

Currently all NL search engines appear to be close sourced and privately hosted and we never know when they crash, why they crash, and when they get retrained

[Jiang Jiedong]

Sorry that there is a problem with the LeanSearch server now. We are trying to fix it.

[Jiang Jiedong]

Shreyas Srinivas said:

And open source the model

That is a very good idea. The PKU team would like to open the pipeline to add new theorems to the model after we develop some new features for the LeanSearch engine in the future.

[Jiang Jiedong]

After that, the FRO can maintain an always-up-to-date LeanSearch. Currently, the LeanSearch database is not updating frequently.

[Jiang Jiedong]

Now LeanSearch is working again. :at_work:

[Floris van Doorn]

Thanks!