initial imports

Stream: mathlib4

[Matthew Ballard]

If you want something to be able available for all files in mathlib, is there a particular place to put it so that this happens automatically? If not, what is usually done?

[Eric Wieser]

You mean available in a file with no imports? (for which I think the answer is Init.lean in core)

[Matthew Ballard]

What is at the bottom of the import tree for mathlib? Is there a single root? I tried (not very hard) to get lake exe graph to tell me but failed.

A concrete question is: what imports do I need to set so that Type* is available for all of mathlib? Does placing it in a particular folder or with particular filename help the process?

[Mario Carneiro]

Tactic.Basic is a reasonable place to put that

[Scott Morrison]

We make an effort to import Tactic.Common fairly early on as well, but that is quite a bit later than Tactic.Basic.

[Jon Eugster]

Maybe Mathlib.Lean.Expr.Basic would make even more sense: it's the lowest import of Mathlib.Tactic.Basic and Type/Sort seem to be defined in Lean.Expr. I understood it that Mathlib.Lean._ would loosely mirror Lean._, so that could make sense.
tactics.png

[Mario Carneiro]

I understood it that Mathlib.Lean._ would loosely mirror Lean._, so that could make sense.

It doesn't really; Lean generally has an additional layer of categorization, and also Mathlib.Lean completely ignores dependency issues within the Lean package (such as the distinction between Meta._ and Elab._ things)

[Jireh Loreaux]

Do we want to have an explicit Mathlib.Init.Root file to make the import hierarchy have a single common ancestor? That is, all current files with no Mathlib.* imports would have import Mathlib.Init.Root added.

[Mario Carneiro]

Wouldn't that just be Mathlib.Init?

[Mario Carneiro]

Now that we are post-port, it might be good to clear out the existing Mathlib.Init folder (containing stuff from lean 3 core) and migrate things to their intended locations (either early in mathlib or in std)

[Mario Carneiro]

and then we can repurpose it as a mathlib init folder instead of just "files from core"