Zulip Chat Archive

Stream: mathlib4

Topic: Loogle offline

Andrew Yang (May 02 2025 at 22:44):

How do I run loogle offline? (or an alternative: when will there be internet access on the London tube?)

Andrew Yang (May 02 2025 at 22:45):

@Eric Wieser :thank_you:

Aaron Liu (May 02 2025 at 22:52):

https://github.com/nomeata/loogle

Andrew Yang (May 02 2025 at 22:53):

Can I configure the vscode plugin to use this instead of requesting a server?

Aaron Liu (May 02 2025 at 22:54):

There's a section that says

Running locally

To use loogle locally:

  1. check out this repository
  2. install elan
  3. run lake exe cache get
  4. run lake exe loogle --help (or other options)

If you use loogle on a large repository like Mathlib, the startup-time will
be rather large. Run lake build LoogleMathlibCache if you want to pre-compute
the index for Mathlib.

[elan]: https://github.com/leanprover/elan

Eric Wieser (May 03 2025 at 00:05):

I don't think you need the plug-in, you can just import it and write #find

Andrew Yang (May 03 2025 at 00:11):

I don't think they are the same thing? #find is never usable to me; even a simple #find AlgebraicGeometry.IsProper times out for me.

Eric Wieser (May 03 2025 at 00:12):

Loogle overrides it I think (edit: yes)

Andrew Yang (May 03 2025 at 00:12):

Oh you mean installing loogle and import it?

Eric Wieser (May 03 2025 at 00:13):

Where "install" probably means "add to lakefile"

Eric Wieser (May 03 2025 at 00:13):

Or if you're in mathlib, clone loogle, point it at your mathlib, and create a dummy file in the loogle directory

Robin Carlier (May 04 2025 at 06:59):

Related: I recently opened an issue at LeanSearchClient so that they'd make it possible to override hardcoded URLs via environment variables. If they make it happen, you'd also be able to use your offline/local loogle instance with #loogle.

Antoine Chambert-Loir (Jun 08 2025 at 16:28):

I just tried to install loogle (git clone…, lake build LoogleMathlibCache), but I get an error message “[INFO] LOOGLE_SECCOMP is not set” when I run lake exe loogle.

Antoine Chambert-Loir (Jun 08 2025 at 16:30):

What I would try to do is to be able to use loogle either as command-line function, or especially when I'm offline, via #loogle in nvim…

Eric Wieser (Jun 08 2025 at 16:57):

Is it an error or just an info message?

Antoine Chambert-Loir (Jun 08 2025 at 17:24):

Indeed, an info.

Antoine Chambert-Loir (Jun 08 2025 at 17:28):

Unclear, in fact, because it's quite slow.

$ time lake exe loogle "IsUnit, ZMod"
lake exe loogle "IsUnit, ZMod"  30,05s user 1,66s system 98% cpu 32,199 total

Antoine Chambert-Loir (Jun 08 2025 at 17:29):

A related question: this works from within the loogle directory, but not otherwise, and I don't have a loogle executable program as the Loogle website suggests there could be.

Eric Wieser (Jun 08 2025 at 17:52):

If you import loogle then you should be able to use #find

Eric Wieser (Jun 08 2025 at 17:52):

That should also be cached and so much faster after the first use

Jz Pan (Jun 08 2025 at 18:39):

How large is the index file for whole Mathlib?

Shreyas Srinivas (Jun 08 2025 at 21:32):

Andrew Yang said:

How do I run loogle offline? (or an alternative: when will there be internet access on the London tube?)

Which extension do you mean?

Kevin Buzzard (Jun 09 2025 at 04:02):

Andrew Yang said:

How do I run loogle offline? (or an alternative: when will there be internet access on the London tube?)

Internet access on London tube is now a thing! There's 5G on the underground (at least on Piccadilly and Victoria lines) as of a few days ago

Last updated: Dec 20 2025 at 21:32 UTC