fix the fix #5635
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 mk_build_yml.sh | |
| # Edit .github/build.in.yml instead and run | |
| # .github/workflows/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-ignore: | |
| # ignore tmp branches used by bors | |
| - 'staging.tmp*' | |
| - 'trying.tmp*' | |
| - 'staging*.tmp' | |
| # 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 Mathlib 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.event.pull_request.number || github.ref }}-${{ (github.event_name == 'push' && 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 | |
| # Limit permissions for GITHUB_TOKEN for the entire workflow | |
| permissions: | |
| contents: read | |
| pull-requests: write # Only allow PR comments/labels | |
| # All other permissions are implicitly 'none' | |
| jobs: | |
| build: | |
| if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing' | |
| name: Build | |
| runs-on: pr | |
| outputs: | |
| build-outcome: ${{ steps.build.outcome }} | |
| archive-outcome: ${{ steps.archive.outcome }} | |
| counterexamples-outcome: ${{ steps.counterexamples.outcome }} | |
| get-cache-outcome: ${{ steps.get.outcome }} | |
| lint-outcome: ${{ steps.lint.outcome }} | |
| mk_all-outcome: ${{ steps.mk_all.outcome }} | |
| noisy-outcome: ${{ steps.noisy.outcome }} | |
| # shake-outcome: ${{ steps.shake.outcome }} | |
| test-outcome: ${{ steps.test.outcome }} | |
| defaults: # On Hoskinson runners, landrun is already installed. | |
| run: # note that .pr-branch/.lake must be created in a step below before we use this | |
| shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0} | |
| steps: | |
| - name: job info | |
| env: | |
| WORKFLOW: ${{ github.workflow }} | |
| PR_NUMBER: ${{ github.event.pull_request.number }} | |
| REF: ${{ github.ref }} | |
| EVENT_NAME: ${{ github.event_name }} | |
| RUN_ID: ${{ github.run_id }} | |
| CONCURRENCY_GROUP: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}-${{ (github.event_name == 'push' && contains(fromJSON('["refs/heads/master", "refs/heads/staging"]'), github.ref) && github.run_id) || '' }} | |
| shell: bash # there is no script body, so this is safe to "run" outside landrun. | |
| run: | | |
| # We just populate the env vars for this step to make them viewable in the logs | |
| - name: cleanup | |
| shell: bash # This *just* deletes old files, so is safe to run outside landrun. | |
| run: | | |
| if ! find . -mindepth 1 -exec rm -rf -- {} +; then | |
| echo "ERROR: Initial cleanup failed, waiting 5 seconds and retrying..." | |
| sleep 5 | |
| find . -mindepth 1 -exec rm -rf -- {} + | |
| fi | |
| # 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/install-jq-action@b7ef57d46ece78760b4019dbc4080a1ba2a40b45 # v3.2.0 | |
| # Checkout the master branch into a subdirectory | |
| - name: Checkout master branch | |
| uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0 | |
| with: | |
| # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository, | |
| # we don't maintain a `master` branch at all. | |
| # For PRs and pushes to this repository, we will use `nightly-testing` instead. | |
| ref: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing' || 'master' }} | |
| path: master-branch | |
| # Checkout the PR branch into a subdirectory | |
| - name: Checkout PR branch | |
| uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0 | |
| with: | |
| ref: "${{ github.sha }}" | |
| path: pr-branch | |
| - name: Prepare DownstreamTest directory | |
| shell: bash | |
| run: | | |
| echo "Copying lean-toolchain to DownstreamTest..." | |
| cd pr-branch | |
| # Ensure DownstreamTest/.lake/ directory exists, since landrun will need it later | |
| mkdir -p DownstreamTest/.lake/ | |
| cd DownstreamTest | |
| cp ../lean-toolchain . | |
| echo "lean-toolchain copied successfully to DownstreamTest." | |
| # Create empty directories so landrun doesn't complain | |
| - name: Create empty directories | |
| shell: bash # We need to run this outside landrun, as it is a prerequisite for landrun! | |
| run: | | |
| mkdir -p pr-branch/.lake/ | |
| mkdir -p .cache/mathlib/ | |
| mkdir -p _work | |
| # NOTE: if you copy this, consider using `leanprover/lean-action` instead. | |
| # We install manually, to avoid running lean outside landrun. | |
| - name: install elan | |
| shell: bash | |
| run: | | |
| set -o pipefail | |
| curl -o elan-init.sh -sSfL https://elan.lean-lang.org/elan-init.sh | |
| chmod +x elan-init.sh | |
| ./elan-init.sh -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" | |
| - name: set toolchain directory | |
| shell: bash | |
| run: | | |
| cd pr-branch | |
| # Get the lake binary path from elan and extract toolchain directory | |
| LAKE_PATH=$(elan which lake) | |
| echo "Lake path: $LAKE_PATH" | |
| # Extract the toolchain directory by removing /bin/lake from the end | |
| TOOLCHAIN_DIR=$(dirname "$LAKE_PATH") | |
| TOOLCHAIN_DIR=$(dirname "$TOOLCHAIN_DIR") | |
| echo "Toolchain directory: $TOOLCHAIN_DIR" | |
| # Set it as an environment variable for subsequent steps | |
| echo "TOOLCHAIN_DIR=$TOOLCHAIN_DIR" >> "$GITHUB_ENV" | |
| - name: set LEAN_SRC_PATH | |
| shell: bash | |
| run: | | |
| cd pr-branch | |
| # Start with the base paths | |
| LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake" | |
| # Extract package names from lake-manifest.json and validate them | |
| # Only allow A-Z, a-z, 0-9, _, and - characters | |
| # Build the LEAN_SRC_PATH by appending each validated package | |
| PACKAGE_NAMES=$(jq -r '.packages[].name' lake-manifest.json) | |
| for pkg in $PACKAGE_NAMES; do | |
| if [[ "$pkg" =~ ^[A-Za-z0-9_-]+$ ]]; then | |
| LEAN_SRC_PATH="$LEAN_SRC_PATH:.lake/packages/$pkg" | |
| else | |
| echo "Warning: Skipping invalid package name: $pkg" | |
| fi | |
| done | |
| echo "LEAN_SRC_PATH=$LEAN_SRC_PATH" | |
| # Set it as an environment variable for subsequent steps | |
| echo "LEAN_SRC_PATH=$LEAN_SRC_PATH" >> "$GITHUB_ENV" | |
| - name: build master-branch tools | |
| shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun. | |
| run: | | |
| cd master-branch | |
| lake build cache check-yaml graph | |
| ls .lake/build/bin/cache | |
| ls .lake/build/bin/check-yaml | |
| ls .lake/packages/importGraph/.lake/build/bin/graph | |
| - name: cleanup .cache/mathlib | |
| # This needs write access to .cache/mathlib, so can't be run inside landrun. | |
| # However it is only using the `master` version of `cache`, so is safe to run outside landrun. | |
| shell: bash | |
| run: | | |
| # Define the cache directory path | |
| CACHE_DIR="$HOME/.cache/mathlib" | |
| # Check if directory exists | |
| if [ ! -d "$CACHE_DIR" ]; then | |
| echo "::warning::Cache directory does not exist: $CACHE_DIR" | |
| exit 0 | |
| fi | |
| # Calculate directory size in bytes | |
| DIR_SIZE=$(du -sb "$CACHE_DIR" | cut -f1) | |
| printf 'Cache size (in bytes): %s\n' "$DIR_SIZE" | |
| # Check if size exceeds 10GB | |
| if [ "$DIR_SIZE" -gt "10737418240" ]; then | |
| echo "Cache size exceeds threshold, running lake exe cache clean" | |
| # We use the master-branch version of `cache`. | |
| cd master-branch | |
| lake exe cache clean | |
| fi | |
| - name: download dependencies | |
| # We need network access to download dependencies | |
| # We run this inside landrun, but restrict disk access. | |
| # Landrun argument notes: | |
| # - we give --rox access to `~/.elan` and `~/actions-runner/_work` (GitHub CI needs this) | |
| # - we give --unrestricted-network as we need this to download dependencies | |
| # - git needs read only access to `/etc`. | |
| shell: landrun --unrestricted-network --rox /etc --rox /usr --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0} | |
| run: | | |
| cd pr-branch | |
| lake env | |
| - name: validate lake-manifest.json inputRevs | |
| # Only enforce this on the main mathlib4 repository, not on nightly-testing | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| shell: bash | |
| run: | | |
| cd pr-branch | |
| # Check that all inputRevs in lake-manifest.json match the required pattern | |
| echo "Validating lake-manifest.json inputRevs..." | |
| # Extract all inputRevs from the manifest | |
| invalid_revs=$(jq -r '.packages[].inputRev // empty' lake-manifest.json | \ | |
| grep -v -E '^(main|master|v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?(\+[a-zA-Z0-9.-]+)?)$' || true) | |
| if [ -n "$invalid_revs" ]; then | |
| echo "❌ Error: Found invalid inputRevs in lake-manifest.json:" | |
| echo "$invalid_revs" | |
| echo "" | |
| echo "All inputRevs must be one of:" | |
| echo " - 'main'" | |
| echo " - 'master'" | |
| echo " - 'vX.Y.Z' (semantic version, e.g., v1.2.3, v1.2.3-pre, or v1.2.3+build)" | |
| exit 1 | |
| else | |
| echo "✅ All inputRevs in lake-manifest.json are valid" | |
| fi | |
| - name: verify ProofWidgets lean-toolchain matches on versioned releases | |
| # Only enforce this on the main mathlib4 repository, not on nightly-testing | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| shell: bash | |
| run: | | |
| cd pr-branch | |
| # Read the lean-toolchain file | |
| TOOLCHAIN=$(cat lean-toolchain | tr -d '[:space:]') | |
| echo "Lean toolchain: $TOOLCHAIN" | |
| # Check if toolchain matches the versioned release pattern: leanprover/lean4:vX.Y.Z (with optional suffix like -rc1) | |
| if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?$ ]]; then | |
| echo "✓ Detected versioned Lean release: $TOOLCHAIN" | |
| echo "Verifying ProofWidgets lean-toolchain matches..." | |
| # Check if ProofWidgets lean-toolchain exists | |
| if [ ! -f .lake/packages/proofwidgets/lean-toolchain ]; then | |
| echo "❌ Error: .lake/packages/proofwidgets/lean-toolchain does not exist" | |
| echo "This file should be created by 'lake env' during dependency download." | |
| exit 1 | |
| fi | |
| # Read ProofWidgets lean-toolchain | |
| PROOFWIDGETS_TOOLCHAIN=$(cat .lake/packages/proofwidgets/lean-toolchain | tr -d '[:space:]') | |
| echo "ProofWidgets toolchain: $PROOFWIDGETS_TOOLCHAIN" | |
| # Compare the two | |
| if [ "$TOOLCHAIN" != "$PROOFWIDGETS_TOOLCHAIN" ]; then | |
| echo "❌ Error: Lean toolchain mismatch!" | |
| echo " Main lean-toolchain: $TOOLCHAIN" | |
| echo " ProofWidgets lean-toolchain: $PROOFWIDGETS_TOOLCHAIN" | |
| echo "" | |
| echo "When using a versioned Lean release (leanprover/lean4:vX.Y.Z)," | |
| echo "the ProofWidgets dependency must use the same toolchain." | |
| echo "Please update the ProofWidgets dependency to use $TOOLCHAIN" | |
| exit 1 | |
| else | |
| echo "✅ ProofWidgets lean-toolchain matches: $TOOLCHAIN" | |
| fi | |
| else | |
| echo "ℹ Lean toolchain is not a versioned release (pattern: leanprover/lean4:vX.Y.Z)" | |
| echo "Skipping ProofWidgets toolchain verification." | |
| fi | |
| - name: get cache (1/3 - setup and initial fetch) | |
| id: get_cache_part1_setup | |
| shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun | |
| run: | | |
| cd pr-branch | |
| echo "Removing old Mathlib build directories prior to cache fetch..." | |
| rm -rf .lake/build/lib/lean/Mathlib | |
| # Fail quickly if the cache is completely cold, by checking for Mathlib.Init | |
| echo "Attempting to fetch olean for Mathlib/Init.lean from cache..." | |
| ../master-branch/.lake/build/bin/cache get Mathlib/Init.lean | |
| - name: get cache (2/3 - test Mathlib.Init cache) | |
| id: get_cache_part2_test | |
| continue-on-error: true # Allow workflow to proceed to Part 3 to check outcome | |
| # This step uses the job's default shell, which is landrun-wrapped bash | |
| run: | | |
| cd pr-branch | |
| echo "Attempting: lake build --no-build -v Mathlib.Init (this runs under landrun)" | |
| lake build --no-build -v Mathlib.Init | |
| - name: get cache (3/3 - finalize cache operation) | |
| id: get | |
| shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun | |
| run: | | |
| cd pr-branch | |
| if [[ "${{ steps.get_cache_part2_test.outcome }}" == "success" ]]; then | |
| echo "Fetching all remaining cache..." | |
| ../master-branch/.lake/build/bin/cache get | |
| # Run again with --repo, to ensure we actually get the oleans. | |
| ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get | |
| else | |
| echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed." | |
| echo "No cache for 'Mathlib.Init' available or it could not be prepared." | |
| fi | |
| - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean | |
| id: mk_all | |
| continue-on-error: true # Allow workflow to continue, outcome checked later | |
| # This runs `mk_all --check` from the `pr-branch` inside landrun | |
| run: | | |
| cd pr-branch | |
| echo "Running mk_all --check (from pr-branch)..." | |
| lake exe mk_all --check | |
| - name: begin gh-problem-match-wrap for build step | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after. | |
| linters: lean | |
| - name: build mathlib | |
| id: build | |
| run: | | |
| cd pr-branch | |
| echo "::group::{test curl}" | |
| # Test curl - should fail when landrun network isolation is working | |
| if curl --silent --head --fail https://www.example.com/ >/dev/null 2>&1; then | |
| echo "ERROR: curl to example.com succeeded, but it should fail when landrun is working correctly!" | |
| exit 1 | |
| else | |
| echo "curl to example.com failed as expected - landrun network isolation is working" | |
| fi | |
| echo "::endgroup::" | |
| ../master-branch/scripts/lake-build-with-retry.sh Mathlib | |
| # results of build at pr-branch/.lake/build_summary_Mathlib.json | |
| - name: end gh-problem-match-wrap for build step | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| action: remove | |
| linters: lean | |
| - name: print the sizes of the oleans | |
| run: | | |
| cd pr-branch | |
| du .lake/build/lib/lean/Mathlib || echo "This code should be unreachable" | |
| - name: upload artifact containing contents of pr-branch | |
| # temporary measure for debugging no-build failures | |
| uses: actions/upload-artifact@330a01c490aca151604b8cf639adc76d48f6c5d4 # v5.0.0 | |
| with: | |
| name: mathlib4_artifact | |
| include-hidden-files: true | |
| # we exclude .git since there may be secrets in there | |
| path: | | |
| pr-branch/ | |
| !pr-branch/.git/ | |
| # The cache secrets are available here, so we must not run any untrusted code. | |
| - name: Upload cache to Azure | |
| # We only upload the cache if the build started (whether succeeding, failing, or cancelled) | |
| # but not if any earlier step failed or was cancelled. | |
| # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836 | |
| if: ${{ always() && steps.get.outcome == 'success' }} | |
| shell: bash | |
| run: | | |
| cd pr-branch | |
| # Trim trailing whitespace from secrets to prevent issues with accidentally added spaces | |
| export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}" | |
| # Use the trusted cache tool from master-branch | |
| # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked | |
| # ../master-branch/.lake/build/bin/cache commit || true | |
| # run this in CI if it gets an incorrect lake hash for existing cache files somehow | |
| # ../master-branch/.lake/build/bin/cache put! | |
| # do not try to upload files just downloaded | |
| echo "Uploading cache to Azure..." | |
| USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked | |
| env: | |
| MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }} | |
| # Note: we should not be including `Archive` and `Counterexamples` in the cache. | |
| # We do this for now for the sake of not rebuilding them in every CI run | |
| # even when they are not touched. | |
| # Since `Archive` and `Counterexamples` files have very simple dependencies, | |
| # it should be possible to determine whether they need to be built without actually | |
| # storing and transferring oleans over the network. | |
| # Hopefully a future re-implementation of `cache` will obviate the present need for this hack. | |
| - name: fetch archive and counterexamples cache | |
| shell: bash | |
| run: | | |
| cd pr-branch | |
| ../master-branch/.lake/build/bin/cache get Archive.lean | |
| ../master-branch/.lake/build/bin/cache get Counterexamples.lean | |
| - name: build archive | |
| id: archive | |
| continue-on-error: true | |
| run: | | |
| cd pr-branch | |
| ../master-branch/scripts/lake-build-with-retry.sh Archive | |
| # results of build at pr-branch/.lake/build_summary_Archive.json | |
| - name: build counterexamples | |
| id: counterexamples | |
| continue-on-error: true | |
| run: | | |
| cd pr-branch | |
| ../master-branch/scripts/lake-build-with-retry.sh Counterexamples | |
| # results of build at pr-branch/.lake/build_summary_Counterexamples.json | |
| - name: Check if building Archive or Counterexamples failed | |
| if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure' | |
| run: | | |
| if [ "${{ steps.archive.outcome }}" == "failure" ]; then | |
| echo "❌ The \"build archive\" step above failed; please check its logs." | |
| fi | |
| if [ "${{ steps.counterexamples.outcome }}" == "failure" ]; then | |
| echo "❌ The \"build counterexamples\" step above failed; please check its logs." | |
| fi | |
| exit 1 | |
| # The cache secrets are available here, so we must not run any untrusted code. | |
| - name: Upload Archive and Counterexamples cache to Azure | |
| shell: bash | |
| run: | | |
| cd pr-branch | |
| # Trim trailing whitespace from secrets to prevent issues with accidentally added spaces | |
| export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}" | |
| echo "Uploading Archive and Counterexamples cache to Azure..." | |
| USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean | |
| USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean | |
| env: | |
| MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }} | |
| - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean | |
| if: ${{ always() && steps.mk_all.outcome != 'skipped' }} | |
| run: | | |
| if [[ "${{ steps.mk_all.outcome }}" != "success" ]]; then | |
| echo "Please run 'lake exe mk_all' to regenerate the import all files" | |
| exit 1 | |
| else | |
| echo "'mk_all --check' passed successfully." | |
| fi | |
| - name: begin gh-problem-match-wrap for test step | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after. | |
| linters: lean | |
| - name: test mathlib | |
| id: test | |
| run: | | |
| cd pr-branch | |
| ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_MathlibTest.json lake --iofail test | |
| - name: end gh-problem-match-wrap for test step | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| action: remove | |
| linters: lean | |
| - name: begin gh-problem-match-wrap for shake and lint steps | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after. | |
| linters: gcc | |
| # With the arrival of the module system, the old `shake` is no longer functional. | |
| # This will be replaced soon. | |
| # - name: check for unused imports | |
| # id: shake | |
| # run: | | |
| # cd pr-branch | |
| # env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style | |
| - name: lint mathlib | |
| if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }} | |
| id: lint | |
| run: | | |
| cd pr-branch | |
| env LEAN_ABORT_ON_PANIC=1 ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_lint.json lake exe runLinter Mathlib | |
| - name: end gh-problem-match-wrap for shake and lint steps | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| action: remove | |
| linters: gcc | |
| - name: check for noisy stdout lines | |
| id: noisy | |
| run: | | |
| cd pr-branch | |
| 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 Mathlib Archive Counterexamples | | |
| ## 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( \\([0-9]+ jobs\\))?\\.?$"){ print $0 }')" | |
| if [ -n "${buildMsgs}" ] | |
| then | |
| printf $'%s\n' "${buildMsgs}" | |
| exit 1 | |
| fi | |
| - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches | |
| if: always() | |
| shell: bash | |
| env: | |
| TOKEN: ${{ secrets.LEAN_PR_TESTING }} | |
| GITHUB_CONTEXT: ${{ toJson(github) }} | |
| WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }} | |
| BUILD_OUTCOME: ${{ steps.build.outcome }} | |
| NOISY_OUTCOME: ${{ steps.noisy.outcome }} | |
| ARCHIVE_OUTCOME: ${{ steps.archive.outcome }} | |
| COUNTEREXAMPLES_OUTCOME: ${{ steps.counterexamples.outcome }} | |
| LINT_OUTCOME: ${{ steps.lint.outcome }} | |
| TEST_OUTCOME: ${{ steps.test.outcome }} | |
| NIGHTLY_TESTING_REPO: leanprover-community/mathlib4-nightly-testing | |
| run: | | |
| master-branch/scripts/lean-pr-testing-comments.sh lean | |
| master-branch/scripts/lean-pr-testing-comments.sh batteries | |
| post_steps: | |
| name: Post-Build Step | |
| if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing' | |
| needs: [build] | |
| runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed. | |
| steps: | |
| - uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0 | |
| with: | |
| ref: "${{ github.sha }}" | |
| - name: Configure Lean | |
| uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0 | |
| with: | |
| auto-config: false # Don't run `lake build`, `lake test`, or `lake lint` automatically. | |
| use-github-cache: false | |
| use-mathlib-cache: false # This can be re-enabled once we are confident in the cache again. | |
| reinstall-transient-toolchain: true | |
| - name: get cache for Mathlib | |
| run: | | |
| # Run once without --repo, so we can diagnose what `lake exe cache get` wants to do by itself. | |
| lake exe cache get | |
| # Run again with --repo, so ensure we actually get the oleans. | |
| lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get | |
| - name: get cache for Archive and Counterexamples | |
| run: | | |
| # Run once without --repo, so we can diagnose what `lake exe cache get` wants to do by itself. | |
| lake exe cache get Archive Counterexamples | |
| # Run again with --repo, so ensure we actually get the oleans. | |
| lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get Archive Counterexamples | |
| - name: verify that everything was available in the cache | |
| run: | | |
| echo "::group::{verify Mathlib cache}" | |
| lake build --no-build --rehash -v Mathlib | |
| echo "::endgroup::" | |
| echo "::group::{verify Archive cache}" | |
| lake build --no-build --rehash -v Archive | |
| echo "::endgroup::" | |
| echo "::group::{verify Counterexamples cache}" | |
| lake build --no-build --rehash -v Counterexamples | |
| echo "::endgroup::" | |
| - name: check declarations in db files | |
| run: | | |
| python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml | |
| lake exe check-yaml | |
| - name: generate our import graph | |
| run: | | |
| lake exe graph | |
| - name: upload the import graph | |
| uses: actions/upload-artifact@330a01c490aca151604b8cf639adc76d48f6c5d4 # v5.0.0 | |
| with: | |
| name: import-graph | |
| path: import_graph.dot | |
| ## the default is 90, but we build often, so unless there's a reason | |
| ## to care about old copies in the future, just say 7 days for now | |
| retention-days: 7 | |
| - name: clean up the import graph file | |
| run: rm import_graph.dot | |
| - name: build everything | |
| # make sure everything is available for test/import_all.lean | |
| # and that miscellaneous executables still work | |
| run: | | |
| lake build Batteries Qq Aesop ProofWidgets Plausible pole unused | |
| - name: build AesopTest (nightly-testing only) | |
| # Only run on the mathlib4-nightly-testing repository | |
| if: github.repository == 'leanprover-community/mathlib4-nightly-testing' | |
| run: | | |
| lake build AesopTest | |
| # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit. | |
| # Instead we run it in a cron job on master: see `lean4checker.yml`. | |
| # Output is posted to the zulip topic | |
| # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker | |
| - name: checkout lean4checker | |
| if: ${{ (always() && needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }} | |
| shell: bash | |
| run: | | |
| git clone https://github.com/leanprover/lean4checker | |
| cd lean4checker | |
| # Read lean-toolchain file and checkout appropriate branch | |
| TOOLCHAIN=$(cat ../lean-toolchain) | |
| if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then | |
| VERSION=${TOOLCHAIN#leanprover/lean4:} | |
| git checkout "$VERSION" | |
| else | |
| git checkout master | |
| fi | |
| - name: run leanchecker on itself | |
| if: ${{ (always() && needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }} | |
| run: | | |
| cd lean4checker | |
| # Build lean4checker using the same toolchain | |
| cp ../lean-toolchain . | |
| lake build | |
| lake -q exe lean4checker Lean4Checker | |
| style_lint: | |
| name: Lint style | |
| if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18 | |
| with: | |
| mode: check | |
| lint-bib-file: true | |
| ref: ${{ github.sha }} | |
| final: | |
| name: Post-CI job | |
| if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing' | |
| needs: [style_lint, build, post_steps] | |
| runs-on: ubuntu-latest | |
| steps: | |
| - id: PR_from_push | |
| uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.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 | |
| # TODO: delete this step and rename `PR_from_push` to `PR` if the above step seems to work properly | |
| # Combine the output from the previous action with the metadata supplied by GitHub itself. | |
| # Note that if we fall back to github.event.pull_request data, the list of labels is generated when this workflow is triggered | |
| # and not updated afterwards! | |
| - id: PR | |
| shell: bash | |
| run: | | |
| echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" | tee -a "$GITHUB_OUTPUT" | |
| echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" | tee -a "$GITHUB_OUTPUT" | |
| - 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 }}' | |
| - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') | |
| name: Get PR label timeline data | |
| # 'auto-merge-after-CI' must be within the last 100 labels added (could be increased to 250 if needed) | |
| # query from https://stackoverflow.com/a/67939355 | |
| # unfortunately we cannot query only for 'auto-merge-after-CI' events | |
| # so we have to process this with jq in the next step | |
| id: get-timeline | |
| uses: octokit/graphql-action@abaeca7ba4f0325d63b8de7ef943c2418d161b93 # v3.0.0 | |
| with: | |
| query: | | |
| query($owner: String!, $name: String!, $number: Int!) { | |
| repository(owner: $owner, name: $name) { | |
| pullRequest(number: $number) { | |
| timelineItems(itemTypes: LABELED_EVENT, last: 100) { | |
| nodes { | |
| ... on LabeledEvent { | |
| createdAt | |
| actor { login } | |
| label { name } | |
| } | |
| } | |
| } | |
| } | |
| } | |
| } | |
| owner: leanprover-community | |
| name: mathlib4 | |
| number: ${{ steps.PR.outputs.number }} | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') | |
| name: Extract label actor username | |
| id: get-label-actor | |
| run: | | |
| # Parse the GraphQL response and filter for the specific label | |
| echo '${{ steps.get-timeline.outputs.data }}' | |
| USERNAME=$(echo '${{ steps.get-timeline.outputs.data }}' | jq -r ' | |
| .repository.pullRequest.timelineItems.nodes | |
| | map(select(.label.name == "auto-merge-after-CI")) | |
| | sort_by(.createdAt) | |
| | last | |
| | .actor.login // empty | |
| ') | |
| # Validate username format (GitHub usernames are alphanumeric + hyphens, max 39 chars) | |
| printf 'USERNAME: %s\n' "$USERNAME" | |
| if [[ -z "$USERNAME" ]]; then | |
| echo "Error: No actor found for the specified label" | |
| exit 1 | |
| elif ! [[ "$USERNAME" =~ ^[a-zA-Z0-9-]{1,39}$ ]]; then | |
| echo "Error: Invalid username format: $USERNAME" | |
| exit 1 | |
| fi | |
| echo "username=$USERNAME" >> "$GITHUB_OUTPUT" | |
| echo "Found label actor: $USERNAME" | |
| - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') | |
| name: check team membership | |
| uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3.0.0 | |
| id: actorTeams | |
| with: | |
| organization: leanprover-community # optional. Default value ${{ github.repository_owner }} | |
| # Organization to get membership from. | |
| username: ${{ steps.get-label-actor.outputs.username }} | |
| GITHUB_TOKEN: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # (Requires scope: `read:org`) | |
| - if: ${{ contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') && (contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') || contains(steps.actorTeams.outputs.teams, 'bot-users')) }} | |
| name: If `auto-merge-after-CI` is present, add a `bors merge` comment. | |
| uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1 | |
| with: | |
| token: ${{ secrets.AUTO_MERGE_TOKEN }} | |
| issue-number: ${{ steps.PR.outputs.number }} | |
| body: | | |
| As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors: | |
| bors merge |