Is `import Mathlib` bad?

Stream: new members

[Adomas Baliuka]

Kyle Miller said:

You might also consider importing just the parts of mathlib you need, which helps a bit with reducing the number of instances you need to be aware of. Mathlib developers don't recommend importing all of mathlib in general, even for mathematical applications.

Doing import Mathlib was suggested to me (I think by Kevin Buzzard, although I can't find the message anymore, so maybe it was someone else) when I was failing to find lemmas (with exact?, apply?, rw?, simp?, I assume aesop also only finds imported lemmas).

Is there consensus that doing import Mathlib is not a good idea? It's tricky to import all the things that might have useful lemmas... How does one do this?

[Kevin Buzzard]

If you want tactics to work then import Mathlib.Tactic is a much better idea.

[Adomas Baliuka]

But if I do that, apply? won't find lemmas, or will it? (Did I accuse (not meant as such, of course) you wrongly about import Mathlib? Sorry if I did :)

[Kevin Buzzard]

It will only find the lemmas you have imported (i.e. a huge number of lemmas, if you import Mathlib.Tactic)

[Adomas Baliuka]

How do experienced people decide what to import? Is missing an import something that holds them up sometimes? It it hard to find a set of imports for a new project? Does someone working in a certain field of math eventually settle on using the same imports every time? Or do you decide for each file what imports to use and how?

[Kevin Buzzard]

If your imports are enough to state the theorems you want to work on, you've probably imported enough to have all the necessary lemmas.

[Ruben Van de Velde]

I'm curious what you consider to be bad about importing all of mathlib while working, Kevin. Does it cause issues for you?

[Kevin Buzzard]

I'm fine with importing all of mathlib. Did you mean to address that to Kyle?

[Yaël Dillies]

Personally I import whatever I need to state what I want. Then when I need a lemma that's not imported, I import the file where the lemma lives. But I have an encyclopedic knowledge of the library and never use apply? or exact?. All I use is the online docs.

[Adomas Baliuka]

Could someone move the discussion starting with "import Mathlib yes or no" to a new topic? I think it might help people who later want to read about that exact topic (which surely also comes up often). At the same time it's probably not relevant for people who want to debug coercions. (I'm assuming I don't have permission to move things or at least don't see how)

(Not to derange the discussion again, but this is something I like about StackOverflow (the use of which I've seen discouraged here on Zulip) to complement this style of discussion, because it's much more focused and later readers get a complete high-quality answer instead of piecing together the process where some individual with unique prerequisites and misunderstandings was taught something, which is of course amazing for that individual)

[Mario Carneiro]

(I'm assuming I don't have permission to move things or at least don't see how)

Everyone should have the permission to move threads. Select "move messages" from the "..." next to any post and you can move either the selected message or it and everything after to another thread name in the same stream. (Only moderators can move messages to another stream.)

[Notification Bot]

11 messages were moved here from #new members > Debugging coercions by Adomas Baliuka.

[Alex J. Best]

I would generally import Mathlib while writing something, and then when I'm done try and work out what imports I actually need

[Joachim Breitner]

and work out what imports I actually need

Do you do that work, or does #minimize_imports do it for you?

[Kyle Miller]

I think it's fine doing import Mathlib when testing things out, but projects should avoid import Mathlib because the library as a whole is much less stable than individual parts of the library; there's less testing that, for example, instances between different parts of the library don't conflict in an unpleasant way. Another reason is not so important, but you might also avoid it because if you update Mathlib in your project, then everything that imports Mathlib is sure to need to be recompiled, vs only the parts that import modules that have (transitively) changed.

That said, if you do run into any issues with import Mathlib, please report them! I think it should work, but caveat emptor :smile:

[Alex J. Best]

Joachim Breitner said:

and work out what imports I actually need

Do you do that work, or does #minimize_imports do it for you?

normally I do it by hand, but that is probably a bad habit :wink:

[Filippo A. E. Nuccio]

On the other hand am I right that there is no way to add the whole Mathlibfolder automatically in Mathlib.lean? I mean, I guess this is made automatically by some trick for mathlib, but in a project, I still have the MyProject.lean file that I have to fill by hand each time I create a new file, right? Wouldn't it be great if I could tell just add an import MyProject.* to mean importall files in the folder?

[Alex J. Best]

You can put

  globs := #[.submodules `MyProject]

in the lean_lib of your lakefile, that should add all files to the library without needing to maintain MyProject.lean

[Filippo A. E. Nuccio]

Oh great! You mean that I have to replace

@[default_target]
lean_lib «MyProject» where
  moreLeanArgs := moreLeanArgs
  weakLeanArgs := weakLeanArgs
  -- add any library configuration options here

by

@[default_target]
lean_lib «MyProject» where
  moreLeanArgs := moreLeanArgs
  weakLeanArgs := weakLeanArgs
  globs := #[.submodules `MyProject]
  -- add any library configuration options here

right?

[Alex J. Best]

Yes that should be it

[Filippo A. E. Nuccio]

Yes, great! Thanks.

[Damiano Testa]

There was also this earlier thread, where you could import directly from your file all paths that begin with a certain string.

[Filippo A. E. Nuccio]

Oh, nice! Thanks.