import `import Mathlib.Tactic` vs `import Mathlib`

Stream: new members

[rzeta0]

I've been trying to create starter minimal examples suitable for beginners like me.

I've been using

import Mathlib.Tactic

but I've noticed several replies to my questions here use

import Mathlib

Question: is import Mathlib more conventional? Is it wasteful because it imports "everything"? What are the pros/cons?

[Daniel Weber]

It usually shouldn't be used as it makes compilation slower, but when writing a short example it can be convenient as you don't need to figure out what imports are actually needed

[Michael Rothgang]

For pedagogical purposes, I'd either try to minimize imports to something reasonable (#min_imports helps with this; perhaps you already heard of this) or just import Mathlib as a sign "this is clearly not minimal".

[Kevin Buzzard]

I sometimes use import Mathlib when replying to questions, when the questioner has not done their job properly i.e. not made an #mwe so I don't know what imports I should be using. It's definitely wasteful, for example it makes exact? take much longer

[Ruben Van de Velde]

On the other hand, sometimes you can state the problem without the imports you need for a (natural) proof

[Adomas Baliuka]

I find it really hard to reason about what needs to be imported to use a certain thing (and sometimes also what import leads to some things being available unexpectedly). You basically have to become familiar with the internal import graph of Mathlib?

If the engineering problems could be solved, it's a much nicer experience to be able to just always use import Mathlib...

[rzeta0]

what does #min_imports do?

my search engine isn't helping...

[Michael Rothgang]

rzeta0 said:

what does #min_imports do?

my search engine isn't helping...

It used to be called #minimize_imports, and was recently renamed. From its docstring.
:

Try to compute a minimal set of imports for this file, by analyzing the declarations.

This must be run at the end of the file, and is not aware of syntax and tactics, so the results will likely need to be adjusted by hand.

[Michael Rothgang]

Adomas Baliuka said:

I find it really hard to reason about what needs to be imported to use a certain thing (and sometimes also what import leads to some things being available unexpectedly). You basically have to become familiar with the internal import graph of Mathlib?

If the engineering problems could be solved, it's a much nicer experience to be able to just always use import Mathlib...

I don't know mathlib's import graph by heart either! A reasonable workflow is "start with import Mathlib, write your code and then use #min_imports to reduce to a reasonable subset". Another (more suitable for working on a mathlib branch) is to gradually add imports as you need them.
If you want to use a certain definition, the API docs (or search in VS Code) will tell you where that is located, so importing that file will do.

[Adomas Baliuka]

Playing around with #min_imports suggests that many files inside Mathlib have unnecessary imports. Should one try to remove those? Is there a reason we don't have a linter for unused imports?

[Ruben Van de Velde]

We do have that linter

[Ruben Van de Velde]

You may be discovering imports that are still imported transitively if you remove the direct import

[Kevin Buzzard]

shake doesn't complain about imports which can be removed because they're importing something which is already there??

[Ruben Van de Velde]

That's correct

[Adomas Baliuka]

Is that desired? Alternatively, would it make any difference (to e.g. performance or docs, etc.) if we remove such unnecessary imports?

[Ruben Van de Velde]

I think it's likely a minimal win on those measures, at the expense of more ci failures