Trigger CI for leanprover/lean4#3082

leanprover-community · Jan 24, 2024 · 54afcd2 · 54afcd2
2 parents 3af4fac + 32009e7
commit 54afcd2
Show file tree

Hide file tree

Showing 1,761 changed files with 36,431 additions and 22,919 deletions.
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -170,16 +170,14 @@ jobs:
           # The ProofWidgets release contains not just the `.js` (which we need in order to build)
           # but also `.oleans`, which may have been built with the wrong toolchain.
           # This removes them.
+          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
           rm -rf .lake/packages/proofwidgets/.lake/build/lib
           rm -rf .lake/packages/proofwidgets/.lake/build/ir
 
       - name: get cache
         run: |
           lake exe cache clean
-          # We've been seeing many failures at this step recently because of network errors.
-          # As a band-aid, we try twice.
-          # The 'sleep 1' is small pause to let the network recover.
-          lake exe cache get || (sleep 1; lake exe cache get)
+          lake exe cache get
 
       - name: build mathlib
         id: build
@@ -190,20 +188,22 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
       - name: check for noisy stdout lines
+        id: noisy
         run: |
           ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras
 
       - name: upload cache
-        if: always()
+        # We only upload the cache if the build ran (either succeeding or failing),
+        # but not if it was skipped.
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         run: |
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
           # lake exe cache pack! || true
           lake exe cache commit || true
-          # try twice in case of network errors
-          lake exe cache put || (sleep 1; lake exe cache put) || true
+          lake exe cache put || true
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -220,6 +220,7 @@ jobs:
           fi
 
       - name: build archive
+        id: archive
         run: |
           # Note: we should not be including `Archive` and `Countexamples` in the cache.
           # We do this for now for the sake of not rebuilding them in every CI run
@@ -228,19 +229,19 @@ jobs:
           # it should be possible to determine whether they need to be built without actually
           # storing and transferring oleans over the network.
           # Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
-          # We retry twice in case of network errors.
-          lake exe cache get Archive.lean || (sleep 1; lake exe cache get Archive.lean)
+          lake exe cache get Archive.lean
           lake build Archive
-          lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
+          lake exe cache put Archive.lean
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: build counterexamples
+        id: counterexamples
         run: |
-          lake exe cache get Counterexamples.lean || (sleep 1; lake exe cache get Counterexamples.lean)
+          lake exe cache get Counterexamples.lean
           lake build Counterexamples
-          lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
+          lake exe cache put Counterexamples.lean
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -255,6 +256,11 @@ jobs:
           lake exe graph
           rm import_graph.dot
 
+      - name: verify `lake exe shake` works
+        # Later, we may want to make output from `shake` a CI error?
+        run: |
+          lake exe shake
+
       - name: test mathlib
         id: test
         run: |
@@ -290,9 +296,12 @@ jobs:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
           GITHUB_CONTEXT: ${{ toJson(github) }}
           WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
+          BUILD_OUTCOME: ${{ steps.build.outcome }}
+          NOISY_OUTCOME: ${{ steps.noisy.outcome }}
+          ARCHIVE_OUTCOME: ${{ steps.archive.outcome }}
+          COUNTEREXAMPLE_OUTCOME: ${{ steps.counterexamples.outcome }}
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
-          BUILD_OUTCOME: ${{ steps.build.outcome }}
           CHECK_OUTCOME: ${{ steps.lean4checker.outcome }}
         run: |
           scripts/lean-pr-testing-comments.sh

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -177,16 +177,14 @@ jobs:
           # The ProofWidgets release contains not just the `.js` (which we need in order to build)
           # but also `.oleans`, which may have been built with the wrong toolchain.
           # This removes them.
+          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
           rm -rf .lake/packages/proofwidgets/.lake/build/lib
           rm -rf .lake/packages/proofwidgets/.lake/build/ir
 
       - name: get cache
         run: |
           lake exe cache clean
-          # We've been seeing many failures at this step recently because of network errors.
-          # As a band-aid, we try twice.
-          # The 'sleep 1' is small pause to let the network recover.
-          lake exe cache get || (sleep 1; lake exe cache get)
+          lake exe cache get
 
       - name: build mathlib
         id: build
@@ -197,20 +195,22 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
       - name: check for noisy stdout lines
+        id: noisy
         run: |
           ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras
 
       - name: upload cache
-        if: always()
+        # We only upload the cache if the build ran (either succeeding or failing),
+        # but not if it was skipped.
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         run: |
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
           # lake exe cache pack! || true
           lake exe cache commit || true
-          # try twice in case of network errors
-          lake exe cache put || (sleep 1; lake exe cache put) || true
+          lake exe cache put || true
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -227,6 +227,7 @@ jobs:
           fi
 
       - name: build archive
+        id: archive
         run: |
           # Note: we should not be including `Archive` and `Countexamples` in the cache.
           # We do this for now for the sake of not rebuilding them in every CI run
@@ -235,19 +236,19 @@ jobs:
           # it should be possible to determine whether they need to be built without actually
           # storing and transferring oleans over the network.
           # Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
-          # We retry twice in case of network errors.
-          lake exe cache get Archive.lean || (sleep 1; lake exe cache get Archive.lean)
+          lake exe cache get Archive.lean
           lake build Archive
-          lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
+          lake exe cache put Archive.lean
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: build counterexamples
+        id: counterexamples
         run: |
-          lake exe cache get Counterexamples.lean || (sleep 1; lake exe cache get Counterexamples.lean)
+          lake exe cache get Counterexamples.lean
           lake build Counterexamples
-          lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
+          lake exe cache put Counterexamples.lean
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -262,6 +263,11 @@ jobs:
           lake exe graph
           rm import_graph.dot
 
+      - name: verify `lake exe shake` works
+        # Later, we may want to make output from `shake` a CI error?
+        run: |
+          lake exe shake
+
       - name: test mathlib
         id: test
         run: |
@@ -297,9 +303,12 @@ jobs:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
           GITHUB_CONTEXT: ${{ toJson(github) }}
           WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
+          BUILD_OUTCOME: ${{ steps.build.outcome }}
+          NOISY_OUTCOME: ${{ steps.noisy.outcome }}
+          ARCHIVE_OUTCOME: ${{ steps.archive.outcome }}
+          COUNTEREXAMPLE_OUTCOME: ${{ steps.counterexamples.outcome }}
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
-          BUILD_OUTCOME: ${{ steps.build.outcome }}
           CHECK_OUTCOME: ${{ steps.lean4checker.outcome }}
         run: |
           scripts/lean-pr-testing-comments.sh

diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
@@ -156,16 +156,14 @@ jobs:
           # The ProofWidgets release contains not just the `.js` (which we need in order to build)
           # but also `.oleans`, which may have been built with the wrong toolchain.
           # This removes them.
+          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
           rm -rf .lake/packages/proofwidgets/.lake/build/lib
           rm -rf .lake/packages/proofwidgets/.lake/build/ir
 
       - name: get cache
         run: |
           lake exe cache clean
-          # We've been seeing many failures at this step recently because of network errors.
-          # As a band-aid, we try twice.
-          # The 'sleep 1' is small pause to let the network recover.
-          lake exe cache get || (sleep 1; lake exe cache get)
+          lake exe cache get
 
       - name: build mathlib
         id: build
@@ -176,20 +174,22 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
       - name: check for noisy stdout lines
+        id: noisy
         run: |
           ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras
 
       - name: upload cache
-        if: always()
+        # We only upload the cache if the build ran (either succeeding or failing),
+        # but not if it was skipped.
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         run: |
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
           # lake exe cache pack! || true
           lake exe cache commit || true
-          # try twice in case of network errors
-          lake exe cache put || (sleep 1; lake exe cache put) || true
+          lake exe cache put || true
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -206,6 +206,7 @@ jobs:
           fi
 
       - name: build archive
+        id: archive
         run: |
           # Note: we should not be including `Archive` and `Countexamples` in the cache.
           # We do this for now for the sake of not rebuilding them in every CI run
@@ -214,19 +215,19 @@ jobs:
           # it should be possible to determine whether they need to be built without actually
           # storing and transferring oleans over the network.
           # Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
-          # We retry twice in case of network errors.
-          lake exe cache get Archive.lean || (sleep 1; lake exe cache get Archive.lean)
+          lake exe cache get Archive.lean
           lake build Archive
-          lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
+          lake exe cache put Archive.lean
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: build counterexamples
+        id: counterexamples
         run: |
-          lake exe cache get Counterexamples.lean || (sleep 1; lake exe cache get Counterexamples.lean)
+          lake exe cache get Counterexamples.lean
           lake build Counterexamples
-          lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
+          lake exe cache put Counterexamples.lean
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -241,6 +242,11 @@ jobs:
           lake exe graph
           rm import_graph.dot
 
+      - name: verify `lake exe shake` works
+        # Later, we may want to make output from `shake` a CI error?
+        run: |
+          lake exe shake
+
       - name: test mathlib
         id: test
         run: |
@@ -276,9 +282,12 @@ jobs:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
           GITHUB_CONTEXT: ${{ toJson(github) }}
           WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
+          BUILD_OUTCOME: ${{ steps.build.outcome }}
+          NOISY_OUTCOME: ${{ steps.noisy.outcome }}
+          ARCHIVE_OUTCOME: ${{ steps.archive.outcome }}
+          COUNTEREXAMPLE_OUTCOME: ${{ steps.counterexamples.outcome }}
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
-          BUILD_OUTCOME: ${{ steps.build.outcome }}
           CHECK_OUTCOME: ${{ steps.lean4checker.outcome }}
         run: |
           scripts/lean-pr-testing-comments.sh