Switch to Mathlib.Init

leanprover-community · Aug 22, 2024 · 48bea5e · 48bea5e
1 parent 4d38bbd
commit 48bea5e
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 12 deletions.
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -152,9 +152,9 @@ jobs:
         id: get
         run: |
           lake exe cache clean
-          # Fail quickly if the cache is completely cold, by checking for Batteries.WF
-          lake exe cache get Batteries.WF
-          ! test -e ./.lake/packages/batteries/.lake/build/lib/Batteries/WF.olean || lake exe cache get
+          # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
+          lake exe cache get Mathlib.Init
+          ! test -e .lake/build/lib/Mathlib/Init.olean || lake exe cache get
 
       - name: build mathlib
         id: build

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -159,9 +159,9 @@ jobs:
         id: get
         run: |
           lake exe cache clean
-          # Fail quickly if the cache is completely cold, by checking for Batteries.WF
-          lake exe cache get Batteries.WF
-          ! test -e ./.lake/packages/batteries/.lake/build/lib/Batteries/WF.olean || lake exe cache get
+          # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
+          lake exe cache get Mathlib.Init
+          ! test -e .lake/build/lib/Mathlib/Init.olean || lake exe cache get
 
       - name: build mathlib
         id: build

diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
@@ -138,9 +138,9 @@ jobs:
         id: get
         run: |
           lake exe cache clean
-          # Fail quickly if the cache is completely cold, by checking for Batteries.WF
-          lake exe cache get Batteries.WF
-          ! test -e ./.lake/packages/batteries/.lake/build/lib/Batteries/WF.olean || lake exe cache get
+          # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
+          lake exe cache get Mathlib.Init
+          ! test -e .lake/build/lib/Mathlib/Init.olean || lake exe cache get
 
       - name: build mathlib
         id: build

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -156,9 +156,9 @@ jobs:
         id: get
         run: |
           lake exe cache clean
-          # Fail quickly if the cache is completely cold, by checking for Batteries.WF
-          lake exe cache get Batteries.WF
-          ! test -e ./.lake/packages/batteries/.lake/build/lib/Batteries/WF.olean || lake exe cache get
+          # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
+          lake exe cache get Mathlib.Init
+          ! test -e .lake/build/lib/Mathlib/Init.olean || lake exe cache get
 
       - name: build mathlib
         id: build