fix: use proper index in standalone CI workflows

leanprover · Dec 13, 2023 · 5b27ab1 · 5b27ab1
1 parent 613e2b7
commit 5b27ab1
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 9 deletions.
diff --git a/.github/workflows/testbed.yml b/.github/workflows/testbed.yml
@@ -28,6 +28,11 @@ on:
         description: "Save to index"
         type: boolean
         required: false
+      ci:
+        description: "Distinguishes a workflow call from a standalone one"
+        type: boolean
+        required: false
+        default: true
   # Enable running this workflow manually from the Actions tab
   workflow_dispatch:
     inputs:
@@ -67,22 +72,22 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v3
       - name: Download Index Artifact
-        if: (!inputs.index-repo)
+        if: (inputs.ci && !inputs.index-repo)
         uses: actions/download-artifact@v3
         with:
           name: index
       - name: Download Index Repository
-        if: inputs.index-repo
+        if: (inputs.index-repo || !inputs.ci)
         run: |
           mkdir index
-          gh api repos/${{ inputs.index-repo }}/tarball \
+          gh api repos/${{ inputs.index-repo || 'leanprover/reservoir-index' }}/tarball \
             | tar -xvz -C index --strip-component=1
         env:
           GH_TOKEN: ${{ secrets.RESERVOIR_INDEX_TOKEN  }}
       - name: Create Matrix
         run: |
           ./testbed-create.py -o matrix.json \
-            ${{ inputs.index-repo && 'index' || 'index.json' }} \
+            ${{ (inputs.index-repo || !inputs.ci) && 'index' || 'index.json' }} \
             -e '${{ inputs.pattern || '.*' }}' \
             -t '${{ inputs.toolchain || 'package' }}'  \
             -n ${{ inputs.max-size == null && 10 || inputs.max-size }} \

diff --git a/.github/workflows/website.yml b/.github/workflows/website.yml
@@ -15,6 +15,11 @@ on:
         description: "Augment index with local testbed results"
         type: boolean
         required: false
+      ci:
+        description: "Distinguishes a workflow call from a standalone one"
+        type: boolean
+        required: false
+        default: true
   # Enable running this workflow manually from the Actions tab
   workflow_dispatch:
     inputs:
@@ -49,22 +54,22 @@ jobs:
         with:
           name: results
       - name: Download Index Artifact
-        if: (!inputs.index-repo)
+        if: (inputs.ci && !inputs.index-repo)
         uses:  actions/download-artifact@v3
         with:
           name: index
       - name: Download Index Repository
-        if: inputs.index-repo
+        if: (inputs.index-repo || !inputs.ci)
         run: |
           mkdir index
-          gh api repos/${{ inputs.index-repo }}/tarball \
+          gh api repos/${{ inputs.index-repo || 'leanprover/reservoir-index' }}/tarball \
             | tar -xvz -C index --strip-component=1
         env:
           GH_TOKEN: ${{ secrets.RESERVOIR_INDEX_TOKEN }}
       - name: Create Manifest
         run: |
           ./bundle.py -o manifest.json \
-            ${{ inputs.index-repo && 'index' || 'index.json'}} \
+            ${{ (inputs.index-repo || !inputs.ci) && 'index' || 'index.json'}} \
             ${{ inputs.testbed-artifact && 'results.json' || '' }}
         env:
           GH_TOKEN: ${{ github.token }}
@@ -94,10 +99,11 @@ jobs:
       - name: Build Site
         run: npm run generate
       - name: Download Index Repository
+        if: (inputs.index-repo || !inputs.ci)
         run: |
           set -eo pipefail
           mkdir .output/public/index
-          gh api repos/leanprover/reservoir-index/tarball \
+          gh api repos/${{ inputs.index-repo || 'leanprover/reservoir-index' }}/tarball \
             | tar -xvz -C .output/public/index --strip-component=1
           cp site/manifest.json .output/public/index/manifest.json
         env: