This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
doc: Add a warning mentioning Lean 4 to the readme (#19243) #81598
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 GitHub-hosted workers and will only be run from external forks | |
| on: | |
| push: | |
| branches-ignore: | |
| # ignore tmp branches used by bors | |
| - 'staging.tmp*' | |
| - 'trying.tmp*' | |
| - 'staging*.tmp' | |
| - 'nolints' | |
| # do not build lean-x.y.z branch used by leanpkg | |
| - 'lean-3.*' | |
| name: continuous integration (mathlib forks) | |
| jobs: | |
| # Cancels previous runs of jobs in this file | |
| cancel: | |
| if: github.repository != 'leanprover-community/mathlib' | |
| 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/mathlib' | |
| name: Lint style (fork) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v3 | |
| - name: Install bibtool | |
| if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }} | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y bibtool | |
| - name: install Python | |
| if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }} | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: 3.8 | |
| - name: lint style | |
| run: | | |
| ./scripts/lint-style.sh | |
| - name: lint references.bib | |
| run: | | |
| ./scripts/lint-bib.sh | |
| build: | |
| if: github.repository != 'leanprover-community/mathlib' | |
| name: Build mathlib (fork) | |
| runs-on: ubuntu-latest | |
| 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@v3 | |
| 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: ${{ ! 0 }} | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: 3.8 | |
| - name: try to find olean cache | |
| run: ./scripts/fetch_olean_cache.sh | |
| - name: leanpkg build | |
| id: build | |
| run: | | |
| set -o pipefail | |
| leanpkg configure | |
| echo "started=true" >> $GITHUB_OUTPUT | |
| lean --json -T100000 --make src | python3 scripts/detect_errors.py | |
| lean --json -T400000 --make src | python3 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 "artifact_name=precompiled-mathlib-$short_lean_version-$git_hash" >> $GITHUB_OUTPUT | |
| - 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 | |
| - name: cleanup after upload step | |
| # cf. https://github.com/actions/upload-artifact/issues/256 | |
| if: always() && steps.build.outputs.started == 'true' && ${{ 0 }} | |
| run: rm /tmp/tmp-* || true | |
| - name: clean up working directory and elan | |
| if: always() && ${{ 0 }} | |
| run: rm -rf * $HOME/.elan | |
| lint: | |
| name: Lint mathlib (fork) | |
| runs-on: ubuntu-latest | |
| needs: build | |
| # skip on master branch | |
| if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master' | |
| steps: | |
| - name: clean build directory | |
| if: ${{ 0 }} | |
| run: rm -rf ./* ./.??* | |
| - name: retrieve build | |
| uses: actions/download-artifact@v3 | |
| 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/leanprover/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 --github | |
| - name: clean up working directory and elan | |
| if: always() && ${{ 0 }} | |
| run: rm -rf * $HOME/.elan | |
| tests: | |
| name: Run tests (fork) | |
| runs-on: ubuntu-latest | |
| needs: build | |
| # skip on master branch | |
| if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master' | |
| steps: | |
| - name: clean build directory | |
| if: ${{ 0 }} | |
| run: rm -rf ./* ./.??* | |
| - name: retrieve build | |
| uses: actions/download-artifact@v3 | |
| 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/leanprover/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: ${{ ! 0 }} | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: 3.8 | |
| - name: install Python dependencies | |
| if: ${{ ! 0 }} | |
| run: python3 -m pip install --upgrade pip pyyaml requests mathlibtools | |
| - name: tests | |
| run: | | |
| set -o pipefail | |
| lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py | |
| - name: check archive and counterexample directories have unique identifiers | |
| run: | | |
| pip install mathlibtools | |
| (cd archive && python -m mathlibtools.leanproject mk-all && mv all.lean archive_all.lean) | |
| (cd counterexamples && python -m mathlibtools.leanproject mk-all && mv all.lean counterexamples_all.lean) | |
| python -m mathlibtools.leanproject mk-all | |
| echo "import all" >> all_all.lean | |
| echo "import counterexamples_all" >> all_all.lean | |
| echo "import archive_all" >> all_all.lean | |
| echo "path ./archive" >> leanpkg.path | |
| echo "path ./counterexamples" >> leanpkg.path | |
| lean --json -T100000 --make all_all.lean | python3 scripts/detect_errors.py | |
| - uses: actions/setup-java@v2 | |
| if: ${{ ! 0 }} | |
| with: | |
| distribution: 'adopt' | |
| java-version: '16' | |
| - name: install trepplein | |
| run: | | |
| trepplein_version=1.1 | |
| 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: | | |
| python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml | |
| bash scripts/mk_all.sh | |
| lean --run scripts/yaml_check.lean | |
| - name: clean up working directory and elan | |
| if: always() && ${{ 0 }} | |
| run: rm -rf * $HOME/.elan | |
| final: | |
| name: Post-CI job (fork) | |
| if: github.repository != 'leanprover-community/mathlib' | |
| needs: [style_lint, build, lint, tests] | |
| 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 }}' |