What to import in a file?

Stream: new members

[Jeremy Kahn]

So far when I start a new project from start I've just been starting with

import Mathlib

Can this cause problems? Sometimes the files runs slow and exact? keeps timing out.

I tried deleting the global import and importing files one at a time. After a lot of trial and error and searching for definitions and theorems on the Mathlib docs, I was able to get a working collection of imports. In my particular case it was this:

import Mathlib.Data.List.Basic
import Mathlib.Data.List.Sort
import Mathlib.Data.List.Intervals
import Mathlib.Data.Finset.Sort
import Mathlib.NumberTheory.Divisors
import Mathlib.Tactic.Linarith.Frontend

(I was working with the sorted list of divisors). Is there any way to consolidate these imports? For example, I would have thought one could write

import Mathlib.Data

but this does not work.

[Michael Rothgang]

Do you know about #minimize_imports? If you place this at the end of a (compiling) file, it will suggest a minimal set of imports for the file. (These suggestions miss tactics and notation, so sometimes you'll need to add more things - but in my experience, this is often pretty good.)

[Michael Rothgang]

Putting import Mathlib in mathlib files doesn't work (that will create import cycles, I think). In a "scratch file", that's fine in principle (with a few exceptions...). In Lean 3, exact? used to get a lot slower - if I understood correctly, that's much less of an issue in Lean 4.

[Michael Rothgang]

Personally, once I've finished a logical change, I try to minimize imports (reasonably) - but during development, placing an import Mathlib seems like a fine compromise if I don't want to do import hunting.

[Kevin Buzzard]

If the claim is "if I import Mathlib then exact? times out when it worked before" then I suspect that this is a bug; my understanding was that this sort of issue had been fixed now, although obviously the more you import, the more work exact? has to do. I had understood that it was now very good at doing this kind of work now though. Do you have a concrete example? Is this a regression or something which is to be expected?

[Jeremy Kahn]

If it's a bug then it's a Heisenbug--I took a long walk and when I returned to the same file, exact? was working perfectly. It even suggested a highly complex 30-line completion of a simple subgoal. Maybe the lesson is to take more long walks.