Loogle mathlib version

Stream: lean4

[Eric Wieser]

I note that https://github.com/nomeata/loogle is pointing at leanprover/lean4:v4.10.0-rc2; does this mean it is running with an old Mathlib version, or is the version that loogle builds against independent of the one it indexes?

[Markus Himmel]

At the bottom of loogle.lean-lang.org you can find the git hash of the mathlib that Loogle currently serves. It should be quite recent.

[Eric Wieser]

Is the implication here that the repo I link to can be bumped to 4.13.0rc3 with no changes then? (Edit: yes!)

[Eric Wieser]

Or is there a secret copy of the repo somewhere that is the one actually being served from the web?

[Joachim Breitner]

Not a secret repo, more a secret checkout on the server that then runs lake update regularly. (But then with git a checkout is a repo, so you are at least technically correct)

[Joachim Breitner]

Eric Wieser said:

, or is the version that loogle builds against independent of the one it indexes?

Not independent, they have to be identical, as Loogle loads the oleans.