Repository navigation
Enable queue validation and independent project metadata #6475
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
| name: Lean Action CI | |
| # The build runs in one of three modes, decided per run by a cheap `plan` job | |
| # (scripts/ci/plan-build-shards.py) from the diff and the cache state: | |
| # | |
| # - `skip`: an exact README-only change. It still reports the | |
| # protected `Build project` check without spending hours rebuilding Lean. | |
| # - `single`: the classic one-job pipeline. This is the fast path for the | |
| # common case — a PR that adds or edits a project or three. | |
| # - `rebase`: reuse an earlier green PR build after the automatic merge of | |
| # independent pool content, then build the combined root and check metadata. | |
| # - `sharded`: for the runs that take hours serially (cold cache, | |
| # toolchain/manifest bump, refactors touching many projects), the dirty | |
| # projects are bin-packed into parallel `shard` build jobs. Pool projects | |
| # never import each other, so project-granular shards duplicate no work. | |
| # Each shard uploads only the files its build produced; `finalize` merges | |
| # them, builds the root library (also a safety net: anything a shard | |
| # missed is built here), and runs the whole-pool linters and quality | |
| # checks once. | |
| # | |
| # Shard assignment is computed from the tree at run time — there is no | |
| # static shard list to maintain as the pool grows. The `Build project` | |
| # gate job reports the overall verdict under the same check name the | |
| # single-job workflow used. | |
| on: | |
| merge_group: | |
| types: [checks_requested] | |
| push: | |
| branches: | |
| - main | |
| paths: | |
| - '**/*.lean' | |
| - 'lakefile.toml' | |
| - 'lean-toolchain' | |
| - 'lake-manifest.json' | |
| - 'LeanPool/projects/**' | |
| - 'LeanPool/projects.yml' | |
| - 'python/lean_pool/quality.py' | |
| - 'python/lean_pool/registry.py' | |
| - 'python/lean_pool/indexes.py' | |
| - 'python/lean_pool/queue_build.py' | |
| - 'python/lean_pool/validation_cache.py' | |
| - 'python/lean_pool/ci_artifacts.py' | |
| - 'python/lean_pool/ci_cache.py' | |
| - 'python/lean_pool/ci_pr_build.py' | |
| - 'python/lean_pool/ci_validation_artifacts.py' | |
| - 'python/lean_pool/rebase_fastpath.py' | |
| - 'python/pyproject.toml' | |
| - 'python/uv.lock' | |
| - 'scripts/nolints-style.txt' | |
| - 'scripts/ci/**' | |
| - '.github/CODE_QUALITY.md' | |
| - '.github/workflows/lean_action_ci.yml' | |
| pull_request: | |
| branches: | |
| - main | |
| # Work stacks on the bump branch during a Lean/Mathlib migration, and | |
| # a contribution that never builds is a contribution nobody can judge: | |
| # PR #301 added a 210-file project onto `bump/v4.33.0-rc1` and got no | |
| # build, no linters, and no quality checks at all. | |
| - 'bump/**' | |
| workflow_dispatch: | |
| inputs: | |
| force_full: | |
| description: "Shard-build the whole pool even when a warm cache exists" | |
| required: false | |
| type: boolean | |
| default: false | |
| # Let main finish and seed caches; cancel superseded PR runs. | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} | |
| permissions: | |
| contents: read | |
| pages: write | |
| id-token: write | |
| actions: read | |
| jobs: | |
| plan: | |
| runs-on: ubuntu-latest | |
| name: Plan build | |
| outputs: | |
| build_revision: ${{ steps.build-identity.outputs.revision }} | |
| base_build_revision: ${{ steps.build-identity.outputs.base_revision }} | |
| minimal_build: ${{ steps.plan.outputs.minimal_build }} | |
| mode: ${{ steps.plan.outputs.mode }} | |
| matrix: ${{ steps.plan.outputs.matrix }} | |
| reuse_run_id: ${{ steps.plan.outputs.reuse_run_id }} | |
| previous_head: ${{ steps.plan.outputs.previous_head }} | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| - name: Install Python tooling runtime | |
| uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff | |
| with: | |
| enable-cache: true | |
| - name: Identify compiled Lean sources | |
| id: build-identity | |
| env: | |
| BASE_REF: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.sha }} | |
| run: | | |
| set -euo pipefail | |
| revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision) | |
| echo "revision=$revision" >> "$GITHUB_OUTPUT" | |
| base_revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision --ref "$BASE_REF") | |
| echo "base_revision=$base_revision" >> "$GITHUB_OUTPUT" | |
| # A cold build cache is when whole-pool sharding pays off most. | |
| - name: Check for a warm build cache | |
| id: lake-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| lookup-only: true | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ steps.build-identity.outputs.revision }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Plan the build | |
| id: plan | |
| env: | |
| EVENT_NAME: ${{ github.event_name }} | |
| BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} | |
| BEFORE_SHA: ${{ github.event.before }} | |
| FORCE_FULL: ${{ inputs.force_full }} | |
| CACHE_MATCHED: ${{ steps.lake-cache.outputs.cache-matched-key }} | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| PR_NUMBER: ${{ github.event.pull_request.number }} | |
| PR_HEAD: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }} | |
| run: | | |
| set -euo pipefail | |
| diff_available=true | |
| # A file, not an environment variable: a large import's path list | |
| # exceeds the kernel's 128 KiB limit on a single environment string. | |
| changed_files="$RUNNER_TEMP/changed-files.txt" | |
| : > "$changed_files" | |
| case "$EVENT_NAME" in | |
| merge_group) | |
| git diff --name-only "$BASE_SHA"..HEAD > "$changed_files" | |
| ;; | |
| pull_request) | |
| git diff --name-only "$BASE_SHA"...HEAD > "$changed_files" | |
| ;; | |
| push) | |
| if [ -n "$BEFORE_SHA" ] \ | |
| && ! printf '%s' "$BEFORE_SHA" | grep -q '^0*$' \ | |
| && git cat-file -e "$BEFORE_SHA" 2>/dev/null; then | |
| git diff --name-only "$BEFORE_SHA"..HEAD > "$changed_files" | |
| else | |
| diff_available=false | |
| fi | |
| ;; | |
| workflow_dispatch) | |
| diff_available=false | |
| ;; | |
| esac | |
| minimal_build=false | |
| if [ "$EVENT_NAME" = pull_request ] && grep -Eq '^(python/lean_pool/(exposition/|ci_artifacts.py$)|scripts/exposition/|.github/workflows/exposition-verify.yml$)' "$changed_files"; then | |
| minimal_build=true | |
| fi | |
| echo "minimal_build=$minimal_build" >> "$GITHUB_OUTPUT" | |
| cold=false | |
| if [ -z "$CACHE_MATCHED" ]; then cold=true; fi | |
| plan=$(CHANGED_FILES_PATH="$changed_files" DIFF_AVAILABLE="$diff_available" \ | |
| COLD="$cold" FORCE_FULL="$FORCE_FULL" \ | |
| python3 scripts/ci/plan-build-shards.py) | |
| reuse_run_id="" | |
| previous_head="" | |
| if [ "$EVENT_NAME" = "pull_request" ] && [ "$FORCE_FULL" != "true" ] && [ "$minimal_build" != true ]; then | |
| reuse=$(PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath decide \ | |
| --repository "$REPOSITORY" --number "$PR_NUMBER" \ | |
| --head "$PR_HEAD" --base "$BASE_SHA") | |
| if [ "$(echo "$reuse" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["eligible"]).lower())')" = true ]; then | |
| reuse_run_id=$(echo "$reuse" | python3 -c 'import json,sys; print(json.load(sys.stdin)["run_id"])') | |
| previous_head=$(echo "$reuse" | python3 -c 'import json,sys; print(json.load(sys.stdin)["previous_head"])') | |
| plan='{"mode":"rebase","matrix":{"include":[{"shard":"00","projects":""}]}}' | |
| else | |
| echo "Rebase reuse unavailable: $(echo "$reuse" | python3 -c 'import json,sys; print(json.load(sys.stdin)["reason"])')" | |
| fi | |
| fi | |
| echo "Plan: $plan" | |
| { | |
| echo "mode=$(echo "$plan" | python3 -c 'import json,sys; print(json.load(sys.stdin)["mode"])')" | |
| echo "matrix=$(echo "$plan" | python3 -c 'import json,sys; print(json.dumps(json.load(sys.stdin)["matrix"]))')" | |
| echo "reuse_run_id=$reuse_run_id" | |
| echo "previous_head=$previous_head" | |
| } >> "$GITHUB_OUTPUT" | |
| # The single-job pipeline is the fast path for ordinary PRs. | |
| build: | |
| needs: plan | |
| if: needs.plan.outputs.mode == 'single' | |
| runs-on: ubuntu-latest | |
| name: Build pool | |
| permissions: | |
| contents: read | |
| actions: write | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| # Keep the large toolchain/Mathlib cache independent of per-commit builds. | |
| - name: Restore Lean dependencies | |
| id: dependency-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Restore pool build | |
| id: cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Install Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Install uv | |
| uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff | |
| with: | |
| enable-cache: true | |
| - name: Check compiled artifact dependency tracking with pinned Lean | |
| env: | |
| LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1' | |
| run: >- | |
| uv run --project python --group test pytest -q | |
| python/tests/test_ci_pr_build.py python/tests/test_indexes.py | |
| -k 'test_lake_' | |
| - name: Install Mathlib cache | |
| id: mathlib-cache | |
| run: | | |
| if [ ! -d ".lake/packages/mathlib" ]; then | |
| ~/.elan/bin/lake exe cache get | |
| else | |
| echo "Mathlib already present from cache" | |
| fi | |
| - name: Check library indexes use the module system and are up to date | |
| run: | | |
| if ! ~/.elan/bin/lake exe mk_all --module --check; then | |
| echo "::error::Library indexes are out of date or missing module headers. Run 'lake exe mk_all --module' locally and commit the result." | |
| exit 1 | |
| fi | |
| - name: Reuse compiled projects from merged PRs | |
| if: github.event_name == 'push' && steps.cache.outputs.cache-hit != 'true' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| BEFORE_SHA: ${{ github.event.before }} | |
| run: | | |
| if PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build \ | |
| --repository "$REPOSITORY" --base "$BEFORE_SHA" --head "$GITHUB_SHA" --merged; then | |
| echo 'Restored the successfully merged queue build.' | |
| elif git cat-file -e "$BEFORE_SHA" 2>/dev/null; then | |
| PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath restore-main \ | |
| --repository "$REPOSITORY" --head "$BEFORE_SHA" --base "$GITHUB_SHA" | |
| fi | |
| - name: Reuse compiled files from this PR's successful runs | |
| if: github.event_name == 'pull_request' && steps.cache.outputs.cache-hit != 'true' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| PR_NUMBER: ${{ github.event.pull_request.number }} | |
| PR_BRANCH: ${{ github.head_ref }} | |
| PR_HEAD: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }} | |
| PR_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} | |
| CURRENT_RUN: ${{ github.run_id }} | |
| run: >- | |
| PYTHONPATH=python uv run --project python --locked python -m lean_pool.ci_pr_build | |
| --number "$PR_NUMBER" --branch "$PR_BRANCH" | |
| --head "$PR_HEAD" --base "$PR_BASE" --current-run "$CURRENT_RUN" | |
| - name: Reuse successful queued PR builds | |
| if: github.event_name == 'merge_group' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| BASE_SHA: ${{ github.event.merge_group.base_sha }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha }} | |
| run: >- | |
| PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build | |
| --base "$BASE_SHA" --head "$HEAD_SHA" | |
| - name: Build project | |
| id: compilation | |
| run: | | |
| set -euo pipefail | |
| ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log | |
| if grep -nE '(^|: )warning:' lean-build.log; then | |
| echo "::error::Lean build emitted warnings; fix them before merging." | |
| exit 1 | |
| fi | |
| # Publish once compilation succeeds, so docs can overlap the later | |
| # linters/quality checks. Rare PRs requiring the minimal-file gate share | |
| # this exact-tree output too, avoiding a second cold whole-pool build. | |
| - name: Package build for documentation | |
| if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') | |
| run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack | |
| - name: Share build with documentation | |
| if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: lean-pool-build | |
| path: lean-pool-build.tar.zst | |
| if-no-files-found: error | |
| compression-level: 0 | |
| retention-days: 1 | |
| # Actions scopes PR caches to refs/pull/<n>/merge: updates to the same | |
| # PR can reuse receipts, while main and other PRs cannot read them. | |
| - name: Restore project validation | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/validation-cache/v1 | |
| key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| restore-keys: | | |
| LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Recover saved validation when caches were evicted | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| BUILD_EVENT: ${{ github.event_name }} | |
| BUILD_HEAD: ${{ github.sha }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.ci_validation_artifacts | |
| --event "$BUILD_EVENT" --head "$BUILD_HEAD" | |
| - name: Install validation dependencies | |
| run: cd python && uv sync --locked | |
| - name: Reuse successful queued PR validation | |
| if: github.event_name == 'merge_group' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| BASE_SHA: ${{ github.event.merge_group.base_sha }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha }} | |
| run: >- | |
| PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build | |
| --base "$BASE_SHA" --head "$HEAD_SHA" --receipts | |
| - name: Lint | |
| run: | | |
| cd python | |
| uv run python -m lean_pool.validation_cache lint --repo .. | |
| cd .. | |
| - name: Text style lint | |
| run: | | |
| ~/.elan/bin/lake exe lint-style LeanPool | |
| - name: Repository quality checks | |
| run: | | |
| cd python | |
| uv run python -m lean_pool.validation_cache quality --repo .. | |
| - name: Retain successful validation independently of build caches | |
| continue-on-error: true | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: lean-validation-receipts | |
| path: .lake/validation-cache/v1/passes.json | |
| include-hidden-files: true | |
| if-no-files-found: error | |
| compression-level: 1 | |
| retention-days: 14 | |
| - name: Package PR project build for later rebases | |
| if: github.event_name == 'pull_request' || github.event_name == 'merge_group' | |
| continue-on-error: true | |
| env: | |
| BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }} | |
| run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA" | |
| - name: Retain PR project build | |
| if: github.event_name == 'pull_request' || github.event_name == 'merge_group' | |
| continue-on-error: true | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: rebase-project-build | |
| path: rebase-project-build.tar.gz | |
| if-no-files-found: error | |
| compression-level: 0 | |
| retention-days: 14 | |
| - name: Save project validation | |
| # Successful receipts are tiny; retain PR results across registry rebases. | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/validation-cache/v1 | |
| key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| - name: Prune old copies of project validation | |
| if: success() && github.ref == 'refs/heads/main' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| CACHE_KEY: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.ci_cache prune | |
| --repository "$REPOSITORY" --key "$CACHE_KEY" | |
| - name: Save Lean dependencies | |
| if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Prune old copies of lean dependencies | |
| if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| CACHE_KEY: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.ci_cache prune | |
| --repository "$REPOSITORY" --key "$CACHE_KEY" | |
| - name: Save pool build | |
| if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} | |
| - name: Prune old copies of pool build | |
| if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| CACHE_KEY: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.ci_cache prune | |
| --repository "$REPOSITORY" --key "$CACHE_KEY" | |
| shard: | |
| needs: plan | |
| if: needs.plan.outputs.mode == 'sharded' | |
| runs-on: ubuntu-latest | |
| name: Build shard ${{ matrix.shard }} | |
| strategy: | |
| # One shard failing must not cancel the rest: `finalize` rebuilds any | |
| # gap itself, so the run still yields a complete log — but the gate | |
| # job fails whenever a shard failed (a shard's warning gate must not | |
| # be bypassable by cache replay in `finalize`). | |
| fail-fast: false | |
| matrix: ${{ fromJSON(needs.plan.outputs.matrix) }} | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| - name: Restore Lean dependencies | |
| id: dependency-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Restore pool build | |
| id: cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Install Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Install Mathlib cache | |
| id: mathlib-cache | |
| run: | | |
| if [ ! -d ".lake/packages/mathlib" ]; then | |
| ~/.elan/bin/lake exe cache get | |
| else | |
| echo "Mathlib already present from cache" | |
| fi | |
| - name: Build this shard's projects | |
| env: | |
| PROJECTS: ${{ matrix.projects }} | |
| run: | | |
| set -euo pipefail | |
| touch "$RUNNER_TEMP/build-stamp" | |
| modules="" | |
| # shellcheck disable=SC2086 # word-split the project list on purpose | |
| for project in $PROJECTS; do | |
| project_modules=$(git ls-files -- "LeanPool/$project.lean" "LeanPool/$project/" \ | |
| | grep '\.lean$' \ | |
| | sed -e 's/\.lean$//' -e 's#/#.#g' \ | |
| | tr '\n' ' ') | |
| modules="$modules $project_modules" | |
| done | |
| # shellcheck disable=SC2086 # modules is a space-separated list on purpose | |
| ~/.elan/bin/lake build $modules 2>&1 | tee shard-build.log | |
| if grep -nE '(^|: )warning:' shard-build.log; then | |
| echo "::error::Lean build emitted warnings; fix them before merging." | |
| exit 1 | |
| fi | |
| # Ship only what this build produced; unchanged (cache-replayed) | |
| # files stay out, so `finalize` can layer the shard outputs onto the | |
| # same restored cache without clobbering anything fresher. | |
| - name: Package new build outputs | |
| env: | |
| SHARD: ${{ matrix.shard }} | |
| run: | | |
| set -euo pipefail | |
| find .lake/build -type f -newer "$RUNNER_TEMP/build-stamp" \ | |
| > "$RUNNER_TEMP/new-files.txt" | |
| echo "$(wc -l < "$RUNNER_TEMP/new-files.txt") new build files" | |
| if [ -s "$RUNNER_TEMP/new-files.txt" ]; then | |
| tar -czf "shard-oleans-$SHARD.tar.gz" -T "$RUNNER_TEMP/new-files.txt" | |
| fi | |
| - name: Upload build outputs | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: ci-oleans-${{ matrix.shard }} | |
| path: shard-oleans-*.tar.gz | |
| if-no-files-found: ignore | |
| retention-days: 1 | |
| finalize: | |
| needs: [plan, shard] | |
| # Run even when a shard failed: merging what succeeded and building the | |
| # rest here still produces a complete build log and lint report for | |
| # debugging. The gate job is what enforces that every shard was green. | |
| if: >- | |
| !cancelled() && needs.plan.result == 'success' && | |
| needs.plan.outputs.mode == 'sharded' | |
| runs-on: ubuntu-latest | |
| name: Assemble and lint | |
| permissions: | |
| contents: read | |
| actions: write | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| - name: Restore Lean dependencies | |
| id: dependency-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Restore pool build | |
| id: cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Install Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Install uv | |
| uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff | |
| with: | |
| enable-cache: true | |
| - name: Check compiled artifact dependency tracking with pinned Lean | |
| env: | |
| LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1' | |
| run: >- | |
| uv run --project python --group test pytest -q | |
| python/tests/test_ci_pr_build.py python/tests/test_indexes.py | |
| -k 'test_lake_' | |
| - name: Install Mathlib cache | |
| id: mathlib-cache | |
| run: | | |
| if [ ! -d ".lake/packages/mathlib" ]; then | |
| ~/.elan/bin/lake exe cache get | |
| else | |
| echo "Mathlib already present from cache" | |
| fi | |
| - name: Download shard build outputs | |
| uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 | |
| with: | |
| pattern: ci-oleans-* | |
| merge-multiple: true | |
| - name: Merge shard build outputs | |
| run: | | |
| set -euo pipefail | |
| for archive in shard-oleans-*.tar.gz; do | |
| if [ -e "$archive" ]; then | |
| tar -xzf "$archive" | |
| rm "$archive" | |
| fi | |
| done | |
| - name: Check library indexes use the module system and are up to date | |
| run: | | |
| if ! ~/.elan/bin/lake exe mk_all --module --check; then | |
| echo "::error::Library indexes are out of date or missing module headers. Run 'lake exe mk_all --module' locally and commit the result." | |
| exit 1 | |
| fi | |
| # With the shard outputs in place this is mostly cache replay; it | |
| # builds the root module and anything a shard missed or failed to | |
| # deliver, so the assembled pool is complete regardless. | |
| - name: Reuse successful queued PR builds | |
| if: github.event_name == 'merge_group' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| BASE_SHA: ${{ github.event.merge_group.base_sha }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha }} | |
| run: >- | |
| PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build | |
| --base "$BASE_SHA" --head "$HEAD_SHA" | |
| - name: Build project | |
| id: compilation | |
| run: | | |
| set -euo pipefail | |
| ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log | |
| if grep -nE '(^|: )warning:' lean-build.log; then | |
| echo "::error::Lean build emitted warnings; fix them before merging." | |
| exit 1 | |
| fi | |
| # Publish once compilation succeeds, so docs can overlap the later | |
| # linters/quality checks. Rare PRs requiring the minimal-file gate share | |
| # this exact-tree output too, avoiding a second cold whole-pool build. | |
| - name: Package build for documentation | |
| if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') | |
| run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack | |
| - name: Share build with documentation | |
| if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true') | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: lean-pool-build | |
| path: lean-pool-build.tar.zst | |
| if-no-files-found: error | |
| compression-level: 0 | |
| retention-days: 1 | |
| # Actions scopes PR caches to refs/pull/<n>/merge: updates to the same | |
| # PR can reuse receipts, while main and other PRs cannot read them. | |
| - name: Restore project validation | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/validation-cache/v1 | |
| key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| restore-keys: | | |
| LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Recover saved validation when caches were evicted | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| BUILD_EVENT: ${{ github.event_name }} | |
| BUILD_HEAD: ${{ github.sha }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.ci_validation_artifacts | |
| --event "$BUILD_EVENT" --head "$BUILD_HEAD" | |
| - name: Install validation dependencies | |
| run: cd python && uv sync --locked | |
| - name: Reuse successful queued PR validation | |
| if: github.event_name == 'merge_group' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| BASE_SHA: ${{ github.event.merge_group.base_sha }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha }} | |
| run: >- | |
| PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build | |
| --base "$BASE_SHA" --head "$HEAD_SHA" --receipts | |
| - name: Lint | |
| run: | | |
| cd python | |
| uv run python -m lean_pool.validation_cache lint --repo .. | |
| cd .. | |
| - name: Text style lint | |
| run: | | |
| ~/.elan/bin/lake exe lint-style LeanPool | |
| - name: Repository quality checks | |
| run: | | |
| cd python | |
| uv run python -m lean_pool.validation_cache quality --repo .. | |
| - name: Retain successful validation independently of build caches | |
| continue-on-error: true | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: lean-validation-receipts | |
| path: .lake/validation-cache/v1/passes.json | |
| include-hidden-files: true | |
| if-no-files-found: error | |
| compression-level: 1 | |
| retention-days: 14 | |
| - name: Package PR project build for later rebases | |
| if: github.event_name == 'pull_request' || github.event_name == 'merge_group' | |
| continue-on-error: true | |
| env: | |
| BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }} | |
| run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA" | |
| - name: Retain PR project build | |
| if: github.event_name == 'pull_request' || github.event_name == 'merge_group' | |
| continue-on-error: true | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: rebase-project-build | |
| path: rebase-project-build.tar.gz | |
| if-no-files-found: error | |
| compression-level: 0 | |
| retention-days: 14 | |
| - name: Save project validation | |
| # Successful receipts are tiny; retain PR results across registry rebases. | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/validation-cache/v1 | |
| key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| - name: Prune old copies of project validation | |
| if: success() && github.ref == 'refs/heads/main' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| CACHE_KEY: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.ci_cache prune | |
| --repository "$REPOSITORY" --key "$CACHE_KEY" | |
| - name: Save Lean dependencies | |
| if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Prune old copies of lean dependencies | |
| if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| CACHE_KEY: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.ci_cache prune | |
| --repository "$REPOSITORY" --key "$CACHE_KEY" | |
| - name: Save pool build | |
| if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} | |
| # Reuse the prior green project's compiled modules and current main's cache. | |
| # A missing artifact falls back to the full validation sequence in this job. | |
| - name: Prune old copies of pool build | |
| if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| CACHE_KEY: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.ci_cache prune | |
| --repository "$REPOSITORY" --key "$CACHE_KEY" | |
| rebase: | |
| needs: plan | |
| if: needs.plan.outputs.mode == 'rebase' | |
| runs-on: ubuntu-latest | |
| name: Check rebased root | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| - name: Restore Lean dependencies | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Restore current main build | |
| id: main-build | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.base_build_revision }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Install uv | |
| uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff | |
| with: | |
| enable-cache: true | |
| - name: Reuse newly merged projects while the main cache warms | |
| if: steps.main-build.outputs.cache-hit != 'true' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| PREVIOUS_HEAD: ${{ needs.plan.outputs.previous_head }} | |
| BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} | |
| run: >- | |
| PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath restore-main | |
| --repository "$REPOSITORY" --head "$PREVIOUS_HEAD" --base "$BASE_SHA" | |
| - name: Restore previously validated PR modules | |
| id: project-build | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| RUN_ID: ${{ needs.plan.outputs.reuse_run_id }} | |
| PREVIOUS_HEAD: ${{ needs.plan.outputs.previous_head }} | |
| REPOSITORY: ${{ github.repository }} | |
| run: >- | |
| PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath restore | |
| --repository "$REPOSITORY" --run-id "$RUN_ID" --head "$PREVIOUS_HEAD" | |
| - name: Install Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Check compiled artifact dependency tracking with pinned Lean | |
| env: | |
| LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1' | |
| run: >- | |
| uv run --project python --group test pytest -q | |
| python/tests/test_ci_pr_build.py python/tests/test_indexes.py | |
| -k 'test_lake_' | |
| - name: Install Mathlib cache | |
| run: | | |
| if [ ! -d ".lake/packages/mathlib" ]; then | |
| ~/.elan/bin/lake exe cache get | |
| fi | |
| - name: Check generated index | |
| run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath check-index | |
| - name: Build combined Lean root | |
| run: | | |
| set -euo pipefail | |
| ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log | |
| if grep -nE '(^|: )warning:' lean-build.log; then | |
| echo "::error::Lean build emitted warnings; fix them before merging." | |
| exit 1 | |
| fi | |
| - name: Install validation dependencies | |
| run: cd python && uv sync --locked | |
| - name: Validate combined repository metadata | |
| if: steps.project-build.outcome == 'success' | |
| run: cd python && uv run python -m lean_pool.quality --repo .. --static-only | |
| - name: Restore validation cache for the combined checkout | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/validation-cache/v1 | |
| key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| restore-keys: | | |
| LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Carry saved checks through the verified rebase | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| PREVIOUS_RUN: ${{ needs.plan.outputs.reuse_run_id }} | |
| BUILD_HEAD: ${{ github.sha }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.ci_validation_artifacts | |
| --event pull_request --head "$BUILD_HEAD" --previous-run "$PREVIOUS_RUN" | |
| - name: Full validation when the prior artifact is unavailable | |
| if: steps.project-build.outcome != 'success' | |
| run: | | |
| set -euo pipefail | |
| (cd python && uv run python -m lean_pool.validation_cache lint --repo ..) | |
| ~/.elan/bin/lake exe lint-style LeanPool | |
| (cd python && uv run python -m lean_pool.validation_cache quality --repo ..) | |
| - name: Retain successful validation independently of build caches | |
| continue-on-error: true | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: lean-validation-receipts | |
| path: .lake/validation-cache/v1/passes.json | |
| include-hidden-files: true | |
| if-no-files-found: warn | |
| compression-level: 1 | |
| retention-days: 14 | |
| - name: Package PR project build for later rebases | |
| continue-on-error: true | |
| env: | |
| BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }} | |
| run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA" | |
| - name: Retain PR project build | |
| continue-on-error: true | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: rebase-project-build | |
| path: rebase-project-build.tar.gz | |
| if-no-files-found: error | |
| compression-level: 0 | |
| retention-days: 14 | |
| # Single overall verdict under the check name the one-job workflow used, | |
| # so nothing watching "Build project" needs to change. | |
| gate: | |
| needs: [plan, build, shard, finalize, rebase] | |
| if: always() | |
| runs-on: ubuntu-latest | |
| name: Build project | |
| steps: | |
| - name: Check outcome | |
| env: | |
| MODE: ${{ needs.plan.outputs.mode }} | |
| PLAN_RESULT: ${{ needs.plan.result }} | |
| BUILD_RESULT: ${{ needs.build.result }} | |
| SHARD_RESULT: ${{ needs.shard.result }} | |
| FINALIZE_RESULT: ${{ needs.finalize.result }} | |
| REBASE_RESULT: ${{ needs.rebase.result }} | |
| run: | | |
| set -euo pipefail | |
| echo "plan=$PLAN_RESULT mode=$MODE build=$BUILD_RESULT shard=$SHARD_RESULT finalize=$FINALIZE_RESULT" | |
| if [ "$PLAN_RESULT" != "success" ]; then | |
| echo "::error::Build planning failed." | |
| exit 1 | |
| fi | |
| case "$MODE" in | |
| skip) | |
| echo "No Lean build inputs changed." | |
| ;; | |
| rebase) | |
| [ "$REBASE_RESULT" = "success" ] || { echo "::error::Rebase validation failed."; exit 1; } | |
| ;; | |
| single) | |
| [ "$BUILD_RESULT" = "success" ] || { echo "::error::Build failed."; exit 1; } | |
| ;; | |
| sharded) | |
| [ "$SHARD_RESULT" = "success" ] || { echo "::error::A build shard failed."; exit 1; } | |
| [ "$FINALIZE_RESULT" = "success" ] || { echo "::error::Assembly or linting failed."; exit 1; } | |
| ;; | |
| *) | |
| echo "::error::Unknown build mode: $MODE" | |
| exit 1 | |
| ;; | |
| esac | |
| echo "CI passed in $MODE mode." |