Testbed #44
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.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" | |
| type: string | |
| required: false | |
| testbed-size: | |
| description: "Number of packages to test" | |
| type: number | |
| required: false | |
| update-index: | |
| description: "Save to reservoir-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" | |
| type: string | |
| required: false | |
| testbed-size: | |
| description: "Number of packages to test" | |
| type: number | |
| required: false | |
| update-index: | |
| description: "Save to reservoir-index" | |
| type: boolean | |
| required: false | |
| default: true | |
| # Permit only 1 concurrent run per branch, cancelling previous ones | |
| concurrency: | |
| group: testbed/${{ github.ref_name }} | |
| cancel-in-progress: true | |
| jobs: | |
| setup: | |
| name: Setup | |
| runs-on: ubuntu-latest | |
| outputs: | |
| matrix: ${{ steps.output-matrix.outputs.matrix }} | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v3 | |
| - id: find-toolchain | |
| name: Find Latest Toolchain | |
| if: (!inputs.toolchain) | |
| shell: bash -euo pipefail {0} | |
| run: | | |
| latest=$(gh release list -R leanprover/lean4 -L 1 | cut -f1) | |
| echo "toolchain=leanprover/lean4:$latest" >> "$GITHUB_OUTPUT" | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| - name: Download Index Artifact | |
| if: inputs.index-artifact | |
| uses: actions/download-artifact@v3 | |
| with: | |
| name: index | |
| - name: Download Index Repository | |
| if: (!inputs.index-artifact) | |
| run: | | |
| mkdir index | |
| gh api repos/leanprover/reservoir-index/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.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'}} | |
| - name: Upload Matrix | |
| uses: actions/upload-artifact@v3 | |
| 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.fullName }} | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| include: ${{ fromJson(needs.setup.outputs.matrix) }} | |
| # complete all jobs | |
| fail-fast: false | |
| 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 ${{ matrix.toolchain }} | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Check Lean | |
| run: lean --version | |
| - name: Checkout | |
| uses: actions/checkout@v3 | |
| - id: build | |
| name: Build | |
| continue-on-error: true | |
| # Note that this runs arbitrary untrusted code so we cannot give it secrets | |
| run: ./build.sh ${{ matrix.gitUrl }} testbed ${{ matrix.toolchain }} | |
| - name: Output Outcome | |
| run: | | |
| echo ${{ steps.build.outcome }} > outcome.txt | |
| - name: Upload Results | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: ${{ matrix.artifact }} | |
| path: outcome.txt | |
| collect: | |
| needs: [setup, build] | |
| name: Collect Results | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v3 | |
| - name: Checkout External Index | |
| if: inputs.update-index | |
| uses: actions/checkout@v3 | |
| with: | |
| token: ${{ secrets.PUSH_RESERVOIR_INDEX_TOKEN }} | |
| repository: leanprover/reservoir-index | |
| path: index | |
| - name: Download Individual Results | |
| uses: actions/download-artifact@v3 | |
| with: | |
| # Without a name, downloads all artifacts | |
| path: testbed | |
| - name: Collect Outcomes | |
| run: | | |
| ./testbed-collect.py \ | |
| testbed ${{ github.run_id }} ${{ github.run_attempt }} \ | |
| -o testbed/results.json ${{ inputs.update-index && '-D index' || '' }} | |
| env: | |
| GH_TOKEN: ${{ github.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 Results Artifact | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: results | |
| path: testbed/results.json | |
| if-no-files-found: error |