data.sigma.default

Stream: mathlib4

[Kevin Buzzard]

On the list of "ready to port" is data.sigma.default, which is a one-line file import data.sigma.basic. Are default files still a thing in Lean 4?

[Scott Morrison]

I'm inclined to suggest that we just remove all our .default files from mathlib3 anyway.

[Jireh Loreaux]

To reduce unnecessary imports?

[Yaël Dillies]

Yes, and because they are abused.

[Yaël Dillies]

For example in the category theory library, .default files are used as normal files, to avoid writing .basicin the imports.

[Yaël Dillies]

They also mess up doc-gen, as doc-gen only records files with declarations, meaning that dependencies that go through a .default file get forgotten.

[Jireh Loreaux]

Scott, is there any chance these .default imports were abolished (except when they contain something besides imports) by your giant import refactor?

[Scott Morrison]

Haha, probably. :-)

[Scott Morrison]

I know we have a bunch of import tactic.linarith (which is really tactic.linarith.default).

[Scott Morrison]

I would very happily endorse someone renaming all the .default files in category theory!

[Mario Carneiro]

The equivalent of .default files in lean 4 is to have e.g. Data/Sigma/Basic.lean and Data/Sigma.lean

[Mario Carneiro]

I agree to some extent with Scott's desire to remove and/or discourage these imports which only serve to group things together because they cause spurious dependencies by design, but for tactics I think we might actually want the opposite: it is better to have fewer entry points to the tactics for precompileModules to be efficient, and also we don't want people importing just one subpart of a tactic, for example you can import Mathlib.Tactic.NormNum.Core and you will get a tactic called norm_num but it is basically unable to solve anything because you didn't import Mathlib.Tactic.NormNum.Basic which has handling for evaluating basic things like + and numbers.

[Yaël Dillies]

I think it makes sense to apply to apply different heuristics to tactic. vs everything else.

[Eric Wieser]

Mario Carneiro said:

The equivalent of .default files in lean 4 is to have e.g. Data/Sigma/Basic.lean and Data/Sigma.lean

Note that this also works in Lean3; is it worth renaming all our default.leans accordingly to make the transition easier?

[Yaël Dillies]

If nobody objects, I will delete/rename all .default to .basic later today.

[Yaël Dillies]

I think this is preferable to the data.sigma/data.sigma.something_else situation where a file is out of the folder it belongs to.

[Eric Wieser]

@Yaël Dillies; Mario's point is that foo/basic.lean + foo/default.lean become Foo/Basic.lean and Foo.lean in Lean 4

[Jireh Loreaux]

Right, but I thought we agreed we should just not have any default files in Lean 3, and hence none of the latter pattern in Lean 4. So Yaël's suggestion makes sense to me.

[Jon Eugster]

I have to say I really like the default files (i.e. the ones with just a few imports) for projects depending on mathlib, like just import LinearAlgebra and have everything ready one would usually need to get started instead of figuring out whether I need to import LinearAlgebra.Basic or LinearAlgebra.Basis or something else.
But not sure if any mathlib file should import any default file instead of the explicit imports.

[Yaël Dillies]

Yeah that's the trick. Maybe there's a way to make shortcuts separate enough from the rest that it would be impossible for mathlib to use them.