chore: test that there are no orphaned modules (#8082)

This PR adds a test that makes sure that there are no orphaned modules.

src/Init/Data/Nat.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 import Init.Data.Nat.Basic
-import Init.Data.Nat.Div.Basic
+import Init.Data.Nat.Div
 import Init.Data.Nat.Dvd
 import Init.Data.Nat.Gcd
 import Init.Data.Nat.MinMax

src/Init/Data/Vector.lean

@@ -21,3 +21,4 @@ import Init.Data.Vector.InsertIdx
 import Init.Data.Vector.FinRange
 import Init.Data.Vector.Extract
 import Init.Data.Vector.Perm
+import Init.Data.Vector.Find

src/Lean/Compiler/IR.lean

@@ -23,6 +23,11 @@ import Lean.Compiler.IR.EmitC
 import Lean.Compiler.IR.CtorLayout
 import Lean.Compiler.IR.Sorry
 
+-- The following imports are not required by the compiler. They are here to ensure that there
+-- are no orphaned modules.
+import Lean.Compiler.IR.LLVMBindings
+import Lean.Compiler.IR.EmitLLVM
+
 namespace Lean.IR
 
 register_builtin_option compiler.reuse : Bool := {

src/Lean/Compiler/LCNF.lean

@@ -41,3 +41,4 @@ import Lean.Compiler.LCNF.MonadScope
 import Lean.Compiler.LCNF.Closure
 import Lean.Compiler.LCNF.LambdaLifting
 import Lean.Compiler.LCNF.ReduceArity
+import Lean.Compiler.LCNF.Probing

src/Lean/Meta/Match/Match.lean

@@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.GeneralizeTelescope
 import Lean.Meta.Match.Basic
 import Lean.Meta.Match.MatcherApp.Basic
+import Lean.Meta.Match.MVarRenaming
 
 namespace Lean.Meta.Match
 

src/Std.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
 prelude
+import Std.Classes
 import Std.Data
 import Std.Sat
 import Std.Sync

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.lean

@@ -1,27 +0,0 @@
-/-
-Copyright (c) 2024 FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-prelude
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Eq
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Not
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.RotateLeft
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.RotateRight
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Ult
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ZeroExtend
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
-
-/-!
-This directory contains the implementations of bitblasters for all basic operations on `BVExpr`
-and `BVPred`.
--/

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.lean

@@ -1,25 +0,0 @@
-/-
-Copyright (c) 2024 FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-prelude
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Append
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Eq
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Extract
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.GetLsbD
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Not
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.RotateLeft
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.RotateRight
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftLeft
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Ult
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ZeroExtend
-
-/-!
-This directory contains the verification of bitblasters for all basic operations on `BVExpr` and
-`BVPred`.
--/

src/Std/Tactic/BVDecide/LRAT/Internal.lean

@@ -1,21 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-prelude
-import Std.Tactic.BVDecide.LRAT.Internal.Actions
-import Std.Tactic.BVDecide.LRAT.Internal.Assignment
-import Std.Tactic.BVDecide.LRAT.Internal.CNF
-import Std.Tactic.BVDecide.LRAT.Internal.Formula
-import Std.Tactic.BVDecide.LRAT.Internal.Entails
-import Std.Tactic.BVDecide.LRAT.Internal.Clause
-import Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
-import Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
-import Std.Tactic.BVDecide.LRAT.Internal.PosFin
-import Std.Tactic.BVDecide.LRAT.Internal.Convert
-
-/-!
-This module contains the internals of the current LRAT checker implementation. It should not be
-considered part of the API of `bv_decide` and will be removed or largely refactored in the future.
--/

tests/lean/run/importStructure.lean

@@ -0,0 +1,90 @@
+import Lean
+import Std
+
+open Std Lean
+
+/-!
+This test analyzes the import structure of the modules and core and fails if something is wrong.
+
+Currently, we only test for the absence of orphaned modules.
+-/
+
+/-- Collects the module names corresponding to all `lean` files in the file system. -/
+partial def collectModulesOnFileSystem (sysroot : System.FilePath) (roots : Array String) :
+    IO (Array String) :=
+  roots.flatMapM (fun (root : String) => go (sysroot / "lib" / "lean" / root) root #[])
+where
+  go (dir : System.FilePath) (pref : String) (sofar : Array String) : IO (Array String) := do
+    if !(← dir.pathExists) then
+      return sofar
+
+    let mut arr := sofar
+    for entry in ← dir.readDir do
+      let mdata ← entry.path.metadata
+      match mdata.type with
+      | .dir => arr ← go entry.path (pref ++ "." ++ entry.fileName) arr
+      | .file =>
+          if entry.path.extension == some "olean" then
+            arr := arr.push (pref ++ "." ++ entry.path.fileStem.get!)
+      | _ => pure ()
+    return arr
+
+partial def dfs (cur : String) (graph : HashMap String (Array String)) (seen : HashSet String) :
+    HashSet String := Id.run do
+  if cur ∈ seen then
+    return seen
+
+  let mut seen' := seen.insert cur
+  for next in graph.getD cur #[] do
+    seen' := dfs next graph seen'
+
+  return seen'
+
+structure ImportGraph where
+  imports : HashMap String (Array String)
+  reverseImports : HashMap String (Array String)
+
+def analyzeModuleData (data : Array (Name × ModuleData)) : ImportGraph := Id.run do
+  let mut result : ImportGraph := ⟨∅, ∅⟩
+
+  for (name, module) in data do
+    for imp in module.imports do
+      let fromString := name.toString
+      let toString := imp.module.toString
+      result := {
+        imports := result.imports.alter fromString
+          (fun arr => some <| (arr.getD #[]).push toString)
+        reverseImports := result.imports.alter toString
+          (fun arr => some <| (arr.getD #[]).push fromString)
+      }
+
+  result
+
+def computeOrphanedModules (sysroot : System.FilePath) (importGraph : ImportGraph) :
+    IO (Array String) := do
+  let onFS ← collectModulesOnFileSystem sysroot #["Init", "Std", "Lean"]
+  let imported : HashSet String := #["Init", "Std", "Lean"].foldl (init := ∅)
+    (fun sofar root => sofar.insertMany (dfs root importGraph.imports ∅))
+  return onFS.filter (fun module => !imported.contains module)
+
+def test : MetaM Unit := do
+  let sysroot ← findSysroot
+  initSearchPath sysroot
+  let env ← importModules #[`Init, `Std, `Lean] {}
+  let importGraph := analyzeModuleData (env.header.moduleNames.zip env.header.moduleData)
+  let orphanedModules ← computeOrphanedModules sysroot importGraph
+
+  if !orphanedModules.isEmpty then do
+    logError s!"There are orphaned modules: {orphanedModules}"
+
+/-!
+We check which modules exist by looking at which `olean` files are present in the file system.
+This means that locally you might get false positives on this test because there are some `olean`
+files still floating around where the corresponding `lean` file no longer exists in the source.
+
+It would be better to check for `lean` files directly, but our CI step which runs the tests doesn't
+see the source files in the `srcPath`.
+-/
+
+#guard_msgs in
+#eval test