This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Snapshot #121017
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: continuous integration | |
| 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.*' | |
| jobs: | |
| style_lint: | |
| name: Lint style | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - name: install Python | |
| uses: actions/setup-python@v1 | |
| with: | |
| python-version: 3.8 | |
| - name: lint | |
| run: | | |
| ./scripts/lint-copy-mod-doc.sh | |
| build: | |
| name: Build mathlib | |
| 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@v2 | |
| with: | |
| fetch-depth: ${{ env.GIT_HISTORY_DEPTH }} | |
| - 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 | |
| echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV | |
| - name: install azcopy | |
| run: | | |
| cd /usr/local/bin | |
| wget -q https://aka.ms/downloadazcopy-v10-linux -O - | sudo tar zxf - --strip-components 1 --wildcards '*/azcopy' | |
| sudo chmod 755 /usr/local/bin/azcopy | |
| - name: install Python | |
| 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 | |
| lean --json -T100000 --make src | python scripts/detect_errors.py | |
| - name: push release to azure | |
| if: always() && github.repository == 'leanprover-community/mathlib' | |
| 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 | |
| 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 | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: ${{ steps.setup_precompiled.outputs.artifact_name }} | |
| path: workspace.tar | |
| lint: | |
| name: Lint mathlib | |
| runs-on: ubuntu-latest | |
| needs: build | |
| 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: ubuntu-latest | |
| needs: build | |
| 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 | |
| uses: actions/setup-python@v1 | |
| with: | |
| python-version: 3.8 | |
| - name: install Python dependencies | |
| run: python -m pip install --upgrade pip pyyaml | |
| - name: tests | |
| run: | | |
| set -o pipefail | |
| lean --json -T100000 --make docs archive roadmap test | python scripts/detect_errors.py | |
| - name: leanchecker | |
| run: | | |
| lean --recursive --export=mathlib.txt src/ | |
| leanchecker 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 |