Prevent cache occupied by non-annotating jobs

utensil · Oct 6, 2024 · bbcd10c · bbcd10c
1 parent 7452b50
commit bbcd10c
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 19 deletions.
diff --git a/.github/workflows/aya.yml b/.github/workflows/aya.yml
@@ -19,7 +19,15 @@ jobs:
       fail-fast: false
     steps:
       - uses: actions/checkout@v4
+      - name: Should annotate
+        id: annotate
+        # annotation is enabled conditionally
+        if: >-
+          matrix.os == 'ubuntu-latest'
+        run: echo "annotate=true" >> "$GITHUB_OUTPUT"
       - name: Cache github-pages
+        if: >-
+          steps.annotate.outputs.annotate == 'true'
         uses: actions/cache@v4
         with:
             path: github-pages

diff --git a/.github/workflows/lean4.yml b/.github/workflows/lean4.yml
@@ -22,8 +22,6 @@ jobs:
       matrix:
         os: [ubuntu-latest, macos-latest, windows-latest]
       fail-fast: false
-    outputs:
-      deploy: ${{ steps.annotate.outputs.deploy }}
     steps:
       - name: install elan on Ubuntu and macOS
         if: matrix.os != 'windows-latest'
@@ -41,7 +39,18 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: recursive
+      - name: Should annotate
+        id: annotate
+        # annotation is enabled conditionally
+        if: >-
+          matrix.os == 'ubuntu-latest' && (
+            startsWith(github.ref, 'refs/heads/v4') ||
+            contains(github.event.head_commit.message, '[annotate]')
+          )
+        run: echo "annotate=true" >> "$GITHUB_OUTPUT"
       - name: Cache github-pages
+        if: >-
+          steps.annotate.outputs.annotate == 'true'
         uses: actions/cache@v4
         with:
             path: github-pages
@@ -61,13 +70,8 @@ jobs:
           lake exe cache get
           lake test
       - name: annotate examples
-        id: annotate
-        # annotation is enabled conditionally
         if: >-
-          matrix.os == 'ubuntu-latest' && (
-            startsWith(github.ref, 'refs/heads/v4') ||
-            contains(github.event.head_commit.message, '[annotate]')
-          )
+          steps.annotate.outputs.annotate == 'true'
         run: |
           cd lean4
           ./install_deps.sh
@@ -77,17 +81,6 @@ jobs:
           mkdir -p ./github-pages
           rm -rf ./github-pages/lean4
           mv ./lean4/dist ./github-pages/lean4
-          echo "deploy=true" >> "$GITHUB_OUTPUT"
-      # - name: Upload artifact
-      #   # Github Pages deployment is enabled conditionally
-      #   if: >-
-      #     matrix.os == 'ubuntu-latest' && (
-      #       startsWith(github.ref, 'refs/heads/v4') ||
-      #       contains(github.event.head_commit.message, '[annotate]')
-      #     )
-      #   uses: actions/upload-pages-artifact@v3
-      #   with:
-      #     path: ./lean4/dist
       - name: Try mk_all
         shell: bash
         run: |