Loogle is live!

Stream: general

[Joachim Breitner]

It seems it’s faster to create a web interface around a new Lean command than get the corresponding PR in…

Anyways, here it is: https://loogle.lean-fro.org/

Remember to parenthesize if you are searching for expressions, else it turns into multiple patterns. And let me know if it fails to find something that you think it should find.

[Joachim Breitner]

Behind this URL is a Hetzner vhost with a nixos system with a ngingx reverse proxy (for SSL) in front of a small python HTTP server that then used stdin/stdout to talk to the loogle CLI (which you could also use locally); the last bit is locked down using SECCOMP. This is mostly a proof of concept setup, with the following limitations:

• It’s single-threaded (because python), which is actually a nice way to do rate limiting.
• It’s not automatically deployed yet, and happens to reflect whatever mathlib commit I am pinning. In particular, mathlib4#6363 ought to be merged before I can track master.
• This shouldn’t be the final hostname for this service. :check:
• Maybe this should be integrated into the docs page.
• Maybe this should also be available as a zulip bot (to answer “Is there code for X”-requests conveniently and while showing them how to find on their own). :check:
• If the loogle process dies and needs to be restarted, it is rebuilding the index for ~2 mins. This should maybe happen at buildtime already, and pickled into the program or loaded from file. :check:
• The web UI could probably be nicer.

Contributions welcome at https://github.com/nomeata/loogle – I’m keen on having this service, not so much running it ;-)

[Yury G. Kudryashov]

https://loogle.nomeata.de/?q=%28Real.sqrt+%28%3Fa+*+%3Fb%29%29 fails

[Yury G. Kudryashov]

As well as https://loogle.nomeata.de/?q=%28Real.sin+%28_+%2B+2*Real.pi%29%29 (one of the examples)

[Joachim Breitner]

Heh, looks like the heartbeats aren't reset between queries? Will investigate tomorrow.

[Frédéric Dupuis]

The second example ("two") also fails, with error "No constant in search pattern"

[Denis Gorbachev]

Congrats on the launch!

[Joachim Breitner]

Ok, now every query gets their own budget of :heart: :drum:, and the docs explain that pure substring searches are not supported yet (I’m waiting for https://github.com/leanprover/std4/pull/178 to see if that KMP matcher makes linear substrings matches fast enough without a dedicated index).

And I should really precompute the index and pickle it out, so that restarting the service doesn’t take several minutes … done

[Joachim Breitner]

Just moved it to https://loogle.lean-fro.org/ which has a higher chance of being a permanently available address, even if I run away screaming at some point.

[Yury G. Kudryashov]

ping: loogle.lean-fro.org: Name or service not known

[Yury G. Kudryashov]

Does it mean we should wait for DNS cache to propagate?

[Joachim Breitner]

Ah, I made a mistake, one moment. But yes, DNS related, so may take a few minutes for the fix to propagate.

[Arthur Paulino]

It might be worth documenting how to run this locally so people are able to use it without access to the internet

[Joachim Breitner]

Sure! What would you expect beyond what’s in https://github.com/nomeata/loogle/#readme, in particular

You can run this server locally as well, either using ./server.py if you
built loogle via lake, or using nix run ./#loogle_server if you use nix.

[Arthur Paulino]

Oh that's already there :tada:

[Arthur Paulino]

Not that I'm requesting this feature, it's just a suggestion: allow the user to point to an already existing mathlib folder, with cache files and stuff so it's not necessary to download cache and extract it again (duplicating file storage consumption)

[Joachim Breitner]

Also supported: You can pass different search paths to loogle. So you can run it on any .olean you might have around (I believe).
(Ok, this is only exposed with the CLI, not the web interface yet) :-)

[Jireh Loreaux]

A small suggestion: when linking search results to the docs, would it be possible to link directly to the declaration instead of using the find/?pattern.... The find is super useful for the Zulip linkifer, but it does take an extra second or two, and I figure you probably already have access to the file the decl lives in.

[Jireh Loreaux]

And a possible bug: searching for (star ?a * ?a = ?a * star _) returns docs#star_comm_self', but searching for (star ?a * ?a = ?a * star ?a) yields no results.

[Joachim Breitner]

Will investigate both, thanks.

[Joachim Breitner]

The latter might require help from someone who actually knows how lean works :-D, as I would expect hope that the current code handles this correctly

[Joachim Breitner]

Quite curious. It works no matter which ?a I replace. It also works with (star ?b * ?b = ?a * star ?a)…

[Joachim Breitner]

And for those who don’t want to leave Zulip:

[Joachim Breitner]

@loogle (Real.sin (_ + 2*Real.pi))

[loogle]

:search: docs#Real.sin_add_two_pi

[Joachim Breitner]

(You can also use private messages.)

[Henrik Böving]

@loogle ((?a -> ?b) -> ?f ?a -> ?f ?b)

[loogle]

:exclamation: Cannot search: No constants in search pattern.

[Henrik Böving]

@Joachim Breitner is this supposed to work? A similar thing on hoogle would find fmap right?

[Joachim Breitner]

That’s not supposed to work, loogle only supports queries that involve at least one constant (so that the index can be used and it doesn’t have to do a linear search), and the function arrow doesn't count.

[Henrik Böving]

@loogle ((?a -> ?b) -> List ?a -> List ?b)

[loogle]

:shrug: nothing found

[Henrik Böving]

@Joachim Breitner how about this? ^^

[Joachim Breitner]

@loogle |- ((?a -> ?b) -> List ?a -> List ?b)

[loogle]

:search: docs#List.map, docs#List.mapAsyncChunked, (and 2 more)

[Joachim Breitner]

Ok, this looks like a bug, it should work without |- in this case too. Thanks!

[Kevin Buzzard]

Let me just remark how phenomenally cool this is.

[Henrik Böving]

@loogle |- ([Functor ?f] -> (?a -> ?b) -> ?f ?a -> ?f ?b)

[loogle]

:shrug: nothing found

[Henrik Böving]

Can we maybe get this to work as well?

[Joachim Breitner]

Oh, the latest fixes re metavariables to #find didn't make it to the online site yet. Wait for a few hours (building mathlib…) before checking stuff with metavariables

[Henrik Böving]

I'll be back then^^

[Joachim Breitner]

Also, I am still very much a stumbling beginner when it comes to lean metaprogramming, so most of you are probably in better position to improve matters! (Loogle just wraps #find, so any improvement to that will help.)

[Joachim Breitner]

Maybe it's best to match function types (or foralls) up to reordering of hypothesis always, not just with |-.

[Yaël Dillies]

Kevin Buzzard said:

Let me just remark how phenomenally cool this is.

I feel replaced :sweat:

[Kevin Buzzard]

I remember Zagier once saying the same thing when OEIS went online.

[Joachim Breitner]

Yaël Dillies said:

I feel replaced :sweat:

Far from it, I am sure. I looked at the recent Is there code for X threads, and only the majority could be resolved directly using #find. So you'll remain at least as phenomenally cool!

[Henrik Böving]

Kevin Buzzard said:

I remember Zagier once saying the same thing when OEIS went online.

for the uninitiated: who is that? I presume they know number series?

[Newell Jensen]

@Joachim Breitner small suggestion/thought. The links could mention if it is for Std, Mathlib, Init, etc. Not a game changer but adds another layer of information when doing a broad search using the site.

[Joachim Breitner]

Right, it was already requested that the links go right to the right module, and when I implement that I thought I'd also show the module name after the name (maybe smaller or slightly grey).

[Kevin Buzzard]

Don Zagier is an excellent puzzle-solver and a former child prodigy, who is very good at e.g. identifying integer sequences, but is less good than a large database of such sequences.

[Newell Jensen]

@Joachim Breitner you might be aware of this already but the bot link for the "(and # more)" gives Not Found. Not sure you were planning on this being served properly or not but thought I would mention it in case.

[Joachim Breitner]

(deleted)

[Joachim Breitner]

@loogle |- ((?a -> ?b) -> List ?a -> List ?b)

[loogle]

:search: docs#List.map, docs#List.mapAsyncChunked, and 10 more

[Joachim Breitner]

Fixed, thanks!

[Joachim Breitner]

I'll be back then^^

The metavariable fix is now live, but it still doesn’t find Functor.map using various patterns. If someone feels like investigating, checkout mathlib4#6363 and add tricky queries to test/Find.lean, and then see if they can be made to work.

[Arthur Paulino]

Omg this is awesome

[Timo Carlin-Burns]

@loogle ((?a -> ?b) -> List ?a -> List ?b)

[loogle]

:shrug: nothing found

[Timo Carlin-Burns]

Looks like it still needs the |-

[Scott Morrison]

So... the loogle name is cute (and the tool amazing), but perhaps if could just be #find, even in its web and bot incarnations? :-)

[Bolton Bailey]

@loogle Fin _ ≃ Option _

[loogle]

:exclamation: <input>:1:6: expected end of input

[Bolton Bailey]

@loogle (Fin _) ≃ (Option (Fin _))

[loogle]

:exclamation: <input>:1:8: expected end of input

[Bolton Bailey]

@loogle ((Fin _) ≃ (Option (Fin _)))
Perhaps if I surround the whole thing in parens?

[loogle]

:search: docs#finSuccEquiv, docs#finSuccEquiv', and 13 more

[Bolton Bailey]

(The "13 more" link gives 502 bad gateway)

[Bolton Bailey]

(does everything you pass to it have to be surrounded by parentheses?)

[Mario Carneiro]

it appears that a query consists of several kinds of things separated by spaces, and one of those things is a pattern (parsed at max prec)

[Mario Carneiro]

I think it would be better to use commas or something as a separator

[Joachim Breitner]

The syntax currently optimizes for “give me all things mentioning the following constants”, e.g.

[Joachim Breitner]

@loogle Real.sin Real.cos

[loogle]

:search: docs#Real.sin_add_two_pi

[Joachim Breitner]

If you want queries to be separated by commas, the above query would be understood as sin applied to cos…
And if you think of @loogle (or #find) as a function, isn’t it natural to parenthesize all its non-atomic arguments?
But happy to bow to popular vote here, it’s just syntax :-)

[Mario Carneiro]

I think that most tactics do not use "function-inspired syntax"

[Mario Carneiro]

e.g. use takes a comma separated list, and exact takes a min-prec term because max-prec would be annoying

[Joachim Breitner]

Right, and rw requires [ ] (why is that by the way). Looks like we haven’t covered the design space completely :D

[Mario Carneiro]

even most term elaborators do not use function-style precedence, e.g. dbg_trace, assert!, return

[Martin Dvořák]

What is "max-prec term" please?

[Joachim Breitner]

@loogle (Real.sin Real.cos)
At least this gives a decent error message instead of just not finding anything

[loogle]

:exclamation: application type mismatch
Real.sin Real.cos
argument
Real.cos
has type
ℝ → ℝ : Type
but is expected to have type
ℝ : Type

[Mario Carneiro]

@Martin Dvořák a term parsed at maximum precedence, meaning it must be surrounded in parentheses if it is not atomic

[Mario Carneiro]

the arguments to a regular function are normally parsed at max prec

[Mario Carneiro]

but e.g. return and exact take a low precedence term which is why return f x is interpreted as return (f x) rather than (return f) x

[Martin Dvořák]

Yeah, I remember exact in Coq was very annoying.

[Joachim Breitner]

Right, but these take _one_ term, then it’s easy to go for min prec.

[Mario Carneiro]

that's why I gave use as an example

[Mario Carneiro]

cases and rcases also take min-prec lists

[Joachim Breitner]

Yeah, maybe commas are fine then. Tangentially: Why does rw not take a comma separated list? I found the […] often annoying, especially when rewriting with just one lemma.

[Mario Carneiro]

in lean 3 the [] were optional if there is only one term; it couldn't take multiple because the comma would conflict

[Mario Carneiro]

in lean 4 the syntax was made more regular, but indeed I think there isn't much need for the brackets

[Mario Carneiro]

it might block out some syntax options though for simp

[Martin Dvořák]

Lean 3's rw foo at bar is my most missed feature in Lean 4.

[Mario Carneiro]

it might read a bit ambiguously when you have at h

[Mario Carneiro]

also, mathlib is ported now, that would be a massive change at this point

[Mario Carneiro]

probably should have brought that up 9 months ago :)

[Joachim Breitner]

So back to #find: Comma separated it is then, or are there dissenting opinions?

[Mario Carneiro]

Bolton Bailey said:

(The "13 more" link gives 502 bad gateway)

Looks like the whole message is being sent to the #find command, even though it seemed to work anyway

[Filippo A. E. Nuccio]

Stupid question: in the Documentation, point 3 says that "The pattern can also be non-linear, as in

#find (Real.sqrt ?a * Real.sqrt ?a)

What is the meaning of "linear" here?

[Mario Carneiro]

https://stackoverflow.com/questions/35891663/what-are-nonlinear-patterns

[Joachim Breitner]

Looks like the whole message is being sent to the #find command, even though it seemed to work anyway

I just fixed a bug there, should work now.

[Joachim Breitner]

The #find PR now uses commas. I agree it's nicer. The loogle service will catch up eventually.

[Scott Morrison]

@Joachim Breitner, I'm not sure whether we should merge the PR yet; it seems like we're still shaking out. If you think it's better to have it in though, just say so and I'll prioritize it.

[Joachim Breitner]

I doubt we'll find all infelicities of the pattern matcher without giving it into the hands of the users. OTOH, we can test it using loogle, so merging isn't urgent.

I guess I'd be grateful to know if it could be merged as is, i.e. have it reviewed. We can then still let it sit and ripe a bit if that's desirable. In any case I'm waiting for the next std4 bump.

[Scott Morrison]

The KMP bump is with bors now, and I left some minor comments on the #find PR. I'll delegate now, as I think it's good enough, and clearly we will iterate further on this.

[Damiano Testa]

Joachim Breitner said:

(You can also use private messages.)

I tried this out messaging myself, but I was not able to work. I copied the example
@loogle (Real.sin Real.cos)
in a message to myself, but got no reply, not even an error message.

[loogle]

:exclamation: <input>:1:1: expected term

[Eric Rodriguez]

you have to PM the loogle bot itself

[Damiano Testa]

Isn't that what @loogle does there?

[Eric Rodriguez]

image.png

[Eric Rodriguez]

no that's just tagging it

[Eric Rodriguez]

it doesn't work in PMs I don't think

[Damiano Testa]

I feel like I am about to learn something new... how do I PM the bot?

[Damiano Testa]

(Also, at least on this stream I got a reply from loogle.)

[Eric Rodriguez]

image.png

[Scott Morrison]

@Damiano Testa, if in this stream you find a place where loogle has replied, and click on its name, a pop-up appears, in which you can select "view direct messages". That will take you to your own private conversation with loogle.

[Damiano Testa]

Scott, Eric, thanks! I have now started a conversation with loogle! :robot:
@loogle AlgebraicGeometry.Scheme

[Damiano Testa]

@loogle AlgebraicGeometry.Scheme

[loogle]

:search: docs#AlgebraicGeometry.IsAffine, docs#AlgebraicGeometry.IsAffineOpen, and 198 more

[Damiano Testa]

Ok, I got it now! Sorry about being so slow in figuring out how this works!

[Martin Dvořák]

I can confirm that @loogle replies to my PMs and provides useful answers!

[Scott Morrison]

I feel like we should all agree to do our loogling in public somewhere, just so everyone can see how awesome it is, rather than hiding away in DMs. :-)

[Arthur Paulino]

Public queries are also didactic. People learn just by looking at them (and their result)

[Damiano Testa]

Sure, but I'm preparing a talk and might be loogling around quite a bit...

[Damiano Testa]

Maybe we could have a loogle stream of conscience?

[Arthur Paulino]

I'd suggest a loogle thread in #mathlib4, since it's querying about mathlib code

[Mario Carneiro]

#Is there code for X? seems more appropriate

[Mario Carneiro]

we just need a bot which reads each new topic on the stream and asks chatgpt to construct a loogle query

[Arthur Paulino]

Just in case you're not joking (I'm worse than computers at noticing these things :upside_down:), I doubt chatgpt knows about loogle syntax :robot:

[Mario Carneiro]

well you would explain the syntax in the prompt

[Mario Carneiro]

it's a half joke, I think it would probably work fairly well

[Arthur Paulino]

The gray area of half jokes!
I think that would be at the very least entertaining to watch. The bot can simply not post if loogle returns "invalid syntax"

[Martin Dvořák]

Will you design a ChatGPT pre-prompt for loogling?

[Joachim Breitner]

Damiano Testa said:

Sure, but I'm preparing a talk and might be loogling around quite a bit...

In that case, maybe using https://loogle.lean-fro.org/ is more ergonomic?

[Damiano Testa]

Ah, yes! Joachim, you come bearing lots of gifts!

[Julian Berman]

Very very minor website UI feedback -- not having really read the page carefully, I just tried copying the first example that caught my eye, which happened to be #find Real.sin "two", which I pasted in the box and clicked the green button, to be presented with error output saying <input>:1:0: expected end of input.

Obviously when that failed I saw that the "Try these" examples at the top do not have #find in them so I figured out that clearly the #find bit isn't meant to go in the box, but perhaps it's worth making the examples at the bottom have the #find part shown in a way that won't be copied to the clipboard when selected. E.g. in Python land we have https://sphinx-extensions.readthedocs.io/en/latest/sphinx-prompt.html#example for this sort of thing (not exactly the same, for when you have something like a prompt but don't want it to be selectable -- obviously it's just doing some HTML/CSS/JS underlying thing to make that actually happen which I don't know what specifically but could be used). Or you could I guess just trim off a possible #find from the input and ignore it for lazy people like me who don't read, or have a #find shown in front of the box so it's clear that the input is adding that for you. Or...

[Joachim Breitner]

The text is copied from the #find docstring, and I'm too lazy to change it every time (at least while it keeps changing a lot). But trimming #find is a good idea, will do that.

[Joachim Breitner]

Done

[Joachim Breitner]

Loogle now expects comma-separated queries.

[Tomas Skrivan]

I tried searching for doc#Pi.mul_apply with (_ * _) _ which does not work with messageCannot search: No constants in search pattern.. So I tried HMul.hMul _ _ _ but that produces an error

function expected at
  ?m.2793799 * ?m.2793800
term has type
  ?m.2793797

[Mario Carneiro]

@loogle (HMul.hMul _ _ _)

[loogle]

:exclamation:

function expected at
  ?m.2794101 * ?m.2794102
term has type
  ?m.2794099

[Mario Carneiro]

wait a minute, mul doesn't have that many arguments

[Mario Carneiro]

@loogle (HMul.hMul _ _)

[loogle]

Failure! Bot is unavailable

[Mario Carneiro]

I suspect there were too many results

[Mario Carneiro]

I think it should truncate after, say, 500 results, as after that you have to start searching the search results

[Mario Carneiro]

Oh, I realize I misinterpreted @Tomas Skrivan 's query, the overapplication of mul is the point

[Mario Carneiro]

@loogle HMul.hMul (γ := ∀ (_ : (_ : Type _)), (_ : Type _)) _ _ _

[loogle]

:search: docs#inner_matrix_col_col, docs#inner_matrix_row_row, and 57 more

[Joachim Breitner]

https://loogle.lean-fro.org/?q=%28_+*+_%29 works just about reasonably fast, but seems to just miss zulip's bot timeout.

[Michael Stoll]

@loogle (Nat -> ZMod _)

[Joachim Breitner]

@loogle Nat -> ZMod _

[loogle]

:shrug: nothing found

[Michael Stoll]

@loogle Nat |- ZMod _

[loogle]

:exclamation: <input>:1:4: expected end of input

[Adam Topaz]

@loogle System.FilePath |- IO Bool

[Adam Topaz]

@loogle System.FilePath |- IO Bool

[loogle]

:exclamation: <input>:1:16: expected end of input

[Adam Topaz]

@loogle System.FilePath |- (IO Bool)

[loogle]

:exclamation: <input>:1:16: expected end of input

[Adam Topaz]

Is it the dependent type that's causing issues?

[Jireh Loreaux]

I think it's suppose to be:
@loogle System.FilePath, ⊢ IO Bool

[loogle]

:exclamation: <input>:1:23: expected end of input

[Jireh Loreaux]

@loogle System.FilePath, ⊢ IO Bool

[loogle]

:shrug: nothing found

[Adam Topaz]

hmmm... ok

[Jireh Loreaux]

It was recently changed so that it takes a comma separated list of arguments.

[Michael Stoll]

@loogle Nat, |- ZMod _

[loogle]

:search: docs#LucasLehmer.lucasLehmerResidue, docs#LucasLehmer.sZMod, and 2 more

[Michael Stoll]

I would have expected something like Nat.cast to show up, but maybe it doesn't, because Nat.cast has a more general type? docs#Nat.cast

[Adam Topaz]

Jireh Loreaux said:

It was recently changed so that it takes a comma separated list of arguments.

I see, but presumably it should be considered a (minor) bug that a comma is required for the last element of the list!

[Jireh Loreaux]

why?

[Adam Topaz]

We don’t write [a, b, c,]…

[Jireh Loreaux]

Okay, but I didn't write System.Path, ⊢ IO Bool, ...., so?

[Adam Topaz]

Oh I’m talking about the stuff before the turnstile

[Jireh Loreaux]

Right, but it's all one list. And the "stuff before the turnstile" doesn't all have to appear before the turnstile.

[Jireh Loreaux]

@loogle ⊢ IO Bool, System.FilePath

[loogle]

:shrug: nothing found

[Jireh Loreaux]

also that :up:

[Adam Topaz]

The turnstile could be considered a separator

[Jireh Loreaux]

I'm not sure how things would parse with that anymore. What does a, b ⊢ c, d mean?

[Adam Topaz]

I’m claiming that it should be equivalent to a, b, |- c, d, whatever that’s supposed to mean

[Jireh Loreaux]

Using the turnstile as an alternative separator seems to make parsing ripe for misinterpretation (by humans), but that's just my opinion.

[Joachim Breitner]

The syntax isn't great: the turnstile is a marker to use the different interpretation for the type (with ->) afterwards

[Joachim Breitner]

Open for suggestions for better syntax. Or maybe it should just for simplicity always match function types up to order of premises, anywhere in the definition's type. Then we wouldn't need the extra syntax

[Kyle Miller]

Here's an option:

/-- The turnstyle for conclusion patterns, unicode or ascii allowed -/
syntax turnstyle := patternIgnore("⊢ " <|> "|- ")

/-- `#find` patterns -/
syntax find_patterns := term,* (turnstyle term)?

Then you could write a, b |- c or a, b. It seems clearer to require that the conclusion come at the end than to allow it to appear anywhere, though maybe there's sub subtlety I'm missing.

Could you say a little bit about why find_patterns is a syntax category in the PR? I don't really understand "so that it can be used by external tools".

[Joachim Breitner]

Right now the commas separate independent filters or predicates. “patterns” in the name above is misleading: filters can be

• names of constants
• substrings of definition names
• term patterns matching anywhere
• term patterns matching on the top level up order .

I'd prefer to keep this top-level “list of filters”, also to extend it easily later by new filters (e.g. “in library std4” or other stuff).

So within commas we can have a term patterns. The meaning of this term patterns can vary along two axes:

• whether it should match the whole definition type, or anywhere therin
• whether a function type patterns should match as is (defEq) or up to reordering or extra assumptions
  The current implementation defaults to “defEq anywhere ”, prefixing the pattern with a turnstile changes both axes “up to reordering, only top-level”.

I am inclined to always match up to reordering, and always anywhere. No need to learn about turnstile or other special syntax etc..

This is the most permissive, and will give you the results. As long as there are only few cases where you really need to narrow it down in the search, this seems the best option, and seems to match what users so far seem to expect

[Michael Stoll]

@loogle Nat, ZMod _

[loogle]

:search: docs#Gamma0Map, docs#Gamma0_det, and 198 more

[Damiano Testa]

Is there a way to further refine a search by excluding declarations that match something? I'm thinking of grep -v.

[Joachim Breitner]

Not yet. I wonder how often that will be useful, compared to refining the search with other constants that must be mentioned and with definition name substrings

[Joachim Breitner]

OTOH its not hard to implement, so if there is intuitive syntax for it (I guess a prefix modifiers before the filter in the comma separated list), and the request comes more often, we can certainly do it.

[Damiano Testa]

A prefix, like -?

[Joachim Breitner]

Sure, as long as it’s unlikely to clash with something you’d start a term with. (You can still parenthesize the term if needed, I think)
But let’s hold off until it itches a bit more often, ok?

[Damiano Testa]

For an example, I'm looking at the output of Michael's query Nat, ZMod _ and I would expect to find a few hits where the only types appearing at Nat and ZMod, and after that, widening the search to including more type. So, maybe, simply sorting by "optimality" might be enough.

[Damiano Testa]

Sure, I'm not in a hurry to have this feature!

[Joachim Breitner]

Hmm, “only these types” is an interesting concept! Although that can maybe be solved by better sorting. Once I figure out I’d like to sort things early that are defined earlier in the dependency tree (so more likely more fundamental). But sorting by “fewer mentioned constants” is also a neat idea

[Joachim Breitner]

One issue with the query Nat, ZMod _ is that it matches every use of ZMod _, because the argument of ZMod _ is always a Nat

[Damiano Testa]

Earlier in the import sense is a good concept, I agree, but I think that if you asked a human to mention a result involving a Nat and ZMod, they would not begin by talking about Gamma0.

[Joachim Breitner]

That’s what I am saying … the code doesn’t do this earlier-import-logic yet :-)

[Damiano Testa]

ZMod is probably too generic, I agree, and I am not exactly sure how to describe the results that I would prefer to find.

[Damiano Testa]

I'll try to find a better (algorithmic) description of an ordering on declarations that might fit better what I would expect.

[Damiano Testa]

Maybe simply sorting by number of distinct constants appearing in the declaration? :shrug:

[Joachim Breitner]

That would certainly move basic stuff to the top!

[Damiano Testa]

Anyway, alphabetical is a good option as well, since you might know how the name starts and "clever sorting" breaks this. I guess just having the option to choose in each situation would be good. But already having one option is great!

[Joachim Breitner]

If you know how the name starts (or ends), add it to the filter!

[Joachim Breitner]

@loogle _ + _, "comm"

[loogle]

:search: docs#CHSH_inequality_of_comm, docs#add_add_add_comm, and 109 more

[Damiano Testa]

So, add_comm is high up! However, the actual "I'm feeling lucky" result I would not have guessed... ever! :smile:

[Damiano Testa]

@loogle _ * _, "comm"

[loogle]

:search: docs#CHSH_inequality_of_comm, docs#card_comm_eq_card_conjClasses_mul_card, and 198 more

[Damiano Testa]

It seems that the add hits were high because of alphabetical order.

[Henrik Böving]

We could run pagerank on the graph of declarations and their bodies to get relevancy results :D

[Damiano Testa]

Is that an option?

[Henrik Böving]

in principle sure. I guess it would drastically increase build times of the index since you need to traverse every expression though. It might also favor type class instances a lot since they appear quite often so you'd have to be at least a bit clever about it.

[Damiano Testa]

Anyway, I agree with what was said: let's play a bit with this tool, before planning an improvement!

[Joachim Breitner]

At least for loogle the index is precomputed, so it wouldn’t be too bad. For #find (without some global cache) it might be less attracktive…

[Joachim Breitner]

Yeah, first someone™ ought to track down the known bugs… (https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/meta.20variable.20confusion/near/387836968)

[Kyle Miller]

Henrik Böving said:

We could run pagerank on the graph of declarations and their bodies to get relevancy results :D

I've thought about this too, but an unfortunate property of declarations is that they form a DAG, so pagerank will very very heavily weight axioms, constructors, and recursors!

I wonder if making the edges bidirectional would give anything sensible.

[Joachim Breitner]

Just deployed a new version of loogle:

• Fixed a bug, so now List.map is found.
• As part of the bug fix, a → b → c patterns are now always matched up to reordering of parameters/premises, with |- or without (the |- now just says that the pattern has to match the definition’s type at the root, not just anywhere within.
• Someone asked for the links to point directly to the right module, this should now happen. Also, https://loogle.lean-fro.org/ shows the defining module next to the results.
• Results are now sorted by the dependency order of their defining module, to bring the most basic lemmas to the top

[Joachim Breitner]

@loogle (?a -> ?b) -> List ?a -> List ?b

[loogle]

:search: List.map, List.mapTR, and 12 more

[Joachim Breitner]

New feature: You can now run queries that contain only lemma name fragments:

[Joachim Breitner]

@loogle "sin", "convex"

[loogle]

:search: convex_singleton, Set.Subsingleton.convex, and 7 more

[Johan Commelin]

Notably, mathlib doesn't seem to have convexity results about the restriction of Real.sin to a suitable interval :bulb:

[Yaël Dillies]

That should be obvious from the second derivative result

[Joachim Breitner]

New feature: https://loogle.lean-fro.org/ shows the 10 most recent queries. This is mostly because I am curious how loogle is being used. Don’t search for your credit card number!

(I removed that feature again due to healthy paranoia; better stateless than sorry.)

[Joachim Breitner]

@Scott Morrison writes

(@Joachim Breitner, it seems you can't say anything to loogle before the mention? Could that be fixed?)

Sure thing, fixed. I hope @loogle "agrees"

[loogle]

:search: CategoryTheory.Presieve.extend_agrees

[Joachim Breitner]

New feature: If you pass a name (like sin) where you so far need to qualify it (Real.sin), it now prints:

unknown identifier sin, using Float.sin instead. (Other candiates: Complex.sin, Real.sin, Real.Angle.sin, Measurable.sin, ContDiff.sin, ContDiffAt.sin, ContDiffOn.sin, ContDiffWithinAt.sin, Differentiable.sin, DifferentiableAt.sin, DifferentiableOn.sin, DifferentiableWithinAt.sin, HasDerivAt.sin, HasDerivWithinAt.sin, HasFDerivAt.sin, HasFDerivWithinAt.sin, HasStrictDerivAt.sin, HasStrictFDerivAt.sin and PowerSeries.sin)
Found 0 definitions mentioning Float.sin.

Probably needs refinement.
The list can get rather long (e.g. with https://loogle.lean-fro.org/?q=Name), and the bot wouldn’t even tell you which constant it picked:
@loogle sin

(And I know about the candiates typo…)

[loogle]

:shrug: nothing found

[Joachim Breitner]

Here is a possible refinement: Instead of blindly picking _one_ possible name, and running the query, #find now gives the error message as usual, but also prints a list of possible #find queries that have a higher chance of succeeding. This is how it looks like in VSCode:

sin.png

It’s clickable in the InfoView, just like the usual try features, and will be prettier once we have tryThese (std4#215).
I’ll now make the web view show these hints as clickable hints as well.
And not sure what the chat bot should do… maybe give the first two suggestions, as links to the website.

[Joachim Breitner]

Now also on the website:

sin.png

and in the bot:
@loogle Name, String

[loogle]

:exclamation: unknown identifier 'Name'
Did you mean Lean.Name, String or something else?

[Joachim Breitner]

Ok, I found a way to generate these suggestions even when the unresolved identifier occurs somewhere in a term pattern:
@loogle replicate (_ + _) _
The implementation is a bit hacky (it runs the term elaborator, catches the exception, takes the SourceInfo from the exception, looks in the Syntax to see if there is an ident there, generates the list of possible Names, changes the Syntax and pretty-prints it), but whatever works. Maybe users will get so used to have sensible replacement suggestions when using underqualified name that eventually the elaborator supports this natively :-)

[loogle]

:exclamation: unknown identifier 'replicate'
Did you mean List.replicate (_ + _) _ or something else?

[Eric Rodriguez]

@Joachim Breitner , small bug report:
image.png

Firefox offers to translate Loogle! Maybe a better offer than german to english is lean to maths ;b

[Joachim Breitner]

:printer: & :spaghetti:, thanks for reporting!
Should be fixed now.

[Joachim Breitner]

Loogle now lives at https://loogle.lean-lang.org/. The old URLs will forward (for now).

[Joachim Breitner]

Since the “Try these” support for multiple suggestions hit mathlib I was inspired to make loogle suggest even more possible fixes. When you now do a search that looks like you are searching for an identifier, but that identifier doesn't exist, it will suggest putting quotes around it, so that you search for names (in addition to suggesting possible qualified names):
@loogle Name

[loogle]

:exclamation: unknown identifier 'Name'
Did you mean "Name" or something else?

[Joachim Breitner]

And now showing the first two suggestions in the bot reponse, for 100% more suggestions
@loogle name

[loogle]

:exclamation: unknown identifier 'name'
Did you mean "name", Lean.Name, or something else?

[Joachim Breitner]

The Loogle website now displays types for all hits (the zulip bot and the CLI don’t, and the JSON API includes types and docstrings).

[Joachim Breitner]

Finally found the bug that prevented queries with placeholders in the conclusion:
@loogle List ?a -> Fin _ -> ?a

[loogle]

:search: List.get

[Notification Bot]

6 messages were moved from this topic to #general > Loogle and iff_of_eq by Joachim Breitner.

[Joachim Breitner]

More lean news:
I added a shortcut to my browser that l <query> sends that query to loogle. With this, I found Loogle to be useful even for searching for things that I know of, because of the convenient link to the docs and the type information. So I made two further tweaks:

When searching for a plain identifier, it will include that identifier in the result list:
@loogle Real.sin

Furthermore, there is a “I’m feeling lucky” mode where loogle will send you directly to the docs of the first hit. You can use that mode with the #lucky button, or by adding &lucky=yes to the URL.

I have added a browser shortcut for that as well, so I can now enter ll Real.sin to the search bar, and a moment later I see docs#Real.sin. And it works with partial queries as well (ll "Name" sends me to docs#Lean.Name).

[loogle]

:search: Real.sin, Complex.ofReal_sin, and 228 more

[Eric Rodriguez]

Could we add loogle to duckduckgo? :)

[Joachim Breitner]

Sure, just do it :-) :duck:

[Eric Rodriguez]

I've submitted :) not sure if they encourage many/few people to suggest it!