trying to delete unused mathlib cache

hhu-adam · Nov 14, 2023 · 789a36d · 789a36d
1 parent defd384
commit 789a36d
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -32,10 +32,18 @@ jobs:
           # The 'sleep 1' is small pause to let the network recover.
           lake exe cache get || (sleep 1; lake exe cache get)
 
+      - name: create timestamp file
+        run: touch tmp_timestamp
 
       - name: building game
         run: env LEAN_ABORT_ON_PANIC=1 lake build
 
+      - name: delete unused mathlib cache
+        run: find ./lake-packages/mathlib/build/lib -type f -name "*" \! -neweraa ./tmp_timestamp -delete
+
+      - name: delete timestamp file
+        run: rm ./tmp_timestamp
+
       - name: zip built game
         run: zip game.zip ./* -r