Update lean-toolchain for testing https://github.com/leanprover/lean4… #61239
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
| # 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. | |
| # Forks of mathlib and other projects should be able to use build_fork.yml directly | |
| # The jobs in this file run on self-hosted workers and will not be run from external forks | |
| on: | |
| push: | |
| branches-ignore: | |
| # ignore tmp branches used by bors | |
| - 'staging.tmp*' | |
| - 'trying.tmp*' | |
| - 'staging*.tmp' | |
| - 'nolints' | |
| # ignore staging branch used by bors, this is handled by bors.yml | |
| - 'staging' | |
| merge_group: | |
| name: continuous integration | |
| jobs: | |
| # Cancels previous runs of jobs in this file | |
| cancel: | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| name: 'Cancel Previous Runs (CI)' | |
| runs-on: ubuntu-latest | |
| # timeout-minutes: 3 | |
| steps: | |
| - uses: styfle/cancel-workflow-action@0.11.0 | |
| with: | |
| all_but_latest: true | |
| access_token: ${{ github.token }} | |
| style_lint: | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| name: Lint style | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: cleanup | |
| run: | | |
| find . -name . -o -prune -exec rm -rf -- {} + | |
| - uses: actions/checkout@v3 | |
| # Run the case checker action | |
| - name: Check Case Sensitivity | |
| uses: credfeto/action-case-checker@v1.3.0 | |
| - name: Look for ignored files | |
| uses: credfeto/action-no-ignored-files@v1.1.0 | |
| - name: install Python | |
| if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }} | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: 3.8 | |
| - name: lint | |
| run: | | |
| ./scripts/lint-style.sh | |
| - name: Install bibtool | |
| if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }} | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y bibtool | |
| - name: lint references.bib | |
| run: | | |
| ./scripts/lint-bib.sh | |
| check_imported: | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| name: Check all files imported | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: cleanup | |
| run: | | |
| find . -name . -o -prune -exec rm -rf -- {} + | |
| - uses: actions/checkout@v3 | |
| - name: update Mathlib.lean | |
| run: | | |
| git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean | |
| - name: update MathlibExtras.lean | |
| run: | | |
| git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean | |
| - name: update Mathlib/Tactic.lean | |
| run: | | |
| git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean | |
| - name: update Counterexamples.lean | |
| run: | | |
| git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean | |
| - name: update Archive.lean | |
| run: | | |
| git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean | |
| - name: check that all files are imported | |
| run: git diff --exit-code | |
| check_workflows: | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| name: check workflows | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: cleanup | |
| run: | | |
| find . -name . -o -prune -exec rm -rf -- {} + | |
| - uses: actions/checkout@v3 | |
| - name: update workflows | |
| run: | | |
| cd .github/workflows/ | |
| ./mk_build_yml.sh | |
| - name: check that workflows were consistent | |
| run: git diff --exit-code | |
| build: | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| name: Build | |
| runs-on: pr | |
| steps: | |
| - name: cleanup | |
| run: | | |
| find . -name . -o -prune -exec rm -rf -- {} + | |
| # Delete all but the 5 most recent toolchains. | |
| # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file. | |
| # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`. | |
| cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true | |
| # The Hoskinson runners may not have jq installed, so do that now. | |
| - name: 'Setup jq' | |
| uses: dcarbone/install-jq-action@v1.0.1 | |
| - name: install elan | |
| run: | | |
| set -o pipefail | |
| curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz | |
| ./elan-init -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - uses: actions/checkout@v3 | |
| # We update `Mathlib.lean` as a convenience here, | |
| # but verify that this didn't change anything in the `check_imported` job. | |
| - name: update Mathlib.lean | |
| run: | | |
| find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean | |
| - name: If using a lean-pr-release toolchain, uninstall | |
| run: | | |
| if [[ `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then | |
| echo "Uninstalling transient toolchain `cat lean-toolchain`" | |
| elan toolchain uninstall `cat lean-toolchain` | |
| fi | |
| - name: print lean and lake versions | |
| run: | | |
| lean --version | |
| lake --version | |
| - name: get cache | |
| run: | | |
| lake exe cache clean | |
| # We've been seeing many failures at this step recently because of network errors. | |
| # As a band-aid, we try twice. | |
| # The 'sleep 1' is small pause to let the network recover. | |
| lake exe cache get || (sleep 1; lake exe cache get) | |
| - name: build mathlib | |
| id: build | |
| uses: liskin/gh-problem-matcher-wrap@v2 | |
| with: | |
| linters: gcc | |
| run: | | |
| bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log" | |
| - name: check for noisy stdout lines | |
| run: | | |
| ! grep --after-context=1 "stdout:" stdout.log | |
| - name: build library_search cache | |
| run: lake build -KCI MathlibExtras | |
| - name: upload cache | |
| if: always() | |
| run: | | |
| # run this in CI if it gets an incorrect lake hash for existing cache files somehow | |
| # lake exe cache pack! || true | |
| lake exe cache commit || true | |
| # try twice in case of network errors | |
| lake exe cache put || (sleep 1; lake exe cache put) || true | |
| env: | |
| MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} | |
| - name: check the cache | |
| run: | | |
| # Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place" | |
| # the cache mechanism is unreliable, so we don't test it if we are on such a branch. | |
| if [[ ! `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then | |
| lake exe cache get || (sleep 1; lake exe cache get) | |
| # We pipe the output of `lake build` to a file, | |
| # and if we find " Building Mathlib" in that file we kill `lake build`, and error. | |
| lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! )) | |
| fi | |
| - name: build archive | |
| run: | | |
| # Note: we should not be including `Archive` and `Countexamples` in the cache. | |
| # We do this for now for the sake of not rebuilding them in every CI run | |
| # even when they are not touched. | |
| # Since `Archive` and `Counterexamples` files have very simple dependencies, | |
| # it should be possible to determine whether they need to be built without actually | |
| # storing and transferring oleans over the network. | |
| # Hopefully a future re-implementation of `cache` will obviate the present need for this hack. | |
| # We retry twice in case of network errors. | |
| lake exe cache get Archive.lean || (sleep 1; lake exe cache get Archive.lean) | |
| lake build Archive | |
| lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean) | |
| env: | |
| MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} | |
| - name: build counterexamples | |
| run: | | |
| lake exe cache get Counterexamples.lean || (sleep 1; lake exe cache get Counterexamples.lean) | |
| lake build Counterexamples | |
| lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean) | |
| env: | |
| MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} | |
| - name: check declarations in db files | |
| run: | | |
| python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml | |
| lake exe checkYaml | |
| - name: verify `lake exe graph` works | |
| run: | | |
| lake exe graph | |
| rm import_graph.dot | |
| - name: test mathlib | |
| id: test | |
| run: | | |
| # Tests use parts of ProofWidgets not imported by Mathlib. | |
| # Ensure everything has been built. | |
| lake build ProofWidgets | |
| make -j 8 test | |
| - name: lint mathlib | |
| id: lint | |
| uses: liskin/gh-problem-matcher-wrap@v2 | |
| with: | |
| linters: gcc | |
| run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib | |
| - name: check environments using lean4checker | |
| id: lean4checker | |
| run: | | |
| git clone https://github.com/leanprover/lean4checker | |
| cd lean4checker | |
| git checkout toolchain/v4.3.0 | |
| # Now that the git hash is embedded in each olean, | |
| # we need to compile lean4checker on the same toolchain | |
| cp ../lean-toolchain . | |
| lake build | |
| ./test.sh | |
| cd .. | |
| lake env lean4checker/.lake/build/bin/lean4checker | |
| - name: Post comments for lean-pr-testing branch | |
| if: always() | |
| env: | |
| TOKEN: ${{ secrets.LEAN_PR_TESTING }} | |
| GITHUB_CONTEXT: ${{ toJson(github) }} | |
| WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }} | |
| LINT_OUTCOME: ${{ steps.lint.outcome }} | |
| TEST_OUTCOME: ${{ steps.test.outcome }} | |
| BUILD_OUTCOME: ${{ steps.build.outcome }} | |
| CHECK_OUTCOME: ${{ steps.lean4checker.outcome }} | |
| run: | | |
| scripts/lean-pr-testing-comments.sh | |
| final: | |
| name: Post-CI job | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| needs: [style_lint, build, check_imported] | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v3 | |
| - id: PR | |
| uses: 8BitJonny/gh-get-current-pr@2.2.0 | |
| # TODO: this may not work properly if the same commit is pushed to multiple branches: | |
| # https://github.com/8BitJonny/gh-get-current-pr/issues/8 | |
| with: | |
| github-token: ${{ secrets.GITHUB_TOKEN }} | |
| # Only return if PR is still open | |
| filterOutClosed: true | |
| - id: remove_labels | |
| name: Remove "awaiting-CI" | |
| # we use curl rather than octokit/request-action so that the job won't fail | |
| # (and send an annoying email) if the labels don't exist | |
| run: | | |
| curl --request DELETE \ | |
| --url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \ | |
| --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' | |
| - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') | |
| name: If `auto-merge-after-CI` is present, add a `bors merge` comment. | |
| uses: GrantBirki/comment@v2.0.1 | |
| with: | |
| token: ${{ secrets.AUTO_MERGE_TOKEN }} | |
| issue-number: ${{ steps.PR.outputs.number }} | |
| body: | | |
| As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors: | |
| bors merge |