@@ -13,9 +13,10 @@ Currently, we only test the following:
1313
1414
1515/-- Collects the module names corresponding to all `lean` files in the file system. -/
16- partial def collectModulesOnFileSystem (sysroot : System.FilePath) (roots : Array String) :
16+ partial def collectModulesOnFileSystem (searchPaths : List System.FilePath) (roots : Array String) :
1717 IO (Array String) :=
18- roots.flatMapM (fun (root : String) => go (sysroot / "lib" / "lean" / root) root #[])
18+ searchPaths.toArray.flatMapM (fun libdir =>
19+ roots.flatMapM (fun (root : String) => go (libdir / root) root #[]))
1920where
2021 go (dir : System.FilePath) (pref : String) (sofar : Array String) : IO (Array String) := do
2122 if !(← dir.pathExists) then
2728 match mdata.type with
2829 | .dir => arr ← go entry.path (pref ++ "." ++ entry.fileName) arr
2930 | .file =>
30- if entry.path.extension == some "olean " then
31+ if entry.path.extension == some "lean " then
3132 arr := arr.push (pref ++ "." ++ entry.path.fileStem.get!)
3233 | _ => pure ()
3334 return arr
@@ -63,9 +64,10 @@ def analyzeModuleData (data : Array (Name × ModuleData)) : ImportGraph := Id.ru
6364
6465 result
6566
66- def computeOrphanedModules (sysroot : System.FilePath) ( importGraph : ImportGraph) :
67+ def computeOrphanedModules (importGraph : ImportGraph) :
6768 IO (Array String) := do
68- let onFS ← collectModulesOnFileSystem sysroot #["Init" , "Std" , "Lean" ]
69+ let searchPath ← Lean.getSrcSearchPath
70+ let onFS ← collectModulesOnFileSystem searchPath #["Init" , "Std" , "Lean" ]
6971 let imported : HashSet String := #["Init" , "Std" , "Lean" ].foldl (init := ∅)
7072 (fun sofar root => sofar.insertMany (dfs root importGraph.imports ∅))
7173 return onFS.filter (fun module => !imported.contains module)
@@ -86,22 +88,13 @@ def test : MetaM Unit := do
8688 let env ← importModules #[`Init, `Std, `Lean] {}
8789 let importGraph := analyzeModuleData (env.header.moduleNames.zip env.header.moduleData)
8890
89- let orphanedModules ← computeOrphanedModules sysroot importGraph
91+ let orphanedModules ← computeOrphanedModules importGraph
9092 if !orphanedModules.isEmpty then do
9193 logError s! "There are orphaned modules: { orphanedModules} "
9294
9395 let illegalReverseImports := computeIllegalReverseImportsOfInitDataOptionCoe importGraph
9496 if !illegalReverseImports.isEmpty then do
9597 logError s! "The following modules illegally (transitively) import Init.Data.Option.Coe: { illegalReverseImports} "
9698
97- /-!
98- We check which modules exist by looking at which `olean` files are present in the file system.
99- This means that locally you might get false positives on this test because there are some `olean`
100- files still floating around where the corresponding `lean` file no longer exists in the source.
101-
102- It would be better to check for `lean` files directly, but our CI step which runs the tests doesn't
103- see the source files in the `srcPath`.
104- -/
105-
10699#guard_msgs in
107100#eval test
0 commit comments