Only import existing files

leanprover-community · Apr 3, 2024 · f9105d8 · f9105d8
1 parent 6485b73
commit f9105d8
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/scripts/mkAll.lean b/scripts/mkAll.lean
@@ -37,8 +37,11 @@ def getAll (git : Bool) (ml : String) : IO String := do
       let all ← walkDir ml
       return all.filter (·.extension == some "lean"))
   let files := (stdout.erase ml.lean).qsort (·.toString < ·.toString)
-  let withImport ← files.mapM fun f => return "import " ++ (← moduleNameOfFileName f none).toString
-  return ("\n".intercalate withImport.toList).push '\n'
+  let withImport ← files.mapM fun f => do
+    if ←  pathExists f then
+      return "import " ++ (← moduleNameOfFileName f none).toString
+    else return ""
+  return ("\n".intercalate (withImport.filter (· != "")).toList).push '\n'
 
 open Lake in
 /-- `getLeanLibs` returns the array of names (as an `Array` of `String`s) of all the libraries