Importing mathlib vs importing part of mathlib

Stream: new members

[Ching-Tsun Chou]

When I develop a Lean project that uses mathlib as the background mathematical theory, should I simply import Mathlib or find out which parts of mathlib I need and import only them? For the latter option, is there an automatic way to find out what I need?

[Michael Rothgang]

I would strongly recommend the latter: you can use the #min_imports command to find which imports you need. (Put it at the end of the file and replace import Mathlib by what it suggests. Sometimes, imports can be reduced even further, but the output is a reasonable start.)

[Michael Rothgang]

If you need to add an import to an existing file, you can either decide to split your file anyway, or you temporarily add import Mathlib and use #min_imports again.

[Michael Rothgang]

import Mathlib can be useful for prototyping. But if you intend to polish your code further, I'd minimise imports as one of the steps.

[Eric Wieser]

I don't think I'd agree with that; I think until you're contributing to mathlib, precise imports are just going to trip you up.

[Eric Wieser]

Advantages of import Mathlib:

• Your imports won't break when you update lean; Mathlib.Foo moves to Mathlib.Bar all the time, but the top level import never changes
• The theorem / instance / tactic extension you need is guaranteed to be imported, making tactics like simp and norm_num more powerful.

[Eric Wieser]

Disadvantages of import Mathlib:

• exact? is slower (it is seaching more things)
• You might run into notation clashes that mathlib developers had never noticed. If this happens, report them and we'll try to fix them!

[Ruben Van de Velde]

Another disadvantage: it will take longer to start processing your own code

[Eric Wieser]

On a fast system that should only be a few seconds though

[Kevin Buzzard]

Another advantage: if you follow the naming convention then you are less likely to write a theorem or definition which is already there. And whilst exact? is slower, it's also better.

A disadvantage if you're using the blueprint software: the more mathlib you import the longer Ci takes. In fact in practice the CI timing bottleneck for blueprint projects in my experience is the large amount of time it takes to create the essentially unused bespoke mathlib docs which go with it.

[Michael Rothgang]

Counterpoint to one advantage: with module deprecations, renaming files should give you nice warnings that you can patch easily. (You have to still do it, though.)

[Christian Krause]

Another disadvantage (only applies for people with slow internet): If you import only a small part of Mathlib, it is sometimes faster to just build that part than to download the entire cache after updating Mathlib.

[Philippe Duchon]

This looks like, unless you are running on a slow computer, importing the whole of Mathlib is better at least while working on the code. At last, something I'm doing right!

[Ching-Tsun Chou]

I tried import Mathlib on one of my Lean files. "Restart File" does take longer, perhaps by 5 or 6 seconds. Since that doesn't seem excessive, I'll give it a try. I'm using an M1 MacBook Air with 16GB of memory.

[Eric Wieser]

Kevin Buzzard said:

the CI timing bottleneck for blueprint projects in my experience is the large amount of time it takes to create the essentially unused bespoke mathlib docs which go with it.

Use of GitHub caching makes this not relevant, you can cache all the generated mathlib docs.

[Eric Wieser]

LeanAPAP has a compatible setup for this I believe; or at least, I successfully derived a working one from it

[Kevin Buzzard]

The only real lag is when I bump mathlib, which we're doing quite a bit in FLT

[Eric Wieser]

Indeed you're out of luck there unless we start globally publishing a docs cache!