Lint to mathlib standards #56
This file contains hidden or 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 scripts/mk_build_yml.sh | |
| # Edit scripts/build_template.yml instead and run | |
| # scripts/mk_build_yml.sh to update. | |
| # Forks of add-combi 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 | |
| env: | |
| # Disable Lake's automatic fetching of cloud builds. | |
| # Lake's cache is currently incompatible with Mathlib's `lake exe cache`. | |
| # This is because Mathlib's Cache assumes all build artifacts present in the build directory | |
| # are valid by-products of the AddCombi build. Build artifacts fetched from Lake's cache do | |
| # not necessarily satisfy this property. | |
| LAKE_NO_CACHE: true | |
| concurrency: | |
| # label each workflow run; only the latest with each label will run | |
| # workflows on master get more expressive labels | |
| group: ${{ github.workflow }}-${{ github.ref }}. | |
| ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}} | |
| # cancel any running workflow with the same label | |
| cancel-in-progress: true | |
| # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages | |
| permissions: | |
| contents: read | |
| pages: write | |
| id-token: write | |
| jobs: | |
| style_lint: | |
| if: github.repository == 'YaelDillies/add-combi' | |
| name: Lint style | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Check out add-combi | |
| uses: actions/checkout@v4 | |
| # 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.2.0 | |
| - name: Check for Lean files with the executable bit set | |
| shell: bash | |
| run: | | |
| executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))" | |
| if [[ -n "$executable_files" ]] | |
| then | |
| echo "ERROR: The following Lean files have the executable bit set." | |
| echo "$executable_files" | |
| exit 1 | |
| fi | |
| - name: Files in AddCombi.Mathlib can't import AddCombi files outside AddCombi.Mathlib | |
| run: | | |
| ! (find AddCombi/Mathlib -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import AddCombi.(?!Mathlib)') | |
| - name: Install elan | |
| run: | | |
| set -o pipefail | |
| curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz | |
| ./elan-init -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" | |
| - name: Install bibtool | |
| if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }} | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y bibtool | |
| - name: Lint references | |
| run: scripts/lint_bib.sh | |
| build: | |
| if: github.repository == 'YaelDillies/add-combi' | |
| name: Build | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Check out add-combi | |
| uses: actions/checkout@v4 | |
| - name: Install elan | |
| run: | | |
| set -o pipefail | |
| curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz | |
| ./elan-init -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" | |
| - name: Build cache | |
| run: lake build cache | |
| - name: Get cache | |
| id: get | |
| run: lake exe cache get || true | |
| - name: Update AddCombi.lean | |
| id: mk_all | |
| run: | | |
| if ! lake exe mk_all --check | |
| then | |
| echo "Not all lean files are in the import all files" | |
| echo "mk_all=false" >> "${GITHUB_OUTPUT}" | |
| else | |
| echo "mk_all=true" >> "${GITHUB_OUTPUT}" | |
| fi | |
| - name: Build add-combi | |
| id: build | |
| uses: liskin/gh-problem-matcher-wrap@v3 | |
| with: | |
| linters: gcc | |
| run: | | |
| bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI" | |
| - name: Check for noisy stdout lines | |
| id: noisy | |
| run: | | |
| buildMsgs="$( | |
| ## we exploit `lake`s replay feature: since the cache is present, running | |
| ## `lake build` will reproduce all the outputs without having to recompute | |
| lake build | | |
| ## we filter out the output lines that begin with `✔ [xx/yy]`, where xx, yy | |
| ## are either numbers or ?, and the "Build completed successfully." message. | |
| ## We keep the rest, which are actual outputs of the files | |
| awk '!($0 ~ "^\\s*✔ \\[[?0-9]*/[?0-9]*\\]" || $0 == "Build completed successfully."){ print $0 }')" | |
| if [ -n "${buildMsgs}" ] | |
| then | |
| printf $'%s\n' "${buildMsgs}" | |
| exit 1 | |
| fi | |
| - name: Shake | |
| id: shake | |
| uses: liskin/gh-problem-matcher-wrap@v3 | |
| with: | |
| linters: gcc | |
| run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style | |
| - name: Lint | |
| if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }} | |
| id: lint | |
| uses: liskin/gh-problem-matcher-wrap@v3 | |
| with: | |
| linters: gcc | |
| run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter AddCombi | |
| - if: github.repository == 'YaelDillies/add-combi' | |
| name: Cache dependencies docs | |
| uses: actions/cache@v3 | |
| with: | |
| path: docbuild/.lake/build/doc | |
| key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} | |
| restore-keys: MathlibDoc- | |
| - if: github.repository == 'YaelDillies/add-combi' | |
| name: Build documentation | |
| run: scripts/build_docs.sh | |
| - if: github.repository == 'YaelDillies/add-combi' | |
| name: Move documentation to the website | |
| run: | | |
| mkdir -p website/docs | |
| mv docs/build website/docs | |
| - if: github.repository == 'YaelDillies/add-combi' | |
| name: Use the README as website index | |
| run: cp README.md website/index.md | |
| - if: github.repository == 'YaelDillies/add-combi' | |
| name: Build import graph | |
| run: | | |
| sudo apt-get update | |
| sudo apt install graphviz -y | |
| ~/.elan/bin/lake exe graph website/import_graph.pdf | |
| - if: github.repository == 'YaelDillies/add-combi' | |
| name: Bundle website dependencies | |
| uses: ruby/setup-ruby@v1 | |
| with: | |
| working-directory: website | |
| ruby-version: "3.0" # Not needed with a .ruby-version file | |
| bundler-cache: true # runs 'bundle install' and caches installed gems automatically | |
| - if: github.repository == 'YaelDillies/add-combi' | |
| name: Bundle website | |
| working-directory: website | |
| run: JEKYLL_ENV=production bundle exec jekyll build | |
| - if: github.repository == 'YaelDillies/add-combi' | |
| name: Upload docs & blueprint artifact to website | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: website/_site | |
| - if: github.repository == 'YaelDillies/add-combi' | |
| name: Deploy website to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v4 |