Use cache to pass built artifacts for Github Pages

utensil · Oct 6, 2024 · bf36cef · bf36cef
1 parent 7e7a832
commit bf36cef
Show file tree

Hide file tree

Showing 4 changed files with 40 additions and 22 deletions.
diff --git a/.github/workflows/aya.yml b/.github/workflows/aya.yml
@@ -19,6 +19,11 @@ jobs:
       fail-fast: false
     steps:
       - uses: actions/checkout@v4
+      - name: Cache github-pages
+        uses: actions/cache@v4
+        with:
+            path: github-pages
+            key: github-pages
       - uses: extractions/setup-just@v1
         with:
           just-version: 1.35.0
@@ -42,10 +47,10 @@ jobs:
             cd aya
             just test
       - name: Generate documentation
+        if: >-
+          matrix.os == 'ubuntu-latest'
         run: |
             cd aya
             just doc
-      - name: Upload artifact
-        uses: actions/upload-pages-artifact@v3
-        with:
-          path: ./aya/dist
+            cd ..
+            mv ./aya/dist ./github-pages/aya
diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml
@@ -32,15 +32,20 @@ jobs:
       url: ${{ steps.deployment.outputs.page_url }}
     runs-on: ubuntu-latest
     steps:
-        - name: Download GitHub Pages artifact
-          uses: actions/download-artifact@v4
+        # - name: Download GitHub Pages artifact
+        #   uses: actions/download-artifact@v4
+        #   with:
+        #     name: github-pages
+        #     path: github-pages
+        #     github-token: ${{ secrets.GITHUB_TOKEN }}
+        #     run-id: ${{ github.event.workflow_run.id }}
+        - name: Cache github-pages
+          uses: actions/cache@v4
           with:
-            name: github-pages
-            path: github-pages
-            github-token: ${{ secrets.GITHUB_TOKEN }}
-            run-id: ${{ github.event.workflow_run.id }}
+              path: github-pages
+              key: github-pages
         - name: Display structure of downloaded files
-          run: ls -R
+          run: ls -R github-pages
     #   - name: Deploy to GitHub Pages
     #     id: deployment
     #     # Github Pages deployment is enabled conditionally

diff --git a/.github/workflows/lean4.yml b/.github/workflows/lean4.yml
@@ -47,6 +47,11 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: recursive
+      - name: Cache github-pages
+        uses: actions/cache@v4
+        with:
+            path: github-pages
+            key: github-pages
       - name: Install Python
         uses: actions/setup-python@v5
         with:
@@ -72,17 +77,20 @@ jobs:
           ./install_deps.sh
           ./annotate_all.sh
           # lake env leanInk analyze examples/Help.lean
+          cd ..
+          mkdir -p ./github-pages
+          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: 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: |

diff --git a/aya/justfile b/aya/justfile
@@ -12,4 +12,4 @@ test:
 
 doc:
     mkdir -p dist
-    aya literate.aya.md --pretty-format=html -o dist/literate.aya.html
+    -aya literate.aya.md --pretty-format=html -o dist/literate.aya.html