From 5565b0911e2bc9862be292d63f0e5a670a7ec555 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Fri, 11 Sep 2026 19:38:19 +0000 Subject: [PATCH 1/2] ci: isolate parallel proof validation from Pages deployment --- .github/workflows/lean_action_ci.yml | 129 +++++++++++++++++++++++++-- AGENTS.md | 12 ++- README.md | 29 +++++- 3 files changed, 153 insertions(+), 17 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 38c71ed05..0c21cc22e 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -8,19 +8,23 @@ on: pull_request: workflow_dispatch: -# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages permissions: - contents: read # Read access to repository contents - pages: write # Write access to GitHub Pages - id-token: write # Write access to ID tokens - -concurrency: - group: pages - cancel-in-progress: false + contents: read jobs: build: + name: build runs-on: ubuntu-latest + timeout-minutes: 90 + concurrency: + # PRs are keyed by number so a new revision supersedes the old merge + # ref. Pushes are keyed by ref. For main, cancel-in-progress=false + # deliberately retains the active run and lets the newest pending + # checkpoint replace older pending work. This bounds the queue while + # making that default-branch policy explicit, without making validation + # wait for documentation or publishing. + group: ${{ github.workflow }}-validation-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} steps: - uses: actions/checkout@v5 @@ -46,4 +50,111 @@ jobs: sudo apt-get clean || true df -h / - uses: leanprover/lean-action@v1 - - uses: leanprover-community/docgen-action@v1 + with: + # Keep the required check an explicit ordinary `lake build`, even + # if future Lake metadata changes lean-action auto-detection. + build: true + build-args: "" + + docs: + name: docs + needs: build + # Documentation is built only for the trusted default branch. This job + # has no Pages credentials; PRs (including fork PRs) never enter it. + if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/main' && needs.build.result == 'success' }} + runs-on: ubuntu-latest + timeout-minutes: 90 + permissions: + contents: read + concurrency: + # Only main reaches this job, but cancel a superseded in-progress docs + # build to avoid an unbounded documentation runner backlog. + group: ${{ github.workflow }}-docs-${{ github.ref }} + cancel-in-progress: true + + steps: + - name: Checkout validated revision + uses: actions/checkout@v5 + with: + ref: ${{ github.sha }} + persist-credentials: false + + - name: Install Lean for documentation generation + uses: leanprover/lean-action@v1 + with: + # docgen-action expects elan/lake from an earlier lean-action step; + # do not run another project build in this documentation job. + auto-config: false + build: false + test: false + lint: false + + - name: Build documentation without publishing + # v1 predates the deploy=false input and would publish from this job; + # use the current upstream revision whose action.yml documents dry-run + # generation, pinned for reproducibility. + uses: leanprover-community/docgen-action@56023ee2a4b3630c1071825be5bafdb43f540bbd # main, 2026-09-11 + with: + # docgen-action documents deploy=false as its dry-run mode. It still + # builds the API docs; upload/deploy remain explicit below. + deploy: false + build-page: false + + - name: Save documentation for the matching revision + uses: actions/upload-artifact@v4 + with: + name: pages-${{ github.sha }} + path: docs + retention-days: 1 + if-no-files-found: error + + publish: + name: publish + needs: [build, docs] + # Only code pushed to the trusted default branch may receive Pages + # credentials, and only after the proof and docs jobs succeed. + if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/main' && needs.build.result == 'success' && needs.docs.result == 'success' }} + runs-on: ubuntu-latest + timeout-minutes: 30 + permissions: + contents: read + pages: write + id-token: write + # Serialize only the publishing stage. Do not cancel an in-flight + # deployment: the SHA check below makes an older queued run fail instead + # of publishing after a newer main revision. + concurrency: + group: pages-production + cancel-in-progress: false + + steps: + - name: Checkout validated revision + uses: actions/checkout@v5 + with: + ref: ${{ github.sha }} + persist-credentials: false + + - name: Restore documentation for the matching revision + uses: actions/download-artifact@v4 + with: + name: pages-${{ github.sha }} + path: docs + + - name: Confirm this is still the current main revision + env: + GH_TOKEN: ${{ github.token }} + EXPECTED_SHA: ${{ github.sha }} + run: | + actual_sha="$(gh api "repos/${GITHUB_REPOSITORY}/git/ref/heads/main" --jq '.object.sha')" + if [[ "$actual_sha" != "$EXPECTED_SHA" ]]; then + echo "Refusing to publish stale revision $EXPECTED_SHA; current main is $actual_sha." >&2 + exit 1 + fi + + - name: Upload documentation artifact + uses: actions/upload-pages-artifact@v3 + with: + path: docs + + - name: Deploy documentation + uses: actions/deploy-pages@v4 diff --git a/AGENTS.md b/AGENTS.md index d6bc14ac1..8bdad1de0 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -108,7 +108,7 @@ theorem-shape suggestions, or proof repairs: - Test isolated snippets and candidate proof steps within the assistant's scratch environment first. - All suggested results are advisory; every proof modification must be fully - validated locally using Lake. + validated using Lake, locally or in the README's CI-first draft-PR workflow. ## Proof Status and Assumption Boundaries @@ -133,6 +133,10 @@ theorem-shape suggestions, or proof repairs: - Before changing files touched by open PRs, inspect the PR diffs to avoid conflicting with the intended API direction. -- Run focused Lake builds for touched Lean modules to verify changes quickly. -- Run a full Lake build and check for warnings before pushing or committing - Lean changes. +- Prefer focused Lake builds for touched Lean modules when a local build owner + is available; never contend for a shared build cache. +- Follow README's CI-first draft-PR policy: source-checked feature-branch + commits may precede remote compilation, but must be labeled unverified until + the exact revision passes the full default build and applicable axiom audits. +- Keep parallel workers on disjoint files and isolated branches. One integrator + reviews and merges verified work; a draft checkpoint is not proof completion. diff --git a/README.md b/README.md index 85d4515fa..8f8790996 100644 --- a/README.md +++ b/README.md @@ -517,7 +517,8 @@ The guard rejects `sorry`, `admit`, and source `axiom` commands, and reports low-use theorem-shaped propositions that still need an explicit status in `PROOF_STATUS.md`. -All committed code must build without warnings. +All code accepted into the default branch must build without warnings. Draft +branches may use the CI-first verification workflow below. To maintain clean and reliable build verification, the use of `set_option` is forbidden in the codebase. All warnings, lint errors, or resource limits should @@ -539,9 +540,29 @@ Please keep repository configuration files (like `lakefile.toml` and ### CI and PR Policy -To keep the repository stable for all developers, please never merge a pull -request or push any change that would cause the CI build to fail. If a change -introduces a CI failure, it must be investigated and fixed immediately. +Small, independently owned changes may use a **CI-first draft PR**: run the +applicable source checks, commit to a feature branch, and push a draft PR for +GitHub-hosted compilation. A local full build is not a prerequisite for that +draft checkpoint. State clearly which checks have and have not run; a draft +commit is not a verified theorem milestone. + +Parallel workers must use isolated branches/worktrees and disjoint file +ownership. Keep builds against a shared local Lake cache serialized; isolated +GitHub-hosted runners can validate PRs independently. One integrator reviews +the theorem statements, assumptions, source changes, and verification results. + +Before merging, require successful proof validation of the exact candidate +revision: all source guards, the ordinary default build (including Production +and tactic regressions), and applicable transitive-axiom checks. The separate +Comparator audit covers only its explicitly listed theorem surface. After a +rebase or integration change, rerun the relevant checks; never treat cancelled, +skipped, stale, or missing checks as success. Fix failed draft checks before +marking the work ready. Do not push unverified changes directly to the default +branch or enable automatic merging merely to bypass review. + +Documentation publication is separate from proof validation and restricted to +validated default-branch revisions. A documentation failure does not establish +a proof failure, and a successful website deployment is not proof verification. ### Repository Cleanliness From 3447bc875baf70f7232bafd912eb2a0c3fdd318f Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Fri, 11 Sep 2026 19:40:00 +0000 Subject: [PATCH 2/2] ci: avoid duplicate branch-push and PR builds --- .github/workflows/lean_action_ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 0c21cc22e..526cb8f12 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -5,6 +5,7 @@ env: on: push: + branches: [main] pull_request: workflow_dispatch: