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
| on: | |
| push: | |
| name: continuous integration | |
| jobs: | |
| # Cancels previous runs of jobs in this file | |
| cancel: | |
| name: 'Cancel Previous Runs (CI)' | |
| runs-on: ubuntu-latest | |
| # timeout-minutes: 3 | |
| steps: | |
| - uses: styfle/[email protected] | |
| with: | |
| all_but_latest: true | |
| access_token: ${{ github.token }} | |
| build: | |
| name: Build | |
| runs-on: ubuntu-latest | |
| 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`. | |
| if 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/{}"'; then | |
| : # Do nothing on success | |
| else | |
| : # Do nothing on failure, but suppress errors | |
| fi | |
| # The Hoskinson runners may not have jq installed, so do that now. | |
| - name: 'Setup jq' | |
| uses: dcarbone/[email protected] | |
| - name: install elan | |
| run: | | |
| set -o pipefail | |
| curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/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@v4 | |
| - name: If using a lean-pr-release toolchain, uninstall | |
| run: | | |
| if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then | |
| printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)" | |
| elan toolchain uninstall "$(cat lean-toolchain)" | |
| fi | |
| - name: print lean and lake versions | |
| run: | | |
| lean --version | |
| lake --version | |
| - name: build cache | |
| run: | | |
| lake build cache | |
| - name: prune ProofWidgets .lake | |
| run: | | |
| # The ProofWidgets release contains not just the `.js` (which we need in order to build) | |
| # but also `.oleans`, which may have been built with the wrong toolchain. | |
| # This removes them. | |
| # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235 | |
| rm -rf .lake/packages/proofwidgets/.lake/build/lib | |
| rm -rf .lake/packages/proofwidgets/.lake/build/ir | |
| - name: get cache | |
| id: get | |
| run: | | |
| rm -rf .lake/build/lib/Mutable/ | |
| rm -rf .lake/build/lib/Algorithm/ | |
| lake exe cache get | |
| - name: update {Mutable, Algorithm}.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 algorithm | |
| 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 {Mutable, Algorithm}.lean | |
| run: | | |
| if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ] | |
| then | |
| echo "Please run 'lake exe mk_all' to regenerate the import all files" | |
| exit 1 | |
| fi | |
| - 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 Mutable Algorithm | | |
| ## 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: verify `lake exe graph` works | |
| run: | | |
| lake exe graph | |
| rm import_graph.dot | |
| # - name: test algorithm | |
| # id: test | |
| # uses: liskin/gh-problem-matcher-wrap@v3 | |
| # with: | |
| # linters: gcc | |
| # run: | |
| # lake test | |
| - name: check for unused imports | |
| 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 algorithm | |
| 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 Algorithm |