Mathlib.Init automation

Stream: mathlib4

[Damiano Testa]

Since a few weeks, there is a Mathlib.Init file that is supposed to have minimal imports and is imported by virtually any file in mathlib, except for a handful of exceptions (such as the style linters).

However, there are currently 9 files that neither import, nor are imported by Mathlib.Init (with the exception of Mathlib.Init itself):

[Mathlib.Data.DList.Defs,
 Mathlib.Data.Nat.Notation,
 Mathlib.Data.Stream.Defs,
 Mathlib.Deprecated.Combinator,
 Mathlib.Tactic.Linter.AdmitLinter,
 Mathlib.Tactic.Linter.FlexibleLinter,
 Mathlib.Tactic.Linter.TextBased,
 Mathlib.Tactic.StacksAttribute,
 Mathlib.Util.AssertExistsExt]

I am responsible for adding some linters and some extension after Mathlib.Init was created. Nevertheless, should there be a CI step that makes sure that the list above stays empty?

[Johan Commelin]

I think it suffices to check this by hand once every while (3~4 times per year?).

[Johan Commelin]

I think it is unlikely that it will cause anybody trouble that this list is non-empty in practice.

[Damiano Testa]

Ok, maybe it can be on a cron job, like lean4checker, but with a slower frequency.

[Johan Commelin]

What would the cronjob do, if the list is non-empty?

[Damiano Testa]

It could add import Mathlib.Init to the import-earliest files that do not import Mathlib.Init and create a PR, maybe?

[Johan Commelin]

Sure, but it could also add those files to Mathlib.Init. And I guess it might be 50-50 which option a file needs... so I think we can't really automate this