Find the module which contains a lemma

Stream: general

[Eric Wieser]

Let's say I remember the name of a lemma/def/structure/..., but not the file I need to import to get it.

Does vs-code have any automation to find and add the imports for me?

[Mario Carneiro]

No. Unfortunately vscode is limited by what lean knows, and lean doesn't know about any files that are not imported

[Eric Wieser]

Could such a database be shipped alongside the mathlib oleans?

[Kevin Buzzard]

I just search; VS Code does have pretty good search, and there are tricks (like searching for exact words etc).

[Kevin Buzzard]

Of course there's also the docs. If you want to want to find real.exp you can do docs#real.exp and then see where the link leads. Rob explained a way of doing this within a browser, where you don't even have to spam zulip.

[Mario Carneiro]

It should be possible to rig up a search using olean-rs to quickly process the olean files without compiling everything

[Eric Wieser]

Kevin Buzzard said:

Of course there's also the docs. If you want to want to find real.exp you can do docs#real.exp and then see where the link leads. Rob explained a way of doing this within a browser, where you don't even have to spam zulip.

I've used this approach before in private messages with welcome bot

[Kevin Buzzard]

(as everyone knows, real.exp is in data.complex.exponential ;-) )

[Mario Carneiro]

Unfortunately this only works if you get the name and namespace exactly right, which in practice usually means you already know what it is

[Mario Carneiro]

for definitions like real.exp that's not so bad but for theorems you usually want some amount of autocomplete to get the name right

[Gabriel Ebner]

docs#exp does something useful btw

[Mario Carneiro]

oh nice, I hadn't thought of using the 404 for this

[Scott Morrison]

I'm confused. How is that helpful? I just land at a 404 that says "Please wait a second. I'll try to help you.", but then nothing happens.

[Mario Carneiro]

it took about 3 seconds for me

[Scott Morrison]

Still nothing for me (chrome on macos).

[Kevin Buzzard]

docs#z

[Utensil Song]

Nothing happens for me too, only seeing "Please wait a second. I'll try to help you."

[Utensil Song]

(Chrome on Windows)

[Gabriel Ebner]

Ah, should've tested in chromium. "please wait a minute"

[Scott Morrison]

I see "exp:45 Uncaught TypeError: window.location.href.replaceAll is not a function
at exp:45" in the javascript console.

[Kevin Buzzard]

On Ubuntu works for me on firefox and not on Chrome

[Utensil Song]

image.png

[Gabriel Ebner]

As of August 2020 the replaceAll() method is supported by Firefox but not by Chrome. It will become available in Chrome 85.

[Gabriel Ebner]

I just pushed a fix, should be online in a few minutes.

[Eric Wieser]

I now get a different problem "Uncaught (in promise) ReferenceError: declSearch is not defined"

[Eric Wieser]

image.png

[Anatole Dedecker]

Ubuntu Chromium does seem to work now

[Ruben Van de Velde]

It seems like the code is assuming nav.js is loaded when setTimeout calls the callback; I don't suppose that's guaranteed.

[Anatole Dedecker]

Quite a lot slower than in Firefox though

[Gabriel Ebner]

Moved into nav.js.

[Eric Wieser]

Works now, thanks (although rather slowly)

[Utensil Song]

Works beautifully, thanks! Combining this with the trick of setting this as a search engine with a prefix of "ml", docs#z is just "ml z" for me in the browser.

[Chris Wong]

I wonder if it's worth adopting JavaScript modules here. That would solve the problem of files being loaded in the wrong order.