Testbed #6
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Testbed | |
| on: | |
| push: | |
| branches: | |
| - 'testbed/**' # branch pattern for testbed-only changes | |
| # Enable running this workflow from ci.ymld | |
| workflow_call: | |
| inputs: | |
| index-repo: | |
| description: "Registry index repository" | |
| type: string | |
| required: false | |
| index-artifact: | |
| description: "Use local artifact for index" | |
| type: boolean | |
| required: false | |
| default: false | |
| pattern: | |
| description: "Regex search for packages to test" | |
| type: string | |
| required: false | |
| toolchain: | |
| description: "Lean toolchain(s) to test against" | |
| type: string | |
| required: false | |
| max-size: | |
| description: "Max number of packages to test" | |
| type: number | |
| required: false | |
| default: 256 | |
| update-index: | |
| description: "Save to index" | |
| type: boolean | |
| required: false | |
| dev: | |
| description: "Optimize for development (uses dev-exclusions)" | |
| type: boolean | |
| required: false | |
| default: false | |
| # 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 | |
| pattern: | |
| description: "Regex search for packages to test" | |
| type: string | |
| required: true | |
| default: ".*" | |
| toolchain: | |
| description: "Lean toolchain(s) to test against" | |
| type: string | |
| required: false | |
| default: package | |
| max-size: | |
| description: "Max number of testbed entries" | |
| type: number | |
| required: true | |
| default: 10 | |
| update-index: | |
| description: "Save to index" | |
| type: boolean | |
| required: false | |
| default: false | |
| jobs: | |
| setup: | |
| name: Setup | |
| runs-on: ubuntu-latest | |
| outputs: | |
| matrix: ${{ steps.output-matrix.outputs.matrix }} | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Download Index Artifact | |
| if: inputs.index-artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: index | |
| path: index | |
| - name: Download Index Repository | |
| if: (!inputs.index-artifact) | |
| run: | | |
| mkdir index | |
| 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: | | |
| scripts/testbed-create.py index -o matrix.json \ | |
| -e '${{ inputs.pattern || '.*' }}' \ | |
| -t '${{ inputs.toolchain || 'package' }}' \ | |
| -n ${{ inputs.max-size == null && 10 || inputs.max-size }} \ | |
| -X ${{ inputs.dev && 'scripts/testbed-dev-exclusions.txt' || 'scripts/testbed-exclusions.txt' }} | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| - name: Upload Matrix | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: matrix | |
| path: matrix.json | |
| if-no-files-found: error | |
| - id: output-matrix | |
| name: Output Matrix | |
| run: (echo -n 'matrix='; cat matrix.json) >> "$GITHUB_OUTPUT" | |
| build: | |
| needs: setup | |
| name: Build ${{ matrix.buildName }} | |
| runs-on: ubuntu-latest | |
| # This job runs arbitrary untrusted code, so we need to harden permissions | |
| permissions: | |
| contents: read | |
| strategy: | |
| matrix: | |
| include: ${{ fromJson(needs.setup.outputs.matrix) }} | |
| # complete all jobs | |
| fail-fast: false | |
| continue-on-error: true # e.g., upload/download failures | |
| steps: | |
| - name: Install Elan | |
| shell: bash -euo pipefail {0} | |
| run: | | |
| curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ | |
| | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| with: | |
| persist-credentials: false | |
| - id: build | |
| name: Build | |
| continue-on-error: true # e.g., clone failures | |
| # We run arbitrary untrusted code here | |
| run: | | |
| scripts/testbed-build.py -v -o result.json \ | |
| ${{ matrix.gitUrl }} -t ${{ matrix.toolchains }} | |
| - name: Upload Result | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: ${{ matrix.artifact }} | |
| path: result.json | |
| collect: | |
| needs: build | |
| name: Collect Results | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Download Individual Results | |
| uses: actions/download-artifact@v4 | |
| with: | |
| # Without a name, downloads all artifacts | |
| path: testbed | |
| - name: Collect Outcomes | |
| run: | | |
| scripts/testbed-collect.py -o testbed/results.json -v \ | |
| testbed ${{ github.run_id }} ${{ github.run_attempt }} | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| - name: Upload Results Artifact | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: results | |
| path: testbed/results.json | |
| if-no-files-found: error | |
| save: | |
| needs: collect | |
| name: Save Results | |
| runs-on: ubuntu-latest | |
| # Permit only 1 concurrent update of the same index repository. | |
| concurrency: | |
| group: ${{ inputs.update-index && format('update-index/{0}', inputs.index-repo) || format('index/{0}', github.run_id) }} | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Download Index Artifact | |
| if: inputs.index-artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: index | |
| path: index | |
| - name: Checkout External Index | |
| if: (!inputs.index-artifact) | |
| uses: actions/checkout@v4 | |
| with: | |
| token: ${{ secrets.RESERVOIR_INDEX_TOKEN }} | |
| repository: ${{ inputs.index-repo }} | |
| path: index | |
| - name: Download Results Artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: results | |
| - name: Write Results to Index | |
| run: scripts/testbed-save.py -v results.json index | |
| env: | |
| GH_TOKEN: ${{ secrets.RESERVOIR_INDEX_TOKEN }} | |
| - name: Update External Index | |
| if: inputs.update-index | |
| uses: EndBug/add-and-commit@v9 | |
| with: | |
| cwd: index | |
| fetch: false | |
| message: | | |
| chore: update w/ testbed run results | |
| ${{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) | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: index | |
| path: index | |
| if-no-files-found: error | |
| overwrite: true |