ci: Push to cache in a separate job to isolate secrets #1
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
| # Reusable workflow invoked by build.yml, bors.yml, and build_fork.yml. | ||
|
Check failure on line 1 in .github/workflows/build_template.yml
|
||
| on: | ||
| workflow_call: | ||
| inputs: | ||
| concurrency_group: | ||
| type: string | ||
| required: true | ||
| pr_branch_ref: | ||
| type: string | ||
| required: true | ||
| runs_on: | ||
| type: string | ||
| required: true | ||
| 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 | ||
| jobs: | ||
| build: | ||
| name: Build | ||
| runs-on: ${{ inputs.runs_on }} | ||
| outputs: | ||
| build-outcome: ${{ steps.build.outcome }} | ||
| archive-outcome: ${{ steps.archive.outcome }} | ||
| counterexamples-outcome: ${{ steps.counterexamples.outcome }} | ||
| cache-staging-has-files: ${{ steps.cache_staging_check.outputs.has_files }} | ||
| 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: ${{ inputs.concurrency_group }} | ||
| 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@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | ||
| 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-green` instead, | ||
| # so that even when `nightly-testing` is broken, we can still build tools from a known good state. | ||
| ref: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing-green' || 'master' }} | ||
| path: master-branch | ||
| # Checkout the PR branch into a subdirectory | ||
| - name: Checkout PR branch | ||
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | ||
| with: | ||
| ref: ${{ inputs.pr_branch_ref }} | ||
| 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" | ||
| # 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: prepare cache staging directory | ||
| if: ${{ steps.build.outcome == 'success' }} | ||
| shell: bash | ||
| run: | | ||
| rm -rf cache-staging | ||
| mkdir -p cache-staging | ||
| - name: stage Mathlib cache files | ||
| if: ${{ steps.build.outcome == 'success' }} | ||
| shell: bash | ||
| run: | | ||
| cd pr-branch | ||
| lake env ../master-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage-unpacked | ||
| - name: stage Archive cache files | ||
| if: ${{ steps.archive.outcome == 'success' }} | ||
| shell: bash | ||
| run: | | ||
| cd pr-branch | ||
| lake env ../master-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage-unpacked Archive.lean | ||
| - name: stage Counterexamples cache files | ||
| if: ${{ steps.counterexamples.outcome == 'success' }} | ||
| shell: bash | ||
| run: | | ||
| cd pr-branch | ||
| lake env ../master-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage-unpacked Counterexamples.lean | ||
| - name: check cache staging contents | ||
| id: cache_staging_check | ||
| if: ${{ steps.build.outcome == 'success' }} | ||
| shell: bash | ||
| run: | | ||
| if find cache-staging -type f -name '*.ltar' -print -quit | grep -q .; | ||
| echo "has_files=true" >> "$GITHUB_OUTPUT" | ||
| else | ||
| echo "has_files=false" >> "$GITHUB_OUTPUT" | ||
| fi | ||
| - name: upload cache staging artifact | ||
| if: ${{ steps.cache_staging_check.outputs.has_files == 'true' }} | ||
| uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0 | ||
| with: | ||
| name: cache-staging | ||
| path: cache-staging/ | ||
| - 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 | ||
| - 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 | ||
| timeout-minutes: 40 | ||
| run: | | ||
| cd pr-branch | ||
| set -o pipefail | ||
| # Try running with --trace; if it fails due to argument parsing, the PR needs to merge master | ||
| # We use .lake/ for the output file because landrun restricts /tmp access | ||
| for attempt in 1 2; do | ||
| if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then | ||
| break | ||
| fi | ||
| status=${PIPESTATUS[0]} | ||
| if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then | ||
| echo "" | ||
| echo "==============================================================================" | ||
| echo "ERROR: Your branch uses an older version of runLinter that doesn't support" | ||
| echo "the --trace flag. Please merge 'master' into your PR branch to get the" | ||
| echo "updated linter, then push again." | ||
| echo "" | ||
| echo "You can do this with:" | ||
| echo " git fetch upstream" | ||
| echo " git merge upstream/master" | ||
| echo " git push" | ||
| echo "==============================================================================" | ||
| echo "" | ||
| exit 1 | ||
| fi | ||
| if [ "$status" -eq 124 ]; then | ||
| echo "runLinter timed out (attempt $attempt)." | ||
| if [ "$attempt" -lt 2 ]; then | ||
| echo "Retrying runLinter after timeout..." | ||
| continue | ||
| fi | ||
| fi | ||
| exit $status | ||
| done | ||
| # We need to separate this step from the previous script because it needs to run outside of landrun | ||
| - name: kill stray runLinter processes | ||
| if: ${{ steps.lint.outcome == 'failure' }} | ||
| continue-on-error: true | ||
| shell: bash | ||
| run: | | ||
| echo "Checking for runLinter processes..." | ||
| if pgrep -af runLinter; then | ||
| echo "Killing runLinter processes..." | ||
| pkill -f runLinter || true | ||
| else | ||
| echo "No stray runLinter processes found." | ||
| fi | ||
| - 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 | ||
| # Generate a fresh token just before posting comments. | ||
| # GitHub App tokens expire after 1 hour, and the build can take longer than that. | ||
| - name: Generate lean-pr-testing app token | ||
| if: always() | ||
| id: lean-pr-testing-token | ||
| uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1 | ||
| with: | ||
| app-id: ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }} | ||
| private-key: ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }} | ||
| owner: leanprover | ||
| repositories: lean4 | ||
| # The create-github-app-token README states that this token is masked and will not be logged accidentally. | ||
| - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches | ||
| if: always() | ||
| shell: bash | ||
| env: | ||
| TOKEN: ${{ steps.lean-pr-testing-token.outputs.token }} | ||
| 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 | ||
| upload_cache: | ||
| name: Upload to cache | ||
| needs: [build] | ||
| runs-on: ubuntu-latest # These steps run on a GitHub runner; no landrun sandboxing is needed. | ||
| # 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() && needs.build.outputs.build-outcome == 'success' && needs.build.outputs.get-cache-outcome == 'success' && needs.build.outputs.cache-staging-has-files == 'true' }} | ||
| steps: | ||
| - name: Checkout master branch | ||
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | ||
| with: | ||
| ref: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing' || 'master' }} | ||
| fetch-depth: 1 | ||
| - name: Configure Lean | ||
| uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.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: build cache executable | ||
| run: | | ||
| lake build cache | ||
| CACHE_BIN="$(pwd)/.lake/build/bin/cache" | ||
| if [ ! -x "$CACHE_BIN" ]; then | ||
| echo "cache binary not found: $CACHE_BIN" | ||
| exit 1 | ||
| fi | ||
| echo "CACHE_BIN=$CACHE_BIN" >> "$GITHUB_ENV" | ||
| - name: Download cache staging artifact | ||
| uses: actions/download-artifact@@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0 | ||
| with: | ||
| name: cache-staging | ||
| path: cache-staging | ||
| - name: Upload staged cache to Azure | ||
| shell: bash | ||
| run: | | ||
| # 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 cache to Azure..." | ||
| MATHLIB_CACHE_USE_CLOUDFLARE=0 lake env "$CACHE_BIN" put-staged --staging-dir="cache-staging" --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} | ||
| env: | ||
| MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }} | ||
| post_steps: | ||
| name: Post-Build Step | ||
| needs: [build, upload_cache] | ||
| runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed. | ||
| steps: | ||
| - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | ||
| with: | ||
| ref: ${{ inputs.pr_branch_ref }} | ||
| - name: Configure Lean | ||
| uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.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@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.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 | ||
| - 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 `daily.yml`. | ||
| style_lint: | ||
| name: Lint style | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18 | ||
| with: | ||
| mode: check | ||
| lint-bib-file: true | ||
| ref: ${{ inputs.pr_branch_ref }} | ||
| final: | ||
| name: Post-CI job | ||
| needs: [style_lint, build, post_steps] | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Generate auto merge app token | ||
| id: auto-merge-app-token | ||
| uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1 | ||
| with: | ||
| app-id: ${{ secrets.MATHLIB_AUTO_MERGE_APP_ID }} | ||
| private-key: ${{ secrets.MATHLIB_AUTO_MERGE_PRIVATE_KEY }} | ||
| - 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@ddde8ebb2493e79f390e6449c725c21663a67505 # v3.0.2 | ||
| 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: >- # bot usernames will cause this step to error with "Could not resolve to a User..." | ||
| contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') && | ||
| steps.get-label-actor.outputs.username != 'mathlib-nolints' && | ||
| steps.get-label-actor.outputs.username != 'mathlib-update-dependencies' | ||
| 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') && | ||
| ( | ||
| steps.get-label-actor.outputs.username == 'mathlib-nolints' || | ||
| steps.get-label-actor.outputs.username == 'mathlib-update-dependencies' || | ||
| 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: | ||
| # The create-github-app-token README states that this token is masked and will not be logged accidentally. | ||
| token: ${{ steps.auto-merge-app-token.outputs.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 | ||
