How to use the #find tactic from Loogle in a custom project?

Stream: general

[Michael Sammler]

I learned from #general > BetterFind.lean - a better way to find theorems in Lean @ 💬 that #loogle provides a #find tactic, which looks like exactly the tactic I have been looking for for quite some time. However, I am struggling to use it in my project that does not depend on Mathlib. I tried adding the following to my lakefile.toml:

[[require]]
name = "loogle"
scope = "nomeata"
version = "git#master"

and then adding import Loogle.Find, but this causes weird build errors in batteries and Qq since my project is using leanprover/lean4:v4.21.0, but loogle master is using leanprover/lean4:v4.20.0-rc5. Also it tries to download mathlib, which I do not need. How can I get access to the #find tactic for my project?

[Joachim Breitner]

The code is there, but convenient integration into downstream projects is still pending, so so far this is mostly for early adopters who'll working around these issues and thus help finding a good way of setting this up.

Eventually I'm hoping that lake comes with support for “local dev dependencies” that allow you to add tools like loogle to your local setup without disturbing your projects dependcy resolution and without having to touch committed files.

Does it help to move the loogle require up or down in your lake file?

[Eric Wieser]

In the meantime should mathlib just depend on loogle, or does that put us in a mess WRT the loogle cache?

[Eric Wieser]

Also it tries to download mathlib, which I do not need.

Does it download the olean cache or just the source files? I'd argue you should just ignore the fact it downloads mathlib, but if it's slow doing so then that's something we should try to fix in lake

[Joachim Breitner]

Eric Wieser schrieb:

In the meantime should mathlib just depend on loogle, or does that put us in a mess WRT the loogle cache?

We can make that work, if there is demand. You still would have to do manual steps to get a local cache, and re-run to update it (or else just wait for a while when you use #find the first time per module).

[Eric Wieser]

Could the loogle cache be part of the mathlib cache?

[Joachim Breitner]

Michael could experiment with a branch of loogle without the mathlib dependency there (which shouldn't really be there)

[Joachim Breitner]

Possibly, but that would require a bit more thought. What if the downstream user uses mathlib as a dependency and wants to find their definitions as well? What about local changes? When to update the cache?

[Kenny Lau]

hot take: loogle should be in core?

[Michael Sammler]

Joachim Breitner said:

Does it help to move the loogle require up or down in your lake file?

I did not know that the order in the lakefile matters. I can try it, but my only other dependency is Qq, so I am not sure what difference to expect.

Joachim Breitner said:

Eventually I'm hoping that lake comes with support for “local dev dependencies” that allow you to add tools like loogle to your local setup without disturbing your projects dependcy resolution and without having to touch committed files.

That would be very nice!

Eric Wieser said:

Does it download the olean cache or just the source files? I'd argue you should just ignore the fact it downloads mathlib, but if it's slow doing so then that's something we should try to fix in lake

It tries to download the cache I think and then fails because of the toolchain mismatch.

[Michael Sammler]

Kenny Lau said:

hot take: loogle should be in core?

I would actually second this. In Rocq, there is the built-in Search command that is very similar to #find and I am using it a lot in large developments to find relevant lemmas. I find that this is really core functionality that Lean is currently missing compared to Rocq.

[Joachim Breitner]

Before it can be in core I think there are a few questions to be solved around the index (when to generate and update). At least if you want to be able to search in the whole project, and not just the imports of the file you currently have open.

Maybe for that reason even for local use it should maybe be a separate process/server that you can use using the browser, the VSCode integration and the #loogle client?

[Robin Carlier]

Eric Wieser said:

In the meantime should mathlib just depend on loogle, or does that put us in a mess WRT the loogle cache?

please, no more mathlib lakefile bloat!

[Robin Carlier]

Joachim Breitner said:

Eventually I'm hoping that lake comes with support for “local dev dependencies” that allow you to add tools like loogle to your local setup without disturbing your projects dependcy resolution and without having to touch committed files.

I second that this would be a nice (and in fact, essential) thing to have. Are there discussions in Core/FRO to make this happens at some point? this is not in this year’s roadmap afaict...

[Michael Sammler]

Joachim Breitner said:

Before it can be in core I think there are a few questions to be solved around the index (when to generate and update). At least if you want to be able to search in the whole project, and not just the imports of the file you currently have open.

Searching the whole project would be nice, but Search in Rocq only works on the currently imported files and that is already very useful. So I personally would also be happy with a simpler version that just works with the currently imported files.

[Joachim Breitner]

Right - but it needs to be possible to develop and use such tools without waiting for core :-)