feat: check that every file imports Mathlib.Init (#18281)

We add a text-based check to the `lint-style` script, that every file either (transitively) imports Mathlib.Init, or is (transitively) imported by it.



Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

Author: grunweg

Mathlib/Init.lean

@@ -1,6 +1,6 @@
 import Mathlib.Tactic.Linter.DocPrime
-import Mathlib.Tactic.Linter.HashCommandLinter
 import Mathlib.Tactic.Linter.GlobalAttributeIn
+import Mathlib.Tactic.Linter.HashCommandLinter
 import Mathlib.Tactic.Linter.Header
 -- This file imports Batteries.Tactic.Lint, where the `env_linter` attribute is defined.
 import Mathlib.Tactic.Linter.Lint
@@ -21,6 +21,9 @@ Here are some general guidelines:
 * strong preference for avoiding files that themselves have imports beyond `Lean`, and
   any exception to this rule should by accompanied by a comment explaining the transitive imports.
 
+A linter verifies that every file in Mathlib imports `Mathlib.Init`
+(perhaps indirectly) --- except for the imports in this file, of course.
+
 ## Linters
 
 All syntax linters defined in Mathlib which are active by default are imported here.
@@ -30,7 +33,7 @@ as early as possible.
 All linters imported here have no bulk imports;
 **Not** imported in this file are
 - the text-based linters in `Linters/TextBased.lean`, as they can be imported later
-- the `minImports` linter, as that is still disabled by default.
+- the `minImports` linter, as that is still disabled by default
 - the `haveLet` linter, as it is currently disabled by default
 
 -/

Mathlib/Tactic/Linter/TextBased.lean

@@ -265,7 +265,7 @@ Return the number of files which had new style errors.
 `moduleNames` are all the modules to lint,
 `mode` specifies what kind of output this script should produce,
 `fix` configures whether fixable errors should be corrected in-place. -/
-def lintModules (moduleNames : Array String) (style : ErrorFormat) (fix : Bool) : IO UInt32 := do
+def lintModules (moduleNames : Array Lean.Name) (style : ErrorFormat) (fix : Bool) : IO UInt32 := do
   -- Read the `nolints` file, with manual exceptions for the linter.
   let nolints ← IO.FS.lines ("scripts" / "nolints-style.txt")
   let styleExceptions := parseStyleExceptions nolints
@@ -274,7 +274,7 @@ def lintModules (moduleNames : Array String) (style : ErrorFormat) (fix : Bool)
   let mut allUnexpectedErrors := #[]
   for module in moduleNames do
     -- Convert the module name to a file name, then lint that file.
-    let path := (mkFilePath (module.split (· == '.'))).addExtension "lean"
+    let path := mkFilePath (module.components.map toString)|>.addExtension "lean"
 
     let (errors, changed) := ← lintFile path styleExceptions
     if let some c := changed then

scripts/lint-style.lean

@@ -4,21 +4,77 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Rothgang
 -/
 
+import Lean.Elab.ParseImportsFast
+import Batteries.Data.String.Basic
 import Mathlib.Tactic.Linter.TextBased
 import Cli.Basic
 
 /-!
 # Text-based style linters
 
-This files defines the `lint-style` executable which runs all text-based style linters.
+This file defines the `lint-style` executable which runs all text-based style linters.
 The linters themselves are defined in `Mathlib.Tactic.Linter.TextBased`.
 
-In addition, this checks that every file in `scripts` is documented in its top-level README.
+In addition, this checks that
+- `Mathlib.Init` is (transitively) imported in all of mathlib, and
+- every file in `scripts` is documented in its top-level README.
 -/
 
-open Cli Mathlib.Linter.TextBased
+open Cli Mathlib.Linter.TextBased System.FilePath
+
+/-- Parse all imports in a text file at `path` and return just their names:
+this is just a thin wrapper around `Lean.parseImports'`.
+Omit `Init (which is part of the prelude). -/
+def findImports (path : System.FilePath) : IO (Array Lean.Name) := do
+  return (← Lean.parseImports' (← IO.FS.readFile path) path.toString)
+    |>.map (fun imp ↦ imp.module) |>.erase `Init
+
+
+/-- Check that `Mathlib.Init` is transitively imported in all of Mathlib.
+
+Every file imported in `Mathlib.Init` should in turn import the `Header` linter
+(except for the header linter itself, of course).
+Return `true` iff there was an error.
+-/
+def checkInitImports : IO Bool := do
+  -- Find any file in the Mathlib directory which does not contain any Mathlib import.
+  -- We simply parse `Mathlib.lean`, as CI ensures this file is up to date.
+  let allModuleNames := (← findImports "Mathlib.lean").erase `Batteries
+  let mut modulesWithoutMathlibImports := #[]
+  let mut importsHeaderLinter := #[]
+  for module in allModuleNames do
+    let path := System.mkFilePath (module.components.map fun n ↦ n.toString)|>.addExtension "lean"
+    let imports ← findImports path
+    let hasNoMathlibImport := imports.all fun name ↦ name.getRoot != `Mathlib
+    if hasNoMathlibImport then
+      modulesWithoutMathlibImports := modulesWithoutMathlibImports.push module
+    if imports.contains `Mathlib.Tactic.Linter.Header then
+      importsHeaderLinter := importsHeaderLinter.push module
+
+  -- Every file importing the `header` linter should be imported in `Mathlib/Init.lean` itself.
+  -- (Downstream files should import `Mathlib.Init` and not the header linter.)
+  -- The only exception are auto-generated import-only files.
+  let initImports ← findImports ("Mathlib" / "Init.lean")
+  let mismatch := importsHeaderLinter.filter (fun mod ↦
+    ![`Mathlib, `Mathlib.Tactic, `Mathlib.Init].contains mod && !initImports.contains mod)
+    -- This file is transitively imported by `Mathlib.Init`.
+    |>.erase `Mathlib.Tactic.DeclarationNames
+  if mismatch.size > 0 then
+    IO.eprintln s!"error: the following {mismatch.size} module(s) import the `header` linter \
+      directly, but should import Mathlib.Init instead: {mismatch}\n\
+      The `header` linter is included in Mathlib.Init, and every file in Mathlib \
+      should import Mathlib.Init.\nPlease adjust the imports accordingly."
+    return true
+
+  -- Now, it only remains to check that every module (except for the Header linter itself)
+  -- imports some file in Mathlib.
+  let missing := modulesWithoutMathlibImports.erase `Mathlib.Tactic.Linter.Header
+  if missing.size > 0 then
+    IO.eprintln s!"error: the following {missing.size} module(s) do not import Mathlib.Init: \
+      {missing}"
+    return true
+  return false
 
-open System.FilePath
 
 /-- Verifies that every file in the `scripts` directory is documented in `scripts/README.md`.
 Return `True` if there are undocumented scripts, otherwise `False`. -/
@@ -40,19 +96,21 @@ def allScriptsDocumented : IO Bool := do
       {String.intercalate "," undocumented.toList}"
   return undocumented.size == 0
 
+
 /-- Implementation of the `lint-style` command line program. -/
 def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
   let style : ErrorFormat := match args.hasFlag "github" with
     | true => ErrorFormat.github
     | false => ErrorFormat.humanReadable
   let fix := args.hasFlag "fix"
   -- Read all module names to lint.
-  let mut allModules := #[]
+  let mut allModuleNames := #[]
   for s in ["Archive.lean", "Counterexamples.lean", "Mathlib.lean"] do
-    allModules := allModules.append ((← IO.FS.lines s).map (·.stripPrefix "import "))
-  -- Note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually.
-  allModules := allModules.erase "Batteries"
-  let mut numberErrors ← lintModules allModules style fix
+    allModuleNames := allModuleNames.append (← findImports s)
+  -- Note: since "Batteries" is added explicitly to "Mathlib.lean", we remove it here manually.
+  allModuleNames := allModuleNames.erase `Batteries
+  let mut numberErrors ← lintModules allModuleNames style fix
+  if ← checkInitImports then numberErrors := numberErrors + 1
   if !(← allScriptsDocumented) then numberErrors := numberErrors + 1
   -- If run with the `--fix` argument, return a zero exit code.
   -- Otherwise, make sure to return an exit code of at most 125,