Zulip Chat Archive

Stream: general

Topic: Find the module which contains a lemma


view this post on Zulip Eric Wieser (Aug 05 2020 at 12:25):

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?

view this post on Zulip Mario Carneiro (Aug 05 2020 at 12:31):

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

view this post on Zulip Eric Wieser (Aug 05 2020 at 12:35):

Could such a database be shipped alongside the mathlib oleans?

view this post on Zulip Kevin Buzzard (Aug 05 2020 at 12:35):

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

view this post on Zulip Kevin Buzzard (Aug 05 2020 at 12:36):

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.

view this post on Zulip Mario Carneiro (Aug 05 2020 at 12:36):

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

view this post on Zulip Eric Wieser (Aug 05 2020 at 12:36):

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

view this post on Zulip Kevin Buzzard (Aug 05 2020 at 12:37):

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

view this post on Zulip Mario Carneiro (Aug 05 2020 at 12:37):

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

view this post on Zulip Mario Carneiro (Aug 05 2020 at 12:39):

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

view this post on Zulip Gabriel Ebner (Aug 05 2020 at 12:40):

docs#exp does something useful btw

view this post on Zulip Mario Carneiro (Aug 05 2020 at 12:40):

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

view this post on Zulip Scott Morrison (Aug 05 2020 at 12:41):

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.

view this post on Zulip Mario Carneiro (Aug 05 2020 at 12:41):

it took about 3 seconds for me

view this post on Zulip Scott Morrison (Aug 05 2020 at 12:42):

Still nothing for me (chrome on macos).

view this post on Zulip Kevin Buzzard (Aug 05 2020 at 12:42):

docs#z

view this post on Zulip Utensil Song (Aug 05 2020 at 12:42):

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

view this post on Zulip Utensil Song (Aug 05 2020 at 12:43):

(Chrome on Windows)

view this post on Zulip Gabriel Ebner (Aug 05 2020 at 12:43):

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

view this post on Zulip Scott Morrison (Aug 05 2020 at 12:43):

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

view this post on Zulip Kevin Buzzard (Aug 05 2020 at 12:43):

On Ubuntu works for me on firefox and not on Chrome

view this post on Zulip Utensil Song (Aug 05 2020 at 12:43):

image.png

view this post on Zulip Gabriel Ebner (Aug 05 2020 at 12:45):

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

view this post on Zulip Gabriel Ebner (Aug 05 2020 at 12:46):

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

view this post on Zulip Eric Wieser (Aug 05 2020 at 13:03):

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

view this post on Zulip Eric Wieser (Aug 05 2020 at 13:03):

image.png

view this post on Zulip Anatole Dedecker (Aug 05 2020 at 13:07):

Ubuntu Chromium does seem to work now

view this post on Zulip Ruben Van de Velde (Aug 05 2020 at 13:09):

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

view this post on Zulip Anatole Dedecker (Aug 05 2020 at 13:10):

Quite a lot slower than in Firefox though

view this post on Zulip Gabriel Ebner (Aug 05 2020 at 13:13):

Moved into nav.js.

view this post on Zulip Eric Wieser (Aug 05 2020 at 13:27):

Works now, thanks (although rather slowly)

view this post on Zulip Utensil Song (Aug 05 2020 at 13:31):

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.

view this post on Zulip Chris Wong (Aug 06 2020 at 09:57):

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


Last updated: May 08 2021 at 19:11 UTC