refactor: generalize index repository CI

.github/workflows/ci.yml

@@ -11,18 +11,16 @@ on:
   # Enable running this workflow manually from the Actions tab
   workflow_dispatch:
     inputs:
-      index:
-        description: "What index to use"
-        type: choice
-        options:
-          # Use the current state of the index repository (i.e., reservoir-index)
-          - current
-          # Update the index repository and then use it
-          - updated
-          # Create and use a small local index artifact (e.g., for testing)
-          - local
-        required: true
-        default: current
+      index-repo:
+        description: "Registry index repository"
+        type: string
+        required: false
+        default: leanprover/reservoir-index
+      reindex:
+        description: "Reindex packages"
+        type: boolean
+        required: false
+        default: true
       toolchain:
         description: "Lean toolchain to test against"
         type: string
@@ -32,7 +30,7 @@ on:
         type: number
         required: false
       save-testbed:
-        description: "Save testbed results to reservoir-index"
+        description: "Save testbed results to index"
         type: boolean
         required: false
         default: true
@@ -47,11 +45,11 @@ permissions:
 jobs:
   index:
     name: Index
-    if: (!inputs.index || inputs.index != 'current')
+    if: (!inputs.index-repo || inputs.reindex)
     uses: ./.github/workflows/index.yaml
     secrets: inherit
     with:
-      update-index: ${{ inputs.index == 'updated' }}
+      repository: ${{ inputs.reindex && inputs.index-repo || '' }}
   testbed:
     needs: index
     # Run even if `index` is skipped
@@ -60,9 +58,9 @@ jobs:
     uses: ./.github/workflows/testbed.yaml
     secrets: inherit
     with:
-      index-artifact: ${{ !inputs.index || inputs.index == 'local' }}
-      toolchain: ${{ inputs.toolchain }}
+      index-repo: ${{ inputs.index-repo }}
       testbed-size: ${{ inputs.testbed-size || 0 }}
+      toolchain: ${{ inputs.toolchain }}
       update-index: ${{ inputs.save-testbed == true }}
   pages:
     needs: [index, testbed]
@@ -72,4 +70,5 @@ jobs:
     uses: ./.github/workflows/pages.yaml
     secrets: inherit
     with:
-      index-artifact: ${{ !inputs.index || inputs.index == 'local' }}
+      index-repo: ${{ inputs.index-repo }}
+      testbed-artifact: ${{ !(inputs.index-repo && inputs.save-testbed) }}

.github/workflows/index.yaml

@@ -7,49 +7,47 @@ on:
   # Enable running this workflow from ci.yml
   workflow_call:
     inputs:
-      update-index:
-        description: "Update reservoir-index"
-        type: boolean
+      repository:
+        description: "Registry index repository to update"
+        type: string
         required: false
-        default: false
   # Enable running this workflow manually from the Actions tab
   workflow_dispatch:
     inputs:
-      update-index:
-        description: "Update reservoir-index"
-        type: boolean
+      repository:
+        description: "Registry index repository to update"
+        type: string
         required: false
-        default: true
+        default: leanprover/reservoir-index
 
-# Permit only 1 concurrent update of the repository
-# and 1 concurrent artifact per branch, cancelling previous ones
+# Permit only 1 concurrent update of the same index repository, cancelling previous ones.
 concurrency:
-  group: ${{ inputs.update-index && 'index' || format('index/{0}', github.ref_name) }}
+  group: ${{ inputs.repository && format('index/{0}', inputs.repository) || github.run_id }}
   cancel-in-progress: true
 
 jobs:
   index:
-    name: ${{ inputs.update-index && 'Update' || 'Fetch'}}
+    name: ${{ inputs.repository && 'Update' || 'Fetch' }}
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
         uses: actions/checkout@v3
-      - name: Checkout External Index
-        if: inputs.update-index
+      - name: Checkout Index Repository
+        if: inputs.repository
         uses: actions/checkout@v3
         with:
           token: ${{ secrets.PUSH_RESERVOIR_INDEX_TOKEN }}
-          repository: leanprover/reservoir-index
+          repository: ${{ inputs.repository }}
           path: index
       - name: Query Repositories
         run: |
           ./query.py -v \
-            ${{ inputs.update-index && '-D index' || '-o index.json' }} \
-            -L ${{ (!inputs.update-index && github.ref_name != 'master') && 100 || 0 }}
+            ${{ inputs.repository && '-D index' || '-o index.json' }} \
+            -L ${{ (!inputs.repository && github.ref_name != 'master') && 100 || 0 }}
         env:
           GH_TOKEN: ${{ github.token }}
-      - name: Update External Index
-        if: inputs.update-index
+      - name: Update Index Repository
+        if: inputs.repository
         uses: EndBug/add-and-commit@v9
         with:
           cwd: index
@@ -60,7 +58,7 @@ jobs:
             ${{github.server_url}}/${{github.repository}}/actions/runs/${{github.run_id}}/attempts/${{github.run_attempt}}
           default_author: github_actions
       - name: Upload Index Artifact
-        if: (!inputs.update-index)
+        if: (!inputs.repository)
         uses: actions/upload-artifact@v3
         with:
           name: index

.github/workflows/pages.yaml

@@ -7,18 +7,23 @@ on:
   # Enable running this workflow from ci.yml
   workflow_call:
     inputs:
-      ci:
-        description: "Used to distinguish a CI workflow call from a standalone workflow"
-        type: boolean
+      index-repo:
+        description: "Registry index repository"
+        type: string
         required: false
-        default: true
-      index-artifact:
-        description: "Use local artifact, not reservoir-index"
+      testbed-artifact:
+        description: "Augment index with local testbed results"
         type: boolean
         required: false
         default: true
   # Enable running this workflow manually from the Actions tab
   workflow_dispatch:
+    inputs:
+      index-repo:
+        description: "Registry index repository"
+        type: string
+        required: true
+        default: leanprover/reservoir-index
 
 # Sets permissions of the GITHUB_TOKEN needed for deployment
 permissions:
@@ -27,11 +32,10 @@ permissions:
   pull-requests: write
   statuses: write
 
-# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued.
-# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete.
+# Allow only one concurrent deployment per commit, cancelling previous ones.
 concurrency:
-  group: pages
-  cancel-in-progress: false
+  group: pages/${{ github.sha }}
+  cancel-in-progress: true
 
 jobs:
   bundle:
@@ -40,31 +44,29 @@ jobs:
     steps:
       - name: Checkout
         uses: actions/checkout@v3
-      - name: Download Testbed Results (CI)
-        if: inputs.ci
+      - name: Download Testbed Artifact
+        if: inputs.testbed-artifact
         uses: actions/download-artifact@v3
         with:
           name: results
-      - name: Download Testbed Results (Standalone)
-        if: (!inputs.ci)
-        run: gh run download -n results
-        env:
-          GH_TOKEN: ${{ github.token }}
       - name: Download Index Artifact
-        if: inputs.index-artifact
+        if: (!inputs.index-repo)
         uses:  actions/download-artifact@v3
         with:
           name: index
       - name: Download Index Repository
-        if: (!inputs.index-artifact)
+        if: inputs.index-repo
         run: |
           mkdir index
-          gh api repos/leanprover/reservoir-index/tarball \
+          gh api repos/${{inputs.index-repo}}/tarball \
             | tar -xvz -C index --strip-component=1
         env:
           GH_TOKEN: ${{ github.token }}
       - name: Create Manifest
-        run: ./bundle.py ${{ inputs.index-artifact && 'index.json' || 'index' }} results.json -o manifest.json
+        run: |
+          ./bundle.py -o manifest.json \
+            ${{ inputs.index-repo && 'index' || 'index.json'}} \
+            ${{ inputs.testbed-artifact && 'results.json' || '' }}
         env:
           GH_TOKEN: ${{ github.token }}
       - name: Upload Manifest

.github/workflows/testbed.yaml

@@ -7,44 +7,48 @@ on:
   # Enable running this workflow from ci.yml
   workflow_call:
     inputs:
-      index-artifact:
-        description: "Use local artifact, not reservoir-index"
-        type: boolean
-        required: false
-        default: true
-      toolchain:
-        description: "Lean toolchain to test against"
+      index-repo:
+        description: "Registry index repository"
         type: string
         required: false
       testbed-size:
         description: "Number of packages to test"
         type: number
         required: false
+      toolchain:
+        description: "Lean toolchain to test against"
+        type: string
+        required: false
       update-index:
-        description: "Save to reservoir-index"
+        description: "Save to index"
         type: boolean
         required: false
         default: false
   # Enable running this workflow manually from the Actions tab
   workflow_dispatch:
     inputs:
-      toolchain:
-        description: "Lean toolchain to test against"
+      index-repo:
+        description: "Registry index repository"
         type: string
-        required: false
+        required: true
+        default: leanprover/reservoir-index
       testbed-size:
         description: "Number of packages to test"
         type: number
         required: false
+      toolchain:
+        description: "Lean toolchain to test against"
+        type: string
+        required: false
       update-index:
-        description: "Save to reservoir-index"
+        description: "Save to index"
         type: boolean
         required: false
         default: true
 
-# Permit only 1 concurrent run per branch, cancelling previous ones
+# Permit only 1 concurrent update of the same index repository, cancelling previous ones.
 concurrency:
-  group: testbed/${{ github.ref_name }}
+  group: ${{ inputs.update-index && format('testbed/{0}', inputs.index-repo) || github.run_id }}
   cancel-in-progress: true
 
 jobs:
@@ -66,22 +70,22 @@ jobs:
         env:
           GH_TOKEN: ${{ github.token }}
       - name: Download Index Artifact
-        if: inputs.index-artifact
+        if: (!inputs.index-repo)
         uses: actions/download-artifact@v3
         with:
           name: index
       - name: Download Index Repository
-        if: (!inputs.index-artifact)
+        if: inputs.index-repo
         run: |
           mkdir index
-          gh api repos/leanprover/reservoir-index/tarball \
+          gh api repos/${{inputs.index-repo}}/tarball \
             | tar -xvz -C index --strip-component=1
         env:
           GH_TOKEN: ${{ github.token }}
       - name: Create Matrix
         run: |
           ./testbed-create.py -o matrix.json \
-            ${{ inputs.index-artifact && 'index.json' || 'index' }} \
+            ${{ inputs.index-repo && 'index' || 'index.json' }} \
             ${{ inputs.toolchain || steps.find-toolchain.outputs.toolchain }}  \
             -n ${{inputs.testbed-size || (github.ref_name == 'master' && 200 || 15)}} \
             -X ${{github.ref_name == 'master' && 'testbed-exclusions.txt' || 'testbed-dev-exclusions.txt'}}
@@ -140,7 +144,7 @@ jobs:
         uses: actions/checkout@v3
         with:
           token: ${{ secrets.PUSH_RESERVOIR_INDEX_TOKEN }}
-          repository: leanprover/reservoir-index
+          repository: ${{ inputs.index-repo }}
           path: index
       - name: Download Individual Results
         uses: actions/download-artifact@v3