feat: add instances about Nat.Primes (#6238)
#3934
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: | |
| - staging | |
| name: continuous integration (staging) | |
| 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: bors | |
| steps: | |
| - name: cleanup | |
| run: | | |
| find . -name . -o -prune -exec rm -rf -- {} + | |
| - uses: actions/checkout@v3 | |
| - name: Install bibtool | |
| if: ${{ 'bors' == 'ubuntu-latest' }} | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y bibtool | |
| - name: install Python | |
| if: ${{ 'bors' == 'ubuntu-latest' }} | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: 3.8 | |
| - name: lint | |
| run: | | |
| ./scripts/lint-style.sh | |
| - 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 | |
| build: | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| name: Build | |
| runs-on: bors | |
| steps: | |
| - name: cleanup | |
| run: | | |
| find . -name . -o -prune -exec rm -rf -- {} + | |
| - name: install elan | |
| run: | | |
| set -o pipefail | |
| curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/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: get cache | |
| run: | | |
| lake exe cache clean | |
| lake exe cache get | |
| - name: build mathlib | |
| 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 "stdout:" stdout.log | |
| - name: build library_search cache | |
| run: lake build -KCI MathlibExtras | |
| - name: upload cache | |
| if: always() | |
| run: | | |
| lake exe cache commit || true | |
| lake exe cache put || true | |
| env: | |
| MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} | |
| - name: build archive | |
| run: lake build Archive | |
| - name: build counterexamples | |
| run: lake build Counterexamples | |
| - name: check declarations in db files | |
| run: | | |
| python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml | |
| build/bin/checkYaml | |
| - name: test mathlib | |
| run: make -j 8 test | |
| - name: lint mathlib | |
| uses: liskin/gh-problem-matcher-wrap@v2 | |
| with: | |
| linters: gcc | |
| run: env LEAN_ABORT_ON_PANIC=1 make lint | |
| 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 }}' |