Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
perf(ci): use self-hosted runner for bors (#8024)
Run CI builds for the `staging` branch used by bors on a self-hosted github actions runner. This runner has been graciously provided by Johan Commelin's DFG grant and is hosted at the Albert-Ludwigs-Universität Freiburg. We need to use two github actions workflow files to use a separate runner for the `staging` branch: `build.yml` and `bors.yml`. These are almost identical, except for the `runs-on:` property indicating which runner should be used. The shell script `mk_build_yml.sh` is therefore used to generate both files from the common template `build.yml.in`.
- Loading branch information
Showing
5 changed files
with
488 additions
and
24 deletions.
There are no files selected for viewing
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,196 @@ | ||
| # DO NOT EDIT THIS FILE!!! | ||
|
|
||
| # This file is automatically generated by mk_build_yml.sh | ||
| # Edit build.yml.in instead and run mk_build_yml.sh to update. | ||
|
|
||
| on: | ||
| push: | ||
| branches: | ||
| - staging | ||
|
|
||
| name: continuous integration | ||
|
|
||
| jobs: | ||
|
|
||
| # Cancels previous runs of jobs in this file | ||
| cancel: | ||
| name: 'Cancel Previous Runs (CI)' | ||
| runs-on: ubuntu-latest | ||
| # timeout-minutes: 3 | ||
| steps: | ||
| - uses: styfle/cancel-workflow-action@0.9.0 | ||
| with: | ||
| all_but_latest: true | ||
| access_token: ${{ github.token }} | ||
|
|
||
| style_lint: | ||
| name: Lint style | ||
| runs-on: self-hosted | ||
| steps: | ||
| - uses: actions/checkout@v2 | ||
|
|
||
| - name: install Python | ||
| if: ${{ ! 1 }} | ||
| uses: actions/setup-python@v2 | ||
| with: | ||
| python-version: 3.8 | ||
|
|
||
| - name: lint | ||
| run: | | ||
| ./scripts/lint-style.sh | ||
| build: | ||
| name: Build mathlib | ||
| runs-on: self-hosted | ||
| env: | ||
| # number of commits to check for olean cache | ||
| GIT_HISTORY_DEPTH: 20 | ||
| outputs: | ||
| artifact_name: ${{ steps.setup_precompiled.outputs.artifact_name }} | ||
| steps: | ||
| - uses: actions/checkout@v2 | ||
| with: | ||
| fetch-depth: ${{ env.GIT_HISTORY_DEPTH }} | ||
|
|
||
| - name: install elan | ||
| run: | | ||
| set -o pipefail | ||
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y | ||
| ~/.elan/bin/lean --version | ||
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | ||
| echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV | ||
| - name: install Python | ||
| if: ${{ ! 1 }} | ||
| uses: actions/setup-python@v1 | ||
| with: | ||
| python-version: 3.8 | ||
|
|
||
| - name: try to find olean cache | ||
| run: ./scripts/fetch_olean_cache.sh | ||
|
|
||
| - name: leanpkg build | ||
| id: build | ||
| run: | | ||
| leanpkg configure | ||
| echo "::set-output name=started::true" | ||
| lean --json -T100000 --make src | python scripts/detect_errors.py | ||
| lean --json -T100000 --make src | python scripts/detect_errors.py | ||
| - name: push release to azure | ||
| if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true' | ||
| run: | | ||
| archive_name="$(git rev-parse HEAD).tar.gz" | ||
| find src/ -name "*.olean" -o -name ".noisy_files" | tar czf "$archive_name" -T - | ||
| azcopy copy "$archive_name" "${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false | ||
| archive_name="$(git rev-parse HEAD).tar.xz" | ||
| find src/ -name "*.olean" -o -name ".noisy_files" | tar cJf "$archive_name" -T - | ||
| azcopy copy "$archive_name" "${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false | ||
| - name: setup precompiled zip file | ||
| if: always() && steps.build.outputs.started == 'true' | ||
| id: setup_precompiled | ||
| run: | | ||
| touch workspace.tar | ||
| tar -cf workspace.tar --exclude=*.tar* . | ||
| git_hash="$(git log -1 --pretty=format:%h)" | ||
| echo "::set-output name=artifact_name::precompiled-mathlib-$short_lean_version-$git_hash" | ||
| - name: upload precompiled mathlib zip file | ||
| if: always() && steps.build.outputs.started == 'true' | ||
| uses: actions/upload-artifact@v2 | ||
| with: | ||
| name: ${{ steps.setup_precompiled.outputs.artifact_name }} | ||
| path: workspace.tar | ||
|
|
||
| lint: | ||
| name: Lint mathlib | ||
| runs-on: self-hosted | ||
| needs: build | ||
|
|
||
| # skip on master branch | ||
| if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master' | ||
|
|
||
| steps: | ||
| - name: retrieve build | ||
| uses: actions/download-artifact@v2 | ||
| with: | ||
| name: ${{ needs.build.outputs.artifact_name }} | ||
|
|
||
| - name: untar build | ||
| run: tar -xf workspace.tar | ||
|
|
||
| - name: install elan | ||
| run: | | ||
| set -o pipefail | ||
| curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y | ||
| ~/.elan/bin/lean --version | ||
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | ||
| - name: lint | ||
| run: | | ||
| ./scripts/mk_all.sh | ||
| lean --run scripts/lint_mathlib.lean | ||
| tests: | ||
| name: Run tests | ||
| runs-on: self-hosted | ||
| needs: build | ||
|
|
||
| # skip on master branch | ||
| if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master' | ||
|
|
||
| steps: | ||
| - name: retrieve build | ||
| uses: actions/download-artifact@v2 | ||
| with: | ||
| name: ${{ needs.build.outputs.artifact_name }} | ||
|
|
||
| - name: untar build | ||
| run: tar -xf workspace.tar | ||
|
|
||
| - name: install elan | ||
| run: | | ||
| set -o pipefail | ||
| curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y | ||
| ~/.elan/bin/lean --version | ||
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | ||
| - name: install Python | ||
| if: ${{ ! 1 }} | ||
| uses: actions/setup-python@v1 | ||
| with: | ||
| python-version: 3.8 | ||
|
|
||
| - name: install Python dependencies | ||
| if: ${{ ! 1 }} | ||
| run: python -m pip install --upgrade pip pyyaml | ||
|
|
||
| - name: tests | ||
| run: | | ||
| set -o pipefail | ||
| lean --json -T100000 --make docs archive roadmap test counterexamples | python scripts/detect_errors.py | ||
| - uses: actions/setup-java@v2 | ||
| if: ${{ ! 1 }} | ||
| with: | ||
| distribution: 'adopt' | ||
| java-version: '16' | ||
|
|
||
| - name: install trepplein | ||
| run: | | ||
| trepplein_version=1.0 | ||
| wget https://github.com/gebner/trepplein/releases/download/v$trepplein_version/trepplein-$trepplein_version.zip | ||
| unzip trepplein-$trepplein_version.zip | ||
| echo $PWD/trepplein-$trepplein_version/bin >>$GITHUB_PATH | ||
| - name: export as low-level text file | ||
| run: lean --recursive --export=mathlib.txt src/ | ||
|
|
||
| - name: trepplein | ||
| run: trepplein mathlib.txt | ||
|
|
||
| - name: check declarations in db files | ||
| run: | | ||
| python scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml | ||
| bash scripts/mk_all.sh | ||
| lean --run scripts/yaml_check.lean |
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
Oops, something went wrong.