loogle for other versions of mathlib

Stream: general

[Patrick Massot]

I think this is indeed an issue that should get fixed. @Henrik Böving did you consider having a frozen loogle for each monthly release Mathlib tag?

[Henrik Böving]

I do not own loogle that's @Joachim Breitner, coincidentally the FRO started talking about something like this just this morning though ^^

[Shreyas Srinivas]

Once it lands, the extensions on vscode and nvim will need to be updated

[Shreyas Srinivas]

I am guessing there will be a change in the URL routes for getting the json.

[Joachim Breitner]

Loogle isn't particularly cheap to run, it’s a persistent process that has all of Mathlib plus an index mmaped. I don’t have urgent plans to support many different versions.

It would be great if it were easier to run loogle locally; this way you get exactly your stuff, including any libraries you import and whatever changes you have locally. I am sure eventually this will be the case. Until then, loogle tracks mathlib master with a delay of about 6h.

[Joachim Breitner]

That said, it is possible already now, just not super convenient, and I am keen to hear from early adopters who play around with it. Happy to assist.

[Patrick Massot]

I don’t know why I pinged Henrik instead of Joachim, I’m sorry. I did that right before getting lunch, I guess my brain was lacking nutriments.

[Joachim Breitner]

Now worries at all :-)
I like having Henrik as my first-level support ;-)