feat: option to configure index for main CI

leanprover · Dec 2, 2023 · ceb6b9e · ceb6b9e
1 parent c6e310b
commit ceb6b9e
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 10 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -11,11 +11,18 @@ on:
   # Enable running this workflow manually from the Actions tab
   workflow_dispatch:
     inputs:
-      reuse-index:
-        description: "Use reservoir-index, not a new local artifact"
-        type: boolean
-        required: false
-        default: true
+      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
 
 # GITHUB_TOKEN permissions needed for deployment (copied from pages.yaml)
 permissions:
@@ -27,16 +34,18 @@ permissions:
 jobs:
   index:
     name: Index
-    if: (!inputs.reuse-index)
+    if: (inputs.index && inputs.index != 'current')
     uses: ./.github/workflows/index.yaml
+    with:
+      update-index: ${{ inputs.index == 'updated' }}
   testbed:
     needs: index
     # Run even if `index` is skipped
     if: (!failure() && !cancelled())
     name: Testbed
     uses: ./.github/workflows/testbed.yaml
     with:
-      index-artifact: ${{ !inputs.reuse-index }}
+      index-artifact: ${{ inputs.index && inputs.index == 'local' || false }}
   pages:
     needs: [index, testbed]
     # Run even if `index` is skipped
@@ -45,4 +54,4 @@ jobs:
     uses: ./.github/workflows/pages.yaml
     secrets: inherit
     with:
-      index-artifact: ${{ !inputs.reuse-index }}
+      index-artifact: ${{ inputs.index && inputs.index == 'local' || false }}
diff --git a/.github/workflows/index.yaml b/.github/workflows/index.yaml
@@ -6,6 +6,12 @@ on:
       - 'index/**' # branch pattern for query-only changes
   # Enable running this workflow from ci.yml
   workflow_call:
+    inputs:
+      update-index:
+        description: "Upadte reservoir-index"
+        type: boolean
+        required: false
+        default: false
   # Enable running this workflow manually from the Actions tab
   workflow_dispatch:
     inputs:
@@ -22,8 +28,8 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  fetch:
-    name: Refresh
+  index:
+    name: ${{ inputs.update-index && 'Update' || 'Fetch'}}
     runs-on: ubuntu-latest
     steps:
       - name: Checkout