Adding files to Mathlib.Init

Stream: mathlib4

[Yaël Dillies]

What is the correct procedure for adding files to Mathlib.Init ? I am trying to add Mathlib.Tactic.MinImports to it, but the obvious thing fails in #24722 with

error: the following 1 module(s) do not import Mathlib.Init: #[Mathlib.Tactic.MinImports]

[Aaron Liu]

I think you have to have Mathlib.Tactic.MinImports import Mathlib.Tactic.Linter.Header or add it as an exception in the script

[Damiano Testa]

The general intention is that Mathlib.Init is the "first import", but Mathlib.Tactic.Linter.Header is the "really first". Plus some mechanism for preventing more imports to Init.

[Michael Rothgang]

Aaron Liu said:

I think you have to have Mathlib.Tactic.MinImports import Mathlib.Tactic.Linter.Header or add it as an exception in the script

Indeed! You shouldn't need to add an exception.

[Damiano Testa]

I wonder though whether ImportGraph is a better place for minImports.