## Stream: general

### Topic: Find the module which contains a lemma

#### 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?

#### 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

#### Eric Wieser (Aug 05 2020 at 12:35):

Could such a database be shipped alongside the mathlib oleans?

#### 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).

#### 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.

#### 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

#### 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

#### Kevin Buzzard (Aug 05 2020 at 12:37):

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

#### 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

#### 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

#### Gabriel Ebner (Aug 05 2020 at 12:40):

docs#exp does something useful btw

#### Mario Carneiro (Aug 05 2020 at 12:40):

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

#### 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.

#### Mario Carneiro (Aug 05 2020 at 12:41):

it took about 3 seconds for me

#### Scott Morrison (Aug 05 2020 at 12:42):

Still nothing for me (chrome on macos).

docs#z

#### 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."

#### Utensil Song (Aug 05 2020 at 12:43):

(Chrome on Windows)

#### Gabriel Ebner (Aug 05 2020 at 12:43):

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

#### 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.

#### Kevin Buzzard (Aug 05 2020 at 12:43):

On Ubuntu works for me on firefox and not on Chrome

image.png

#### 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.

#### Gabriel Ebner (Aug 05 2020 at 12:46):

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

#### Eric Wieser (Aug 05 2020 at 13:03):

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

image.png

#### Anatole Dedecker (Aug 05 2020 at 13:07):

Ubuntu Chromium does seem to work now

#### 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.

#### Anatole Dedecker (Aug 05 2020 at 13:10):

Quite a lot slower than in Firefox though

#### Gabriel Ebner (Aug 05 2020 at 13:13):

Moved into nav.js.

#### Eric Wieser (Aug 05 2020 at 13:27):

Works now, thanks (although rather slowly)

#### 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.

#### 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