chore: revert move utilities into Util directory (#5787) (#5825)

This reverts commit 4dd7b55.

Per [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Warning.3A.20some.20files.20were.20not.20found.20in.20the.20cache.2E/near/374481558) discussion.




Co-authored-by: Scott Morrison <[email protected]>

Author: kim-em

.github/workflows/bors.yml

@@ -72,10 +72,9 @@ jobs:
         run: |
           git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
-      - name: update TacticCaches.lean
+      - name: update MathlibExtras.lean
         run: |
-          cd Util
-          git ls-files 'TacticCaches/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > TacticCaches.lean
+          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
 
       - name: update Mathlib/Tactic.lean
         run: |
@@ -132,8 +131,8 @@ jobs:
         run: |
           ! grep "stdout:" stdout.log
 
-      - name: build tactic caches
-        run: lake build TacticCaches
+      - name: build library_search cache
+        run: lake build MathlibExtras
 
       - name: upload cache
         if: always()

.github/workflows/build.yml

@@ -78,10 +78,9 @@ jobs:
         run: |
           git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
-      - name: update TacticCaches.lean
+      - name: update MathlibExtras.lean
         run: |
-          cd Util
-          git ls-files 'TacticCaches/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > TacticCaches.lean
+          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
 
       - name: update Mathlib/Tactic.lean
         run: |
@@ -138,8 +137,8 @@ jobs:
         run: |
           ! grep "stdout:" stdout.log
 
-      - name: build tactic caches
-        run: lake build TacticCaches
+      - name: build library_search cache
+        run: lake build MathlibExtras
 
       - name: upload cache
         if: always()

.github/workflows/build.yml.in

@@ -58,10 +58,9 @@ jobs:
         run: |
           git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
-      - name: update TacticCaches.lean
+      - name: update MathlibExtras.lean
         run: |
-          cd Util
-          git ls-files 'TacticCaches/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > TacticCaches.lean
+          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
 
       - name: update Mathlib/Tactic.lean
         run: |
@@ -118,8 +117,8 @@ jobs:
         run: |
           ! grep "stdout:" stdout.log
 
-      - name: build tactic caches
-        run: lake build TacticCaches
+      - name: build library_search cache
+        run: lake build MathlibExtras
 
       - name: upload cache
         if: always()

.github/workflows/build_fork.yml

@@ -76,10 +76,9 @@ jobs:
         run: |
           git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
-      - name: update TacticCaches.lean
+      - name: update MathlibExtras.lean
         run: |
-          cd Util
-          git ls-files 'TacticCaches/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > TacticCaches.lean
+          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
 
       - name: update Mathlib/Tactic.lean
         run: |
@@ -136,8 +135,8 @@ jobs:
         run: |
           ! grep "stdout:" stdout.log
 
-      - name: build tactic caches
-        run: lake build TacticCaches
+      - name: build library_search cache
+        run: lake build MathlibExtras
 
       - name: upload cache
         if: always()

Util/Cache/Hashing.lean Cache/Hashing.lean

@@ -103,7 +103,7 @@ partial def getFileHash (filePath : FilePath) : HashM $ Option UInt64 := do
         depsMap := stt.depsMap.insert filePath fileImports })
 
 /-- Files to start hashing from. -/
-def roots : Array FilePath := #["Mathlib.lean", "Util/TacticCaches.lean"]
+def roots : Array FilePath := #["Mathlib.lean", "MathlibExtras.lean"]
 
 /-- Main API to retrieve the hashes of the Lean files -/
 def getHashMemo : IO HashMemo :=

Util/Cache/IO.lean Cache/IO.lean

@@ -69,10 +69,7 @@ def mathlibDepPath : FilePath :=
 -- TODO this should be generated automatically from the information in `lakefile.lean`.
 def getPackageDirs : IO PackageDirs := return .ofList [
   ("Mathlib", if ← isMathlibRoot then "." else mathlibDepPath),
-  -- Note that this prevents downstream projects from using a top-level `Util` directory.
-  -- I'm not sure a good way around this for now, but hopefully it will be made obsolete
-  -- by a new `cache` before it affects anyone.
-  ("Util", if ← isMathlibRoot then "." else mathlibDepPath),
+  ("MathlibExtras", if ← isMathlibRoot then "." else mathlibDepPath),
   ("Aesop", LAKEPACKAGESDIR / "aesop"),
   ("Std", LAKEPACKAGESDIR / "std"),
   ("ProofWidgets", LAKEPACKAGESDIR / "proofwidgets"),
@@ -85,7 +82,7 @@ def getPackageDir (path : FilePath) : IO FilePath :=
   match path.withExtension "" |>.components.head? with
   | none => throw $ IO.userError "Can't find package directory for empty path"
   | some pkg => match pkgDirs.find? pkg with
-    | none => throw $ IO.userError s!"Unknown package directory for {pkg}, {path}"
+    | none => throw $ IO.userError s!"Unknown package directory for {pkg}"
     | some path => return path
 
 /-- Runs a terminal command and retrieves its output, passing the lines to `processLine` -/
@@ -209,8 +206,8 @@ def isPathFromMathlib (path : FilePath) : Bool :=
   match path.components with
   | "Mathlib" :: _ => true
   | ["Mathlib.lean"] => true
-  | "Util" :: "TacticCaches" :: _ => true
-  | ["Util", "TacticCaches.lean"] => true
+  | "MathlibExtras" :: _ => true
+  | ["MathlibExtras.lean"] => true
   | _ => false
 
 /-- Decompresses build files into their respective folders -/

Util/Cache/Main.lean Cache/Main.lean

@@ -28,8 +28,8 @@ section Get
 
 /-- Formats the config file for `curl`, containing the list of files to be downloaded -/
 def mkGetConfigContent (hashMap : IO.HashMap) : IO String := do
-  -- We sort the list so that the large files in `Util/TacticCaches` are requested first.
-  hashMap.toArray.qsort (fun ⟨p₁, _⟩ ⟨_, _⟩ => p₁.components.take 2 = ["Util", "TacticCaches"])
+  -- We sort the list so that the large files in `MathlibExtras` are requested first.
+  hashMap.toArray.qsort (fun ⟨p₁, _⟩ ⟨_, _⟩ => p₁.components.head? = "MathlibExtras")
     |>.foldlM (init := "") fun acc ⟨_, hash⟩ => do
     let fileName := hash.asTarGz
     -- Below we use `String.quote`, which is intended for quoting for use in Lean code

Util/Cache/Requests.lean Cache/Requests.lean

@@ -67,7 +67,7 @@ def processLemma (name : Name) (constInfo : ConstantInfo) :
 /-- Insert a lemma into the discrimination tree. -/
 -- Recall that `apply?` caches the discrimination tree on disk.
 -- If you are modifying this file, you will probably want to delete
--- `build/lib/Util/TacticCaches/LibrarySearch.extra`
+-- `build/lib/MathlibExtras/LibrarySearch.extra`
 -- so that the cache is rebuilt.
 def addLemma (name : Name) (constInfo : ConstantInfo)
     (lemmas : DiscrTree (Name × DeclMod) true) : MetaM (DiscrTree (Name × DeclMod) true) := do
@@ -92,9 +92,9 @@ open System (FilePath)
 
 def cachePath : IO FilePath :=
   try
-    return (← findOLean `TacticCaches.LibrarySearch).withExtension "extra"
+    return (← findOLean `MathlibExtras.LibrarySearch).withExtension "extra"
   catch _ =>
-    return "build" / "lib" / "Util" / "TacticCaches" / "LibrarySearch.extra"
+    return "build" / "lib" / "MathlibExtras" / "LibrarySearch.extra"
 
 initialize cachedData : CachedData (Name × DeclMod) ← unsafe do
   let path ← cachePath

Mathlib/Tactic/LibrarySearch.lean

@@ -64,7 +64,7 @@ def processLemma (name : Name) (constInfo : ConstantInfo) :
 /-- Insert a lemma into the discrimination tree. -/
 -- Recall that `rw?` caches the discrimination tree on disk.
 -- If you are modifying this file, you will probably want to delete
--- `build/lib/Util/TacticCaches/Rewrites.extra`
+-- `build/lib/MathlibExtras/Rewrites.extra`
 -- so that the cache is rebuilt.
 def addLemma (name : Name) (constInfo : ConstantInfo)
     (lemmas : DiscrTree (Name × Bool × Nat) true) : MetaM (DiscrTree (Name × Bool × Nat) true) := do
@@ -89,9 +89,9 @@ open System (FilePath)
 
 def cachePath : IO FilePath :=
   try
-    return (← findOLean `TacticCaches.Rewrites).withExtension "extra"
+    return (← findOLean `MathlibExtras.Rewrites).withExtension "extra"
   catch _ =>
-    return "build" / "lib" / "Util" / "TacticCaches" / "Rewrites.extra"
+    return "build" / "lib" / "MathlibExtras" / "Rewrites.extra"
 
 initialize cachedData : CachedData (Name × Bool × Nat) ← unsafe do
   let path ← cachePath

Mathlib/Tactic/Rewrites.lean

@@ -0,0 +1,2 @@
+import MathlibExtras.LibrarySearch
+import MathlibExtras.Rewrites

MathlibExtras.lean

@@ -33,35 +33,24 @@ require aesop from git "https://github.com/JLimperg/aesop" @ "master"
 require Cli from git "https://github.com/mhuisi/lean4-cli.git" @ "nightly"
 require proofwidgets from git "https://github.com/EdAyers/ProofWidgets4" @ "v0.0.11"
 
-lean_lib Archive where
-  roots := #[`Archive]
-
-lean_lib Counterexamples where
-  roots := #[`Counterexamples]
-
-/-!
-# Utilities, stored in the `Util` directory.
-
-* `lake exe cache`, providing olean caching
-* `lake exe graph`, generating import graphs, as `leanproject import-graph` used to in Lean 3.
-* additional caches for tactics, stored in `Util/TacticCaches`.
--/
-
 lean_lib Cache where
   moreLeanArgs := moreLeanArgs
   roots := #[`Cache]
-  srcDir := "Util"
 
 lean_exe cache where
-  root := `Util.Cache.Main
+  root := `Cache.Main
+
+lean_lib MathlibExtras where
+  roots := #[`MathlibExtras]
+
+lean_lib Archive where
+  roots := #[`Archive]
+
+lean_lib Counterexamples where
+  roots := #[`Counterexamples]
 
 lean_lib ImportGraph where
   roots := #[`ImportGraph]
-  srcDir := "Util"
 
 lean_exe graph where
-  root := `Util.ImportGraph.Main
-
-lean_lib TacticCaches where
-  roots := #[`TacticCaches]
-  srcDir := "Util"
+  root := `ImportGraph.Main

Util/TacticCaches/LibrarySearch.lean MathlibExtras/LibrarySearch.lean

@@ -14,7 +14,7 @@ import Mathlib.Data.Nat.Prime
 -- Recall that `apply?` caches the discrimination tree on disk.
 -- If you are modifying the way that `apply?` indexes lemmas,
 -- while testing you will probably want to delete
--- `build/lib/Util/TacticCaches/LibrarySearch.extra`
+-- `build/lib/MathlibExtras/LibrarySearch.extra`
 -- so that the cache is rebuilt.
 
 noncomputable section

Util/TacticCaches/Rewrites.lean MathlibExtras/Rewrites.lean

@@ -10,7 +10,7 @@ import Mathlib.Algebra.Group.Basic
 -- Recall that `rw?` caches the discrimination tree on disk.
 -- If you are modifying the way that `rewrites` indexes lemmas,
 -- while testing you will probably want to delete
--- `build/lib/Util/TacticCaches/Rewrites.extra`
+-- `build/lib/MathlibExtras/Rewrites.extra`
 -- so that the cache is rebuilt.
 
 /--