Repetition and reverse

leanprover-community · Apr 3, 2024 · 49729f9 · 49729f9
1 parent f9105d8
commit 49729f9
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/scripts/mkAll.lean b/scripts/mkAll.lean
@@ -71,10 +71,14 @@ def mkAllCLI (args : Parsed) : IO UInt32 := do
               | some lib => return #[lib.as! String]
               | none => getLeanLibs
   let mut updates := 0
-  for d in libs do
+  for d in libs.reverse do  -- reverse to create `Mathlib.Tactic` before `Mathlib`
     let fileName := addExtension d "lean"
     let fileContent ← getAll git d
-    if (! (←  pathExists fileName)) || (← IO.FS.readFile fileName) != fileContent then
+    if !(← pathExists fileName) then
+      IO.println s!"Updating '{fileName}'"
+      updates := updates + 1
+      IO.FS.writeFile fileName fileContent
+    else if (← IO.FS.readFile fileName) != fileContent then
       IO.println s!"Updating '{fileName}'"
       updates := updates + 1
       IO.FS.writeFile fileName fileContent