refactor: testbed: do not upload pkg build dirs #43
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: | |
| ci: | |
| description: 'Used to dinstinguish a CI workflow call from a standalone workflow' | |
| type: boolean | |
| required: false | |
| default: true | |
| # Enable running this workflow manually from the Actions tab | |
| workflow_dispatch: | |
| inputs: | |
| toolchain: | |
| description: "The Lean toolchain to test against" | |
| type: string | |
| required: false | |
| repositories: | |
| description: "The number of repositories to test" | |
| type: number | |
| required: false | |
| # 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 }} | |
| toolchain: ${{ inputs.toolchain || steps.find-toolchain.outputs.toolchain }} | |
| 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 (CI) | |
| if: inputs.ci | |
| uses: actions/download-artifact@v3 | |
| with: | |
| name: index | |
| - name: Download Index (Standalone) | |
| if: (!inputs.ci) | |
| run: gh run download -n index | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| - name: Create Matrix | |
| run: | | |
| ./testbed-create.py index.json -o matrix.json \ | |
| -n ${{inputs.repositories || (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 ${{ needs.setup.outputs.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.url }} testbed ${{ needs.setup.outputs.toolchain }} | |
| - name: Output Outcome | |
| run: | | |
| echo ${{ steps.build.outcome }} > outcome.txt | |
| - name: Upload Results | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: ${{ matrix.id }} | |
| path: outcome.txt | |
| collect: | |
| needs: [setup, build] | |
| name: Collect Results | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v3 | |
| - 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 ${{ needs.setup.outputs.toolchain }} ${{ github.run_id }} -o testbed/results.json | |
| - name: Upload Results | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: results | |
| path: testbed/results.json | |
| if-no-files-found: error |