not going crazy without using import Mathlib

Stream: new members

[Luigi Massacci]

I just realized I don't really know how to do the following: suppose I'm working mid-way through Mathlib (in my case Mathlib.Analysis.Stuff.Stuff) and need some trivial instance (eg: NontrivallyNormedField ℂ), that I cannot synthesize with the current imports ; how do people find out what to import quickly? It's been driving me insane for the last 15 minutes.

So far I've either been working on my own/new files and could just import Mathlib while working, or sufficiently close to the leaves that I guess nearly everything was already imported.

[Michael Rothgang]

Can you import Mathlib temporarily and (when that fixes your problem) use #min_imports to trim down your imports again?

[Johan Commelin]

You can just put import Mathlib at the top of the file.

And then put #min_imports at the bottom, when you are done.

[Michael Rothgang]

Or is the issue that import Mathlib won't work as-is since you'd need to recompile downstream files first?

[Michael Rothgang]

(For that case: if you can quickly isolate an MWE, you can use the playground to minimise imports for you.)

[Luigi Massacci]

Michael Rothgang said:

Can you import Mathlib temporarily and (when that fixes your problem) use #min_imports to trim down your imports again?

[accidentally deleted my message while trying to quote the right message from Michael, I asked if that wouldn't require deleting my file from Mathlib.lean and thus rebuilding everything]

[Damiano Testa]

If I find myself in a situation where I edited a mathlib file, I sometimes open the lean server, copy the entirety of the file there and add import Mathlib at the top.

[Damiano Testa]

(I am assuming that creating a scratch file locally is not a viable option, since you have already compromised the cache.)

[Luigi Massacci]

Ok that sounds workable (and then doing #min_imports I assume)

[Eric Wieser]

Or just do #synth NontrivallyNormedField ℂ in the web editor, then do #check whatItfound, then hover whatItfound to see the module name

[Luigi Massacci]

Eric Wieser said:

Or just do #synth NontrivallyNormedField ℂ in the web editor, then do #check whatItfound, then hover whatItfound to see the module name

That is what I did, but it seemed very suboptimal