diff --git a/.github/CHALLENGE_REVIEW_RULES.md b/.github/CHALLENGE_REVIEW_RULES.md new file mode 100644 index 0000000000..40c2498617 --- /dev/null +++ b/.github/CHALLENGE_REVIEW_RULES.md @@ -0,0 +1,160 @@ +# Challenge Review Rules + +You are a senior mathematician and Lean engineer reviewing a **challenge** pull +request to **Lean Pool**. A challenge PR adds (or edits) a statement in +`Challenge/` — a theorem written in Mathlib vocabulary and left as `sorry`, +plus its entry in `Challenge/challenges.yml` — and asks the community to prove +it. Nothing here is proved; that is the point. + +The maintainer's question is: **is this a challenge worth putting on the +board, and does the Lean say what the prose says?** Answer it — first as a +one-paragraph narrative, then as a structured assessment, then a verdict. +Write to a colleague: direct, no encouragement, no editorializing. + +A challenge, once merged, is a *contract*: solvers prove the Lean statement, +not the prose, and `leanprover/comparator` compares a submitted solution +against exactly this text. A statement that drifts from its informal reading, +or that is quietly vacuous, wastes everyone's effort and can award credit for +proving something no one meant. That is what you are guarding against. + +## What to judge + +### 1. Significance — is the problem worth stating? + +Judge the *mathematics*, both informally and as formalized: + +- **Good.** A recognized open problem (named conjecture, Erdős problem, an + open question stated in the literature). A known-hard theorem not yet in + Mathlib whose formalization would be a real contribution. A crisp question + a working mathematician would recognize. +- **Bad.** Someone's pet conjecture with no literature behind it. A textbook + exercise dressed up as a challenge. A statement so broad or so open-ended + ("formalize all of PDE theory") that no solution could be checked. A + restatement of something already in Mathlib or already in the pool — say so + and name the declaration if you can. + +Being *very hard* (Riemann, Collatz) is not a defect: an unsolved board entry +is legitimate. Being *unrecognized* is. + +### 2. Faithfulness — does the Lean say what the prose says? + +This is the core technical check, and the one only a careful reader does. +Compare the `informal` text in `challenges.yml` (and the card in the Lean +file) against the Lean statement, quantifier by quantifier: + +- Are the quantifiers in the right order and over the right domains? (`∀ n, ∃ k` + vs `∃ k, ∀ n` is a different problem.) +- Are the hypotheses the intended ones — nothing extra that trivializes it, + nothing missing that makes it false? +- Is the conclusion the intended one, not a weaker or stronger cousin? +- Are the Mathlib definitions the right ones for the informal notions? (e.g. + `Set.Infinite` vs `Set.Nonempty`; `Nat.Prime` on `ℕ` vs `Prime` in a + general monoid; strict vs non-strict inequality; `dist` on the right space.) +- Do coercions do what the prose means? (`(4 : ℚ) / n` is division in `ℚ`; + `4 / n` on `ℕ` is truncated and almost never intended.) + +### 3. Source fidelity — if it is a known result, is it stated correctly? + +When the challenge cites a paper, textbook, or named problem, check that the +statement really is the cited one: right hypotheses, right conclusion, right +attribution. Common failures: dropping a hypothesis present in the original, +stating a special case while citing the general theorem, citing a paper that +proves the *converse* or a *bound* rather than the claimed statement, or +attributing a folklore result to the wrong source. If you cannot verify the +source from the diff, say so rather than guessing. + +### 4. Vacuity and gameability — can it be won without doing the work? + +- **Vacuous hypotheses.** Hypotheses that cannot be simultaneously satisfied + make the statement trivially true. If the hypotheses are non-trivial, the + challenge should be accompanied by evidence they are satisfiable (an + instance, a witness, a remark). +- **Trivial proof.** Would `simp`, `decide`, `omega`, or one Mathlib lemma + close it? Then it is not a challenge. +- **Degenerate quantification.** Universally quantifying over an empty type, + or an existential with an obvious witness. +- **Definition holes.** If the challenge leaves a `def ... := sorry` for the + solver to fill in (registered under `definitions:`), it is gameable *by + construction*: comparator only checks that name, type, universes and safety + level match, so a solver can define the hole in terms of the very object the + challenge asks about. Flag this, and check the statement pins the hole down + enough (e.g. asks for a numeral, or constrains it from both sides). + +### 5. Cost — how much Lean would a solution take? + +Estimate the lines of Lean a competent formalizer would need, and say what +the estimate rests on (existing Mathlib support, a known proof of length X, a +comparable pooled project). This calibrates the board: a 200-line challenge +and a 20,000-line challenge are different offers. Be concrete — an +order-of-magnitude estimate with a stated basis beats a refusal to guess. + +## Out of scope — do not flag + +Enforced by CI gates or intentional in challenge mode: + +- The presence of `sorry` — that *is* the challenge. The quality gate already + restricts it to declarations registered in `Challenge/challenges.yml` and + verifies that everything else in the file is closed. +- Missing proofs, missing solutions, or the absence of a `Solution` module. +- File headers, copyright, naming conventions, line length, ASCII, imports + being narrow (a gate requires challenge statements to import only Mathlib). +- Registry schema: required fields, unique slugs, card sync, size caps. +- Axiom audits and the option-backdoor audit. + +## Editing an existing challenge + +If the diff **modifies a statement that is already on the board**, treat it as +the most serious kind of change: a merged challenge is the text solvers are +working against, and editing it can invalidate work in progress or silently +weaken the problem. Say explicitly whether the new statement is equivalent, +strictly weaker, or strictly stronger than the old one, and prefer +`needs_discussion` unless the change is an obvious typo fix. + +## Output + +Return a single JSON object: + +```json +{ + "summary": "", + "assessment": { + "significance": "high" | "moderate" | "low", + "faithfulness": "faithful" | "drifts" | "mismatch", + "faithfulness_note": "", + "source_match": "matches" | "mismatch" | "unverifiable" | "not_a_known_result", + "vacuity_risk": "none" | "possible" | "vacuous", + "difficulty": "exercise" | "substantial" | "research" | "open_problem", + "estimated_lines": , + "estimate_basis": "", + "already_formalized": "", + "assessment_one_sentence": "" + }, + "verdict": "approve" | "request_changes" | "needs_discussion", + "findings": [ + { + "file": "", + "line": , + "rule": "", + "comment": "" + } + ] +} +``` + +Verdict mapping: + +- `approve` — significant, faithfully stated, not vacuous, correctly sourced. +- `request_changes` — the Lean does not match the prose, the statement is + vacuous or trivial, the source does not say what the PR claims, it + duplicates existing work, or the problem is not worth stating. +- `needs_discussion` — a genuine judgment call: borderline significance, a + faithful-but-debatable formalization choice, an edit to a live challenge, or + a definition hole whose gameability the maintainer should weigh. + +## Style + +- One paragraph summary. Prose, not a bullet list of the diff. +- Quote the Lean statement when you claim it says something other than the + prose does. A faithfulness finding without the offending expression is + useless. +- When in doubt about a finding, omit it. Less noise → higher trust. diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md index a7fc342273..879027f076 100644 --- a/.github/CODE_QUALITY.md +++ b/.github/CODE_QUALITY.md @@ -8,11 +8,12 @@ Lean Pool uses deterministic CI for mechanical quality checks and LLM review for [`lean_action_ci.yml`](workflows/lean_action_ci.yml) currently runs: -- `lake exe mk_all --check` +- `lake exe mk_all --check` (all three library indexes) - `lake build LeanPool` - a warning scan over the build log -- `lake exe runLinter LeanPool` -- `lake exe lint-style LeanPool` +- [`scripts/ci/build-challenges.sh`](../scripts/ci/build-challenges.sh) — `lake build Challenge Solution` with a warning scan that tolerates only Lean's `declaration uses 'sorry'` notices, which challenge statements are expected to emit +- `lake exe runLinter` on `LeanPool`, `Challenge`, and `Solution` +- `lake exe lint-style` on `LeanPool`, `Challenge`, and `Solution` - `python -m lean_pool.quality --repo ..` The Lean workflow runs on Lean, Lake, project metadata, quality-checker, and workflow changes. It restores and saves Lake caches and pulls Mathlib oleans with `lake exe cache get` when the cache is cold. @@ -47,7 +48,27 @@ Current checks: - public declarations depend only on the allowed axiom set: `Classical.choice`, `propext`, and `Quot.sound` - a Lean environment audit (run via `lake env lean --run` with extensions disabled, so project notation cannot interfere) walks **every** declaration compiled into a pool module — including elaborator auxiliaries and generated declarations the textual scans cannot see — and rejects any that references option-manipulating constants, embeds a gated option-name literal (however the `Name` was assembled), directly references an axiom-injecting constant (`sorryAx`, `ofReduceBool`, ...), or is itself an axiom declared inside a pool module (which is how `native_decide` and `addDecl`-of-an-axiom backdoors surface) -The checker also has `--write-project-cards` to regenerate entry-point module docstrings from `LeanPool/projects.yml`. +Challenge-mode checks (the `Challenge/` library — open statements awaiting a proof, see [Challenge mode](../CONTRIBUTING.md#challenge-mode)): + +- every rule above applies to `Challenge/**/*.lean` too — header, no `set_option`, no `nolint`, no programmatic option manipulation, no unchecked declarations, no diagnostic commands, reachability from `Challenge.lean`, proof-size cap, and the environment backdoor audit +- `sorry` is allowed **only** in `Challenge/`, and only as the whole proof body of a declaration (`:= sorry`); a `sorry` buried in a larger term is rejected, and `admit` is rejected everywhere +- challenge statement files cap at 500 code lines and may import only `Mathlib.*` modules, so a statement never rests on pool code that could be refactored underneath it +- `Challenge/challenges.yml` exists and every entry carries `slug`, `title`, `summary`, `branch`, `entry_module`, `proposers`, `source` (at least one of `arxiv`/`doi`/`url`), `license`, `provenance`, `status`, `statements` (each with `declaration` and a nonempty `informal` statement), `tags`, and `msc`; `definitions` (definition holes) and a positive `estimated_lines` are optional +- `status` is `open` or `solved`; a solved challenge carries a `solution` block naming an in-repo `module`, a pool `project`, or a `url`, and an open one carries none +- slugs, entry modules, and open declaration names are unique; every declaration named in the registry lives in that challenge's namespace and is declared in its file; every statement file is registered +- generated challenge cards match `Challenge/challenges.yml` — the card carries the informal statement next to the Lean, which is what the [challenge review](CHALLENGE_REVIEW_RULES.md) judges faithfulness against +- `#print axioms` over the challenge library: declarations the registry lists as open must depend on `sorryAx` (a statement quietly proved in place is rejected — the statement is the contract solvers work against), every other declaration must not, and nothing may use an axiom outside the allowed set +- the environment audit tolerates a `sorryAx` reference only for registered open declarations and their generated companions; combined findings (`sorryAx` plus an axiom declaration, an option backdoor, ...) still fail + +Solution checks (the `Solution/` library — answers to challenges, see [Solving a challenge](../CONTRIBUTING.md#solving-a-challenge)): + +- solutions are held to the pool's rules, `sorry` included: a solution is a proof +- a solution may not import the challenge module it answers — comparator exports the two environments separately and compares them, and importing would inherit the statement instead of restating it +- every file under `Solution/` is the recorded `solution.module` of some challenge, and a solved challenge's solution module exists and declares every registered statement name (comparator matches challenge and solution by declaration name) +- `#print axioms` over the solution library, run in its own Lean process because a solution declares the same names as its challenge: no `sorryAx`, no axiom outside the allowed set. The environment backdoor audit runs separately over `Solution` for the same reason +- generated solution cards match the registry + +The checker also has `--write-project-cards` and `--write-challenge-cards` to regenerate entry-point module docstrings from `LeanPool/projects.yml` and `Challenge/challenges.yml` (the latter writes challenge *and* solution cards). ### 3. PR Separation @@ -58,8 +79,17 @@ Content files are: - `LeanPool.lean` - `LeanPool/**/*.lean` - `LeanPool/projects.yml` +- `Challenge.lean` +- `Challenge/**/*.lean` +- `Challenge/challenges.yml` +- `Solution.lean` +- `Solution/**/*.lean` -A PR may touch only content files or only non-content files. Mixing these categories fails CI, except that a Lean/Mathlib version bump may pair content with the toolchain, manifest, lakefile, their `docbuild/` equivalents, and this workflow. Branch protection to require this check before merge is future work. +A PR may touch only content files or only non-content files. Mixing these categories fails CI, except that a Lean/Mathlib version bump may pair content with the toolchain, manifest, lakefile, their `docbuild/` equivalents, and this workflow. Challenge statements and solutions count as content, so a PR that solves a challenge can add the answer, a pooled project, and the registry flip together. + +The same workflow enforces one challenge-mode rule: **a PR may not modify a challenge statement and touch a solution at the same time.** The merged statement is the text comparator judges a solution against, so editing it in the PR that claims to meet it is the one way to fake a solution past the kernel. Statement repairs land on their own. + +Branch protection to require these checks before merge is future work. ### 4. Python CI @@ -77,7 +107,18 @@ A PR may touch only content files or only non-content files. Mixing these catego ### 6. LLM Review -[`llm-review.yml`](workflows/llm-review.yml) runs after successful Lean Action CI on a PR head, or manually through `/review` and `workflow_dispatch`. It fetches the PR diff with `gh`, applies [`.github/REVIEW_RULES.md`](REVIEW_RULES.md), and posts a sticky PR comment containing the reviewed head SHA, structured assessment, verdict, findings, token counts, tier, and estimated cost. +[`llm-review.yml`](workflows/llm-review.yml) runs after successful Lean Action CI on a PR head, or manually through `/review` and `workflow_dispatch`. It fetches the PR diff with `gh`, classifies the PR, and posts a sticky PR comment containing the reviewed head SHA, structured assessment, verdict, findings, token counts, tier, and estimated cost. + +The rules applied depend on what the PR does: + +| PR kind | Detected by | Rules | +|---|---|---| +| project | adds a project directory that appears only through added `.lean` files | [`REVIEW_RULES.md`](REVIEW_RULES.md) — fit and significance | +| refactor | only touches projects already in the pool | [`REFACTOR_REVIEW_RULES.md`](REFACTOR_REVIEW_RULES.md) — tech debt and maintainability | +| challenge | adds a `Challenge/**/*.lean` statement, or edits one without touching pooled Lean content | [`CHALLENGE_REVIEW_RULES.md`](CHALLENGE_REVIEW_RULES.md) — significance, faithfulness of the Lean to the prose, source fidelity, vacuity/gameability, and the estimated size of a solution | +| solution | touches `Solution/**/*.lean` | [`SOLUTION_REVIEW_RULES.md`](SOLUTION_REVIEW_RULES.md) — statement tampering, definition-hole gaming, and proof quality. Correctness belongs to comparator (§11), not to the model | + +A solution PR is **not** sent to the model at all when it touches nothing but the answer, the generated index, and its registry entry, and the challenge leaves no definition hole: everything about such a PR is machine-checked, so the workflow posts a short note saying so instead. See `solution_needs_llm_review` in [`review.py`](../python/lean_pool/review.py). The review workflow checks out the base branch only. It does not execute PR-head code. @@ -118,12 +159,40 @@ Scheduled update checks are future work. check. Pushes to `main` build `LeanPool:docs` and deploy `docbuild/.lake/build/doc` to GitHub Pages. +### 11. Challenge Solution Verification + +[`challenge-verify.yml`](workflows/challenge-verify.yml) runs +[`leanprover/comparator`](https://github.com/leanprover/comparator) over every +challenge the registry records as solved. Comparator exports the challenge and +solution environments separately with `lean4export`, checks that the statements +agree, and replays the proof through the Lean kernel accepting no axiom beyond +`propext`, `Quot.sound`, and `Classical.choice`. This is what makes +`status: solved` a verified claim, and it is the check the solution review +defers to. + +The three external tools are pinned to exact commits and cached by pin: + +- `landrun` (the sandbox comparator runs builds under), built with Go from + `zouuup/landrun` +- `lean4export`, pinned to the tag matching [`lean-toolchain`](../lean-toolchain) + — it reads this repository's oleans, so its Lean version has to match +- `comparator` itself, which builds at its own (newer) toolchain + +Bumping any pin is a deliberate change: they are part of the trusted base for +every "solved" claim. The same pins are used by +[`leanprover/lean-eval`](https://github.com/leanprover/lean-eval). + +Like the Lean build, this workflow compiles pull-request code. It runs on +`pull_request`, so the token is read-only and no secret is in scope; landrun is +defence in depth on top of the ephemeral runner. + ## Future Work The following items are documented goals but are not fully implemented or enforced yet: - branch protection requiring the CI gates before merge - scheduled Lean/Mathlib update checks +- doc-gen4 pages for the `Challenge` and `Solution` libraries, so the board is browsable on the docs site alongside the pool - LeanExplore semantic dedup comments in PRs; the prototype CLI is [`python/lean_pool/semantic_dedup.py`](../python/lean_pool/semantic_dedup.py) - controlled tag vocabulary for `LeanPool/projects.yml`; tags are currently only checked as nonempty strings - generated domain/status indexes diff --git a/.github/SOLUTION_REVIEW_RULES.md b/.github/SOLUTION_REVIEW_RULES.md new file mode 100644 index 0000000000..32c0e89114 --- /dev/null +++ b/.github/SOLUTION_REVIEW_RULES.md @@ -0,0 +1,89 @@ +# Solution Review Rules + +You are reviewing a **solution** pull request to **Lean Pool**: it answers a +challenge that is already on the board. Keep this review short. Most of what +would normally be in question has already been settled by machines: + +- **Correctness is not yours to judge.** `leanprover/comparator` replays the + solution through the Lean kernel and checks that it proves *the same* + statement as the challenge module using no axiom beyond `propext`, + `Quot.sound`, and `Classical.choice`. Its verdict is a separate CI check. + Never say a proof is right or wrong; you cannot see the challenge statement + unless the PR changed it. +- **Significance was settled when the challenge merged.** Do not re-litigate + whether the problem was worth stating. +- **Mechanics are gated.** `sorry`, axioms, headers, imports (a solution may + not import the challenge module), size caps, the registry schema, generated + cards, and the `status: solved` bookkeeping all fail CI on their own. + +## What is left for you + +1. **Statement tampering.** If the diff touches any file under `Challenge/`, + say so loudly and quote the change. A merged statement is the text every + solver works against, and editing it in the same PR that claims to solve + it is how a hard problem quietly becomes an easy one. This alone is + grounds for `request_changes`. +2. **Definition holes.** If the challenge left a `def ... := sorry` for the + solver to fill in, comparator only checks that the name, type, universes, + and safety level match. A solution can define the hole in terms of the + very object the challenge asks about — the classic + `def ChallengeSolution : Prop := RiemannHypothesis` move. Read the filled + hole and say whether it answers the question or restates it. +3. **Proof quality.** The pool's usual standard: is this a proof a maintainer + would be content to keep building against Mathlib, or is it agent slop — + walls of repeated `have`s, dead branches, an opaque `simp_all` where a + structured argument was there to be written? Brittleness matters here for + the same reason it does in a refactor: someone has to fix it at the next + bump. +4. **Delegated work.** A large solution may prove the real content in a + pooled project and leave a thin bridge module under `Solution/`. If the + PR adds such a project, the project's own standards apply — card, source + anchor, provenance, and no slop. + +## Out of scope — do not flag + +- Whether the theorem is actually proved (comparator's job). +- The mathematical interest of the problem (settled at challenge time). +- `sorry`, axioms, headers, naming, line length, imports, size caps, registry + fields, card sync (all gated). +- That the solution restates the challenge statement instead of importing it + — that is required, and enforced. + +## Output + +Return a single JSON object: + +```json +{ + "summary": "", + "assessment": { + "touches_challenge_statement": , + "definition_hole_risk": "none" | "review_needed" | "gamed", + "proof_quality": , + "assessment_one_sentence": "" + }, + "verdict": "approve" | "request_changes" | "needs_discussion", + "findings": [ + { + "file": "", + "line": , + "rule": "", + "comment": "" + } + ] +} +``` + +Verdict mapping: + +- `approve` — nothing but a proof, and a decent one. This is the common case; + an empty `findings` list is correct. +- `request_changes` — the PR edits the challenge statement, games a + definition hole, or the proof is bad enough to reject on quality grounds. +- `needs_discussion` — a definition hole that needs a human eye, or a + judgment call about a delegated project. + +## Style + +- Be brief. A clean solution deserves two sentences, not an essay. +- Do not restate the comparator result; it has its own check. diff --git a/.github/workflows/challenge-verify.yml b/.github/workflows/challenge-verify.yml new file mode 100644 index 0000000000..de86e436db --- /dev/null +++ b/.github/workflows/challenge-verify.yml @@ -0,0 +1,158 @@ +name: Verify challenge solutions + +# Replays every solved challenge through `leanprover/comparator`: it exports +# the challenge and solution environments separately, checks that the solution +# proves the *same* statement, and re-checks the proof in the Lean kernel with +# no axiom beyond propext / Quot.sound / Classical.choice. This is what makes +# `status: solved` in Challenge/challenges.yml a verified claim rather than an +# assertion, and it is the check the solution review defers to. +# +# The three external tools are pinned to exact commits, because they are part +# of the trusted base for that claim. Bumping one is a deliberate change, not a +# floating `@main`. The same pins are what leanprover/lean-eval uses. +# +# This workflow compiles pull-request code, exactly as the Lean build does. It +# runs on `pull_request`, so the token is read-only and no secret is exposed; +# landrun is defence in depth on top of the ephemeral runner. + +on: + pull_request: + branches: + - main + paths: + - 'Challenge/**' + - 'Challenge.lean' + - 'Solution/**' + - 'Solution.lean' + - 'lean-toolchain' + - 'lake-manifest.json' + - 'lakefile.toml' + - 'scripts/challenge/**' + - 'python/lean_pool/challenge.py' + - '.github/workflows/challenge-verify.yml' + push: + branches: + - main + paths: + - 'Challenge/**' + - 'Challenge.lean' + - 'Solution/**' + - 'Solution.lean' + workflow_dispatch: + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +env: + # landrun: zouuup/landrun main HEAD as of 2026-05-04. Tagged releases + # through v0.1.15 lack fixes comparator needs, so this is a commit pin. + LANDRUN_COMMIT: 5ed4a3db3a4ad930d577215c6b9abaa19df7f99f + # lean4export at refs/tags/v4.32.0-rc1 — it must match this repository's + # lean-toolchain, because it reads the oleans the build produced. + LEAN4EXPORT_COMMIT: 3de59f10bc4b4a0f2de698597aeb1246caa0df0a + COMPARATOR_COMMIT: 71b52ec29e06d4b7d882726553b1ceb99a2499e0 + +jobs: + verify: + runs-on: ubuntu-latest + name: Verify challenge solutions + steps: + - name: Checkout project + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + + - name: Restore caches + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: | + ~/.elan + .lake/packages + .lake/build + key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + restore-keys: | + Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + + - 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: Install Mathlib cache + run: | + if [ ! -d ".lake/packages/mathlib" ]; then + ~/.elan/bin/lake exe cache get + else + echo "Mathlib already present from cache" + fi + + - name: Cache verification tools + id: tools + uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: | + ~/go/bin/landrun + .ci/lean4export/.lake/build/bin/lean4export + .ci/comparator/.lake/build/bin/comparator + key: >- + challenge-tools-${{ runner.os }}-${{ env.LANDRUN_COMMIT }}-${{ + env.LEAN4EXPORT_COMMIT }}-${{ env.COMPARATOR_COMMIT }}-${{ + hashFiles('lean-toolchain') }} + + # actions/setup-go pinned to d35c59ab (= refs/tags/v5.5.0), the pin + # leanprover/lean-eval uses to build the same landrun commit. + - name: Set up Go + if: steps.tools.outputs.cache-hit != 'true' + uses: actions/setup-go@d35c59abb061a4a6fb18e82ac0862c26744d6ab5 + with: + go-version: '1.24.0' + + - name: Build landrun + if: steps.tools.outputs.cache-hit != 'true' + run: go install "github.com/zouuup/landrun/cmd/landrun@$LANDRUN_COMMIT" + + - name: Build lean4export + if: steps.tools.outputs.cache-hit != 'true' + run: | + set -euo pipefail + git clone https://github.com/leanprover/lean4export.git .ci/lean4export + cd .ci/lean4export + git checkout "$LEAN4EXPORT_COMMIT" + ~/.elan/bin/lake build lean4export + + - name: Build comparator + if: steps.tools.outputs.cache-hit != 'true' + run: | + set -euo pipefail + git clone https://github.com/leanprover/comparator.git .ci/comparator + cd .ci/comparator + git checkout "$COMPARATOR_COMMIT" + ~/.elan/bin/lake build comparator + + - name: Verify every solved challenge + env: + COMPARATOR_LANDRUN: /home/runner/go/bin/landrun + run: | + set -euo pipefail + export PATH="$HOME/.elan/bin:$PATH" + slugs=$(cd python && uv run python -m lean_pool.challenge --repo .. solved) + if [ -z "$slugs" ]; then + echo "No solved challenges to verify." + exit 0 + fi + for slug in $slugs; do + echo "::group::comparator: $slug" + scripts/challenge/verify-solution.sh "$slug" \ + --comparator "$PWD/.ci/comparator/.lake/build/bin/comparator" \ + --lean4export "$PWD/.ci/lean4export/.lake/build/bin/lean4export" + echo "::endgroup::" + done diff --git a/.github/workflows/content-pr-guard.yml b/.github/workflows/content-pr-guard.yml index d9242c23fe..3899b46e0c 100644 --- a/.github/workflows/content-pr-guard.yml +++ b/.github/workflows/content-pr-guard.yml @@ -5,6 +5,17 @@ name: PR Separation Guard # - LeanPool.lean # - LeanPool/**/*.lean # - LeanPool/projects.yml +# - Challenge/**/*.lean +# - Challenge/challenges.yml +# - Solution/**/*.lean +# Challenge statements and their solutions count as content: they are +# formalization material reviewed on their mathematics, and a PR that solves a +# challenge legitimately adds a pooled project alongside the registry flip. +# `Challenge.lean` and `Solution.lean` are neutral — generated indexes with no +# mathematics in them, which have to exist before anything can be added to +# those libraries — so they may accompany either category. +# One extra rule applies here: a PR may not edit a challenge statement and a +# solution together; see the check below. # A PR may touch only content files, or only non-content files (.github/, # python/, scripts/, docs, lakefile.toml, lean-toolchain, etc.). Mixing both # categories fails this gate, except for Lean/lake version-bump metadata. @@ -61,8 +72,35 @@ jobs: printf '%s\n' "$files" | sed 's/^/ /' echo - # Content: the mk_all index, any .lean under LeanPool/, projects.yml. - content_re='^(LeanPool\.lean|LeanPool/.+\.lean|LeanPool/projects\.yml)$' + # Content: the pool index, any .lean under LeanPool/, Challenge/ or + # Solution/, and the two registries. + content_re='^(LeanPool\.lean|LeanPool/.+\.lean|LeanPool/projects\.yml|Challenge/.+\.lean|Challenge/challenges\.yml|Solution/.+\.lean)$' + + # Neutral: the generated indexes of the challenge libraries. They are + # `lake exe mk_all` output with no mathematics in them, and the + # libraries have to exist — with empty indexes — before any statement + # can be added to them, so they may accompany either category. + neutral_re='^(Challenge\.lean|Solution\.lean)$' + files="$(printf '%s\n' "$files" | { grep -vE "$neutral_re" || true; })" + + # A solution PR may not edit the statement it claims to solve: the + # merged statement is the text comparator judges against, and + # changing it in the same PR is how a hard problem quietly becomes + # an easy one. Land statement repairs separately. + edited_statements="$(gh api "repos/$REPO/pulls/$PR_NUMBER/files" --paginate \ + --jq '.[] | select(.status == "modified") | .filename' \ + | { grep -E '^Challenge/.+\.lean$' || true; })" + touched_solutions="$(printf '%s\n' "$files" | { grep -E '^Solution/.+\.lean$' || true; })" + if [ -n "$edited_statements" ] && [ -n "$touched_solutions" ]; then + echo "::error::This PR edits a challenge statement and a solution together." + echo "Statements are the text solutions are judged against; edit them in" + echo "their own PR so the change is reviewed on its own terms." + while IFS= read -r f; do + [ -n "$f" ] || continue + echo "::error file=$f::challenge statement modified alongside a solution" + done <<< "$edited_statements" + exit 1 + fi content="$(printf '%s\n' "$files" | { grep -E "$content_re" || true; })" non_content="$(printf '%s\n' "$files" | { grep -vE "$content_re" || true; })" @@ -86,6 +124,11 @@ jobs: echo " - LeanPool.lean" echo " - LeanPool/**/*.lean" echo " - LeanPool/projects.yml" + echo " - Challenge/**/*.lean" + echo " - Challenge/challenges.yml" + echo " - Solution/**/*.lean" + echo "(Challenge.lean and Solution.lean are generated indexes and" + echo " may accompany either category.)" echo "(Exception: a version bump may also touch lean-toolchain," echo " lake-manifest.json, and lakefile.toml.)" echo diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index efc834ddf4..519ae68c54 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -7,6 +7,7 @@ on: paths: - '**/*.lean' - 'LeanPool/projects.yml' + - 'Challenge/challenges.yml' - 'lakefile.toml' - 'lake-manifest.json' - 'lean-toolchain' @@ -19,6 +20,7 @@ on: paths: - '**/*.lean' - 'LeanPool/projects.yml' + - 'Challenge/challenges.yml' - 'lakefile.toml' - 'lake-manifest.json' - 'lean-toolchain' @@ -153,9 +155,15 @@ jobs: echo "Mathlib already present from cache" fi + # The challenge board is documented alongside the pool: each statement's + # card carries the informal statement it is judged against, which is + # worth reading on the docs site. `Solution:docs` is deliberately not + # built — a solution restates its challenge's declarations under the same + # names, so rendering both into one doc tree would produce two pages + # claiming the same declaration. - name: Build documentation id: build - run: cd docbuild && ~/.elan/bin/lake build LeanPool:docs + run: cd docbuild && ~/.elan/bin/lake build LeanPool:docs Challenge:docs - name: Add exposition site # Wait for the parallel `exposition` job's artifact and merge it into diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index a288027e1e..c605deffc2 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -30,6 +30,8 @@ on: - 'lean-toolchain' - 'lake-manifest.json' - 'LeanPool/projects.yml' + - 'Challenge/challenges.yml' + - 'python/lean_pool/challenge.py' - 'python/lean_pool/quality.py' - 'python/pyproject.toml' - 'python/uv.lock' @@ -46,6 +48,8 @@ on: - 'lean-toolchain' - 'lake-manifest.json' - 'LeanPool/projects.yml' + - 'Challenge/challenges.yml' + - 'python/lean_pool/challenge.py' - 'python/lean_pool/quality.py' - 'python/pyproject.toml' - 'python/uv.lock' @@ -199,11 +203,20 @@ jobs: exit 1 fi + - name: Build challenges and solutions + run: ./scripts/ci/build-challenges.sh + - name: Lint - run: ~/.elan/bin/lake exe runLinter LeanPool + run: | + ~/.elan/bin/lake exe runLinter LeanPool + ~/.elan/bin/lake exe runLinter Challenge + ~/.elan/bin/lake exe runLinter Solution - name: Text style lint - run: ~/.elan/bin/lake exe lint-style LeanPool + run: | + ~/.elan/bin/lake exe lint-style LeanPool + ~/.elan/bin/lake exe lint-style Challenge + ~/.elan/bin/lake exe lint-style Solution - name: Repository quality checks run: | @@ -392,11 +405,20 @@ jobs: exit 1 fi + - name: Build challenges and solutions + run: ./scripts/ci/build-challenges.sh + - name: Lint - run: ~/.elan/bin/lake exe runLinter LeanPool + run: | + ~/.elan/bin/lake exe runLinter LeanPool + ~/.elan/bin/lake exe runLinter Challenge + ~/.elan/bin/lake exe runLinter Solution - name: Text style lint - run: ~/.elan/bin/lake exe lint-style LeanPool + run: | + ~/.elan/bin/lake exe lint-style LeanPool + ~/.elan/bin/lake exe lint-style Challenge + ~/.elan/bin/lake exe lint-style Solution - name: Repository quality checks run: | diff --git a/.github/workflows/readme-stats.yml b/.github/workflows/readme-stats.yml index 6734c37f92..d6b4791c72 100644 --- a/.github/workflows/readme-stats.yml +++ b/.github/workflows/readme-stats.yml @@ -9,6 +9,7 @@ on: # cannot re-trigger this workflow (no commit loop). paths: - 'LeanPool/**' + - 'Challenge/**' - 'python/lean_pool/stats.py' - '.github/workflows/readme-stats.yml' workflow_dispatch: diff --git a/AGENTS.md b/AGENTS.md index c81e8af66d..36e4cdc1e7 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -33,6 +33,21 @@ make setup # pull Mathlib oleans, build the whole pool (~1.5h), install Pytho To work on a single project you don't need the whole pool built — see the [fast per-project build](CONTRIBUTING.md#dev-setup) in `CONTRIBUTING.md`. +### Challenge mode + +[`Challenge/`](Challenge/) is the other half of the pool: open *statements* rather than finished proofs. A challenge is a theorem written in Mathlib vocabulary and left as `sorry`, registered in [`Challenge/challenges.yml`](Challenge/challenges.yml) alongside the English statement it is supposed to say. It is the only place `sorry` is allowed, and only for the declarations the registry lists — everything else in the file must be closed, and every other gate still applies. + +Anyone can propose one. The [LLM reviewer](.github/CHALLENGE_REVIEW_RULES.md) judges a challenge on different grounds than a project: whether the problem is significant, whether the Lean faithfully says what the prose says, whether a cited known result is stated the way its source states it, whether the statement is vacuous or gameable, and how many lines of Lean a solution would take. + +Anyone can answer one, too. A solution lands in [`Solution/`](Solution/), restating the statement and proving it, and [`leanprover/comparator`](https://github.com/leanprover/comparator) settles whether it counts: [CI](.github/workflows/challenge-verify.yml) exports the challenge and solution environments separately, checks that the statements agree, and replays the proof through the Lean kernel with no axiom beyond `propext`/`Quot.sound`/`Classical.choice`. Because a kernel decides correctness, the [solution review](.github/SOLUTION_REVIEW_RULES.md) is short — and is skipped entirely when the PR adds nothing but the answer. + +```bash +make challenges # what's on the board +make verify-challenge C= # replay a solution locally +``` + +See [Challenge mode](CONTRIBUTING.md#challenge-mode) in `CONTRIBUTING.md`. + ### Contributing See [`CONTRIBUTING.md`](CONTRIBUTING.md). @@ -65,6 +80,41 @@ There are two paths: Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.) +## Challenge mode + +A **challenge** is the mirror image of a project: instead of a finished proof, it is an open *statement* — a theorem written in Mathlib vocabulary, left as `sorry`, that the pool is asking someone to prove. Challenges live in [`Challenge/`](Challenge/), the only place in the repository where `sorry` is allowed. Browse the board with `make challenges`. + +Anyone can submit one. Open a content PR that adds: + +- `Challenge/.lean` — the statement, with the standard four-line file header, imports **only** from `Mathlib.*`, and each open declaration proved by exactly `:= sorry`; +- an entry in [`Challenge/challenges.yml`](Challenge/challenges.yml) — `slug`, `title`, `summary`, `branch`, `entry_module`, `proposers`, `source`, `license`, `provenance`, `status: open`, `statements` (each with a `declaration` and its `informal` English statement), `tags`, `msc`, plus optional `definitions` (definition holes) and `estimated_lines`; +- the regenerated indexes: `lake exe mk_all` and `cd python && uv run python -m lean_pool.quality --repo .. --write-challenge-cards`. + +The gates then enforce that the board stays honest: `sorry` appears only as the whole proof body of a declaration the registry lists, every *other* declaration in the file is closed (checked with `#print axioms`, so scaffolding can't hide behind an open statement), the registered statements really are open, imports are Mathlib-only, and the generated card matches the registry. Everything else — headers, `set_option`, axioms, the option-backdoor audit, size caps — applies exactly as it does to pooled projects. + +A challenge PR gets its own [LLM review](.github/CHALLENGE_REVIEW_RULES.md), which asks a different question than the project review: is the problem significant (both informally and as formalized), does the Lean statement faithfully say what the prose says, does a cited known result match its source, is the statement vacuous or gameable, and roughly how many lines of Lean would a solution take. + +## Solving a challenge + +A challenge statement never changes once merged: it is the text every solution is judged against. So a solution goes in [`Solution/`](Solution/) as its own module, which **restates** the statement under the same name and proves it. It must not import the challenge module — comparator exports the two environments separately and checks that the statements agree, and importing would defeat exactly that check (a gate enforces it). + +Open a content PR that adds `Solution/.lean` and flips the registry entry to `status: solved` with a `solution:` block (`module:`, plus optional `authors:`, `project:`, and `verified:`), then regenerate the index and cards. A solution that needs real work should prove it in a pooled project under `LeanPool/` and leave a thin bridge here. + +Correctness is decided by [`leanprover/comparator`](https://github.com/leanprover/comparator), which replays the solution through the Lean kernel and checks that it proves *the same* statement with no axiom beyond `propext`/`Quot.sound`/`Classical.choice`. [`challenge-verify.yml`](.github/workflows/challenge-verify.yml) runs it on every solved challenge in CI, with `landrun`, `lean4export`, and comparator pinned to exact commits. Locally: + +```bash +make comparator # one-time: build the judge +make verify-challenge C= # replay a solution +``` + +`make comparator` also builds a `lean4export` at this repository's toolchain (comparator pins a newer one, which cannot read our oleans). Sandboxing needs [`landrun`](https://github.com/Zouuup/landrun), which is Linux-only; elsewhere pass `--insecure-no-sandbox` to `scripts/challenge/verify-solution.sh` and understand that compiling a solution runs its code. `python -m lean_pool.challenge config ` prints the JSON configuration if you want to drive comparator yourself. + +A failed verification is loud rather than tidy: a solution missing the theorem ends in a `lean4export` panic ("Constant … not found in environment"), a weakened statement in `Challenge and solution theorem statement do not match`, and one that still leans on `sorry` in `Illegal axiom detected: 'sorryAx'`. All are rejections — the script exits non-zero and prints the `Verified:` line only on success. + +Because a kernel decides correctness, the [solution review](.github/SOLUTION_REVIEW_RULES.md) is deliberately thin, and is skipped altogether when the PR touches nothing but the answer, the generated index, and the registry entry. It runs when there is something a machine cannot settle: a definition hole, a pooled project to judge as a project, or anything else in the diff. Editing a challenge statement in the same PR as a solution is rejected outright by the PR guard. + +**Definition holes.** A challenge may leave a `def ... := sorry` for the solver to fill in (register it under `definitions:`). Comparator only checks that the name, type, universes, and safety level match, so a hole can be gamed — a solution may define it in terms of the very object the challenge asks about. Holes always need human review on top of a green comparator run. + ## Dev setup Requires Lean (via [`elan`](https://leanprover-community.github.io/install/), with the toolchain pinned in [`lean-toolchain`](lean-toolchain)) and Python 3.13+ with [`uv`](https://docs.astral.sh/uv/). @@ -80,19 +130,20 @@ cd python && uv sync # Python tooling only; add `--group test` for pytest lake exe cache get # prebuilt Mathlib oleans (fast) lake build LeanPool.YourProject # builds only your project — minutes, not hours # or: make build-project P=YourProject +lake build Challenge # the whole challenge board — seconds ``` The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style LeanPool`, the quality checker) do need the full pool built, but CI runs them on your PR — you don't have to reproduce them locally. ## Pull requests -- **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool.lean`, `LeanPool/**/*.lean`, and `LeanPool/projects.yml`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. This is enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml). +- **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool.lean`, `LeanPool/**/*.lean`, `LeanPool/projects.yml`, `Challenge.lean`, `Challenge/**/*.lean`, `Challenge/challenges.yml`, `Solution.lean`, and `Solution/**/*.lean`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. The same guard rejects a PR that edits a challenge statement alongside a solution. Both are enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml). - **Never change the checks or gates.** Do not modify `.github/workflows/`, `.github/CODE_QUALITY.md`, `python/lean_pool/quality.py`, `scripts/nolints-style.txt`, the `[leanOptions]`/lint settings in `lakefile.toml`, or any other CI step or linter config — and do not add a waiver of any kind (a `size-limit-ok` comment, a `nolints-style.txt` entry, `set_option linter.X false`, etc.) — unless explicitly asked. If a check fails, fix the code, not the check. This applies to everyone, and especially to AI agents. - **Branches.** `yourname/description` for solo work; `feature/`/`fix/` prefixes when shared. Open PRs early (draft + `WIP` is fine) and use `Closes #123` to link issues. ## Linting and testing -**Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `lake exe runLinter LeanPool`, `lake exe lint-style LeanPool`, and the quality checker (see [`lean_action_ci.yml`](.github/workflows/lean_action_ci.yml)). Conventions live in [`.github/CODE_QUALITY.md`](.github/CODE_QUALITY.md). +**Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `scripts/ci/build-challenges.sh` (the `Challenge`/`Solution` build, where only the expected `sorry` notices are tolerated), `lake exe runLinter` and `lake exe lint-style` on all three libraries, the quality checker (see [`lean_action_ci.yml`](.github/workflows/lean_action_ci.yml)), and comparator on every solved challenge (see [`challenge-verify.yml`](.github/workflows/challenge-verify.yml)). Conventions live in [`.github/CODE_QUALITY.md`](.github/CODE_QUALITY.md). **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`. diff --git a/CLAUDE.md b/CLAUDE.md index c81e8af66d..36e4cdc1e7 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -33,6 +33,21 @@ make setup # pull Mathlib oleans, build the whole pool (~1.5h), install Pytho To work on a single project you don't need the whole pool built — see the [fast per-project build](CONTRIBUTING.md#dev-setup) in `CONTRIBUTING.md`. +### Challenge mode + +[`Challenge/`](Challenge/) is the other half of the pool: open *statements* rather than finished proofs. A challenge is a theorem written in Mathlib vocabulary and left as `sorry`, registered in [`Challenge/challenges.yml`](Challenge/challenges.yml) alongside the English statement it is supposed to say. It is the only place `sorry` is allowed, and only for the declarations the registry lists — everything else in the file must be closed, and every other gate still applies. + +Anyone can propose one. The [LLM reviewer](.github/CHALLENGE_REVIEW_RULES.md) judges a challenge on different grounds than a project: whether the problem is significant, whether the Lean faithfully says what the prose says, whether a cited known result is stated the way its source states it, whether the statement is vacuous or gameable, and how many lines of Lean a solution would take. + +Anyone can answer one, too. A solution lands in [`Solution/`](Solution/), restating the statement and proving it, and [`leanprover/comparator`](https://github.com/leanprover/comparator) settles whether it counts: [CI](.github/workflows/challenge-verify.yml) exports the challenge and solution environments separately, checks that the statements agree, and replays the proof through the Lean kernel with no axiom beyond `propext`/`Quot.sound`/`Classical.choice`. Because a kernel decides correctness, the [solution review](.github/SOLUTION_REVIEW_RULES.md) is short — and is skipped entirely when the PR adds nothing but the answer. + +```bash +make challenges # what's on the board +make verify-challenge C= # replay a solution locally +``` + +See [Challenge mode](CONTRIBUTING.md#challenge-mode) in `CONTRIBUTING.md`. + ### Contributing See [`CONTRIBUTING.md`](CONTRIBUTING.md). @@ -65,6 +80,41 @@ There are two paths: Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.) +## Challenge mode + +A **challenge** is the mirror image of a project: instead of a finished proof, it is an open *statement* — a theorem written in Mathlib vocabulary, left as `sorry`, that the pool is asking someone to prove. Challenges live in [`Challenge/`](Challenge/), the only place in the repository where `sorry` is allowed. Browse the board with `make challenges`. + +Anyone can submit one. Open a content PR that adds: + +- `Challenge/.lean` — the statement, with the standard four-line file header, imports **only** from `Mathlib.*`, and each open declaration proved by exactly `:= sorry`; +- an entry in [`Challenge/challenges.yml`](Challenge/challenges.yml) — `slug`, `title`, `summary`, `branch`, `entry_module`, `proposers`, `source`, `license`, `provenance`, `status: open`, `statements` (each with a `declaration` and its `informal` English statement), `tags`, `msc`, plus optional `definitions` (definition holes) and `estimated_lines`; +- the regenerated indexes: `lake exe mk_all` and `cd python && uv run python -m lean_pool.quality --repo .. --write-challenge-cards`. + +The gates then enforce that the board stays honest: `sorry` appears only as the whole proof body of a declaration the registry lists, every *other* declaration in the file is closed (checked with `#print axioms`, so scaffolding can't hide behind an open statement), the registered statements really are open, imports are Mathlib-only, and the generated card matches the registry. Everything else — headers, `set_option`, axioms, the option-backdoor audit, size caps — applies exactly as it does to pooled projects. + +A challenge PR gets its own [LLM review](.github/CHALLENGE_REVIEW_RULES.md), which asks a different question than the project review: is the problem significant (both informally and as formalized), does the Lean statement faithfully say what the prose says, does a cited known result match its source, is the statement vacuous or gameable, and roughly how many lines of Lean would a solution take. + +## Solving a challenge + +A challenge statement never changes once merged: it is the text every solution is judged against. So a solution goes in [`Solution/`](Solution/) as its own module, which **restates** the statement under the same name and proves it. It must not import the challenge module — comparator exports the two environments separately and checks that the statements agree, and importing would defeat exactly that check (a gate enforces it). + +Open a content PR that adds `Solution/.lean` and flips the registry entry to `status: solved` with a `solution:` block (`module:`, plus optional `authors:`, `project:`, and `verified:`), then regenerate the index and cards. A solution that needs real work should prove it in a pooled project under `LeanPool/` and leave a thin bridge here. + +Correctness is decided by [`leanprover/comparator`](https://github.com/leanprover/comparator), which replays the solution through the Lean kernel and checks that it proves *the same* statement with no axiom beyond `propext`/`Quot.sound`/`Classical.choice`. [`challenge-verify.yml`](.github/workflows/challenge-verify.yml) runs it on every solved challenge in CI, with `landrun`, `lean4export`, and comparator pinned to exact commits. Locally: + +```bash +make comparator # one-time: build the judge +make verify-challenge C= # replay a solution +``` + +`make comparator` also builds a `lean4export` at this repository's toolchain (comparator pins a newer one, which cannot read our oleans). Sandboxing needs [`landrun`](https://github.com/Zouuup/landrun), which is Linux-only; elsewhere pass `--insecure-no-sandbox` to `scripts/challenge/verify-solution.sh` and understand that compiling a solution runs its code. `python -m lean_pool.challenge config ` prints the JSON configuration if you want to drive comparator yourself. + +A failed verification is loud rather than tidy: a solution missing the theorem ends in a `lean4export` panic ("Constant … not found in environment"), a weakened statement in `Challenge and solution theorem statement do not match`, and one that still leans on `sorry` in `Illegal axiom detected: 'sorryAx'`. All are rejections — the script exits non-zero and prints the `Verified:` line only on success. + +Because a kernel decides correctness, the [solution review](.github/SOLUTION_REVIEW_RULES.md) is deliberately thin, and is skipped altogether when the PR touches nothing but the answer, the generated index, and the registry entry. It runs when there is something a machine cannot settle: a definition hole, a pooled project to judge as a project, or anything else in the diff. Editing a challenge statement in the same PR as a solution is rejected outright by the PR guard. + +**Definition holes.** A challenge may leave a `def ... := sorry` for the solver to fill in (register it under `definitions:`). Comparator only checks that the name, type, universes, and safety level match, so a hole can be gamed — a solution may define it in terms of the very object the challenge asks about. Holes always need human review on top of a green comparator run. + ## Dev setup Requires Lean (via [`elan`](https://leanprover-community.github.io/install/), with the toolchain pinned in [`lean-toolchain`](lean-toolchain)) and Python 3.13+ with [`uv`](https://docs.astral.sh/uv/). @@ -80,19 +130,20 @@ cd python && uv sync # Python tooling only; add `--group test` for pytest lake exe cache get # prebuilt Mathlib oleans (fast) lake build LeanPool.YourProject # builds only your project — minutes, not hours # or: make build-project P=YourProject +lake build Challenge # the whole challenge board — seconds ``` The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style LeanPool`, the quality checker) do need the full pool built, but CI runs them on your PR — you don't have to reproduce them locally. ## Pull requests -- **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool.lean`, `LeanPool/**/*.lean`, and `LeanPool/projects.yml`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. This is enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml). +- **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool.lean`, `LeanPool/**/*.lean`, `LeanPool/projects.yml`, `Challenge.lean`, `Challenge/**/*.lean`, `Challenge/challenges.yml`, `Solution.lean`, and `Solution/**/*.lean`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. The same guard rejects a PR that edits a challenge statement alongside a solution. Both are enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml). - **Never change the checks or gates.** Do not modify `.github/workflows/`, `.github/CODE_QUALITY.md`, `python/lean_pool/quality.py`, `scripts/nolints-style.txt`, the `[leanOptions]`/lint settings in `lakefile.toml`, or any other CI step or linter config — and do not add a waiver of any kind (a `size-limit-ok` comment, a `nolints-style.txt` entry, `set_option linter.X false`, etc.) — unless explicitly asked. If a check fails, fix the code, not the check. This applies to everyone, and especially to AI agents. - **Branches.** `yourname/description` for solo work; `feature/`/`fix/` prefixes when shared. Open PRs early (draft + `WIP` is fine) and use `Closes #123` to link issues. ## Linting and testing -**Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `lake exe runLinter LeanPool`, `lake exe lint-style LeanPool`, and the quality checker (see [`lean_action_ci.yml`](.github/workflows/lean_action_ci.yml)). Conventions live in [`.github/CODE_QUALITY.md`](.github/CODE_QUALITY.md). +**Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `scripts/ci/build-challenges.sh` (the `Challenge`/`Solution` build, where only the expected `sorry` notices are tolerated), `lake exe runLinter` and `lake exe lint-style` on all three libraries, the quality checker (see [`lean_action_ci.yml`](.github/workflows/lean_action_ci.yml)), and comparator on every solved challenge (see [`challenge-verify.yml`](.github/workflows/challenge-verify.yml)). Conventions live in [`.github/CODE_QUALITY.md`](.github/CODE_QUALITY.md). **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 8dff437cf9..39b5dd797d 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -15,6 +15,41 @@ There are two paths: Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.) +## Challenge mode + +A **challenge** is the mirror image of a project: instead of a finished proof, it is an open *statement* — a theorem written in Mathlib vocabulary, left as `sorry`, that the pool is asking someone to prove. Challenges live in [`Challenge/`](Challenge/), the only place in the repository where `sorry` is allowed. Browse the board with `make challenges`. + +Anyone can submit one. Open a content PR that adds: + +- `Challenge/.lean` — the statement, with the standard four-line file header, imports **only** from `Mathlib.*`, and each open declaration proved by exactly `:= sorry`; +- an entry in [`Challenge/challenges.yml`](Challenge/challenges.yml) — `slug`, `title`, `summary`, `branch`, `entry_module`, `proposers`, `source`, `license`, `provenance`, `status: open`, `statements` (each with a `declaration` and its `informal` English statement), `tags`, `msc`, plus optional `definitions` (definition holes) and `estimated_lines`; +- the regenerated indexes: `lake exe mk_all` and `cd python && uv run python -m lean_pool.quality --repo .. --write-challenge-cards`. + +The gates then enforce that the board stays honest: `sorry` appears only as the whole proof body of a declaration the registry lists, every *other* declaration in the file is closed (checked with `#print axioms`, so scaffolding can't hide behind an open statement), the registered statements really are open, imports are Mathlib-only, and the generated card matches the registry. Everything else — headers, `set_option`, axioms, the option-backdoor audit, size caps — applies exactly as it does to pooled projects. + +A challenge PR gets its own [LLM review](.github/CHALLENGE_REVIEW_RULES.md), which asks a different question than the project review: is the problem significant (both informally and as formalized), does the Lean statement faithfully say what the prose says, does a cited known result match its source, is the statement vacuous or gameable, and roughly how many lines of Lean would a solution take. + +## Solving a challenge + +A challenge statement never changes once merged: it is the text every solution is judged against. So a solution goes in [`Solution/`](Solution/) as its own module, which **restates** the statement under the same name and proves it. It must not import the challenge module — comparator exports the two environments separately and checks that the statements agree, and importing would defeat exactly that check (a gate enforces it). + +Open a content PR that adds `Solution/.lean` and flips the registry entry to `status: solved` with a `solution:` block (`module:`, plus optional `authors:`, `project:`, and `verified:`), then regenerate the index and cards. A solution that needs real work should prove it in a pooled project under `LeanPool/` and leave a thin bridge here. + +Correctness is decided by [`leanprover/comparator`](https://github.com/leanprover/comparator), which replays the solution through the Lean kernel and checks that it proves *the same* statement with no axiom beyond `propext`/`Quot.sound`/`Classical.choice`. [`challenge-verify.yml`](.github/workflows/challenge-verify.yml) runs it on every solved challenge in CI, with `landrun`, `lean4export`, and comparator pinned to exact commits. Locally: + +```bash +make comparator # one-time: build the judge +make verify-challenge C= # replay a solution +``` + +`make comparator` also builds a `lean4export` at this repository's toolchain (comparator pins a newer one, which cannot read our oleans). Sandboxing needs [`landrun`](https://github.com/Zouuup/landrun), which is Linux-only; elsewhere pass `--insecure-no-sandbox` to `scripts/challenge/verify-solution.sh` and understand that compiling a solution runs its code. `python -m lean_pool.challenge config ` prints the JSON configuration if you want to drive comparator yourself. + +A failed verification is loud rather than tidy: a solution missing the theorem ends in a `lean4export` panic ("Constant … not found in environment"), a weakened statement in `Challenge and solution theorem statement do not match`, and one that still leans on `sorry` in `Illegal axiom detected: 'sorryAx'`. All are rejections — the script exits non-zero and prints the `Verified:` line only on success. + +Because a kernel decides correctness, the [solution review](.github/SOLUTION_REVIEW_RULES.md) is deliberately thin, and is skipped altogether when the PR touches nothing but the answer, the generated index, and the registry entry. It runs when there is something a machine cannot settle: a definition hole, a pooled project to judge as a project, or anything else in the diff. Editing a challenge statement in the same PR as a solution is rejected outright by the PR guard. + +**Definition holes.** A challenge may leave a `def ... := sorry` for the solver to fill in (register it under `definitions:`). Comparator only checks that the name, type, universes, and safety level match, so a hole can be gamed — a solution may define it in terms of the very object the challenge asks about. Holes always need human review on top of a green comparator run. + ## Dev setup Requires Lean (via [`elan`](https://leanprover-community.github.io/install/), with the toolchain pinned in [`lean-toolchain`](lean-toolchain)) and Python 3.13+ with [`uv`](https://docs.astral.sh/uv/). @@ -30,19 +65,20 @@ cd python && uv sync # Python tooling only; add `--group test` for pytest lake exe cache get # prebuilt Mathlib oleans (fast) lake build LeanPool.YourProject # builds only your project — minutes, not hours # or: make build-project P=YourProject +lake build Challenge # the whole challenge board — seconds ``` The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style LeanPool`, the quality checker) do need the full pool built, but CI runs them on your PR — you don't have to reproduce them locally. ## Pull requests -- **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool.lean`, `LeanPool/**/*.lean`, and `LeanPool/projects.yml`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. This is enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml). +- **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool.lean`, `LeanPool/**/*.lean`, `LeanPool/projects.yml`, `Challenge.lean`, `Challenge/**/*.lean`, `Challenge/challenges.yml`, `Solution.lean`, and `Solution/**/*.lean`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. The same guard rejects a PR that edits a challenge statement alongside a solution. Both are enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml). - **Never change the checks or gates.** Do not modify `.github/workflows/`, `.github/CODE_QUALITY.md`, `python/lean_pool/quality.py`, `scripts/nolints-style.txt`, the `[leanOptions]`/lint settings in `lakefile.toml`, or any other CI step or linter config — and do not add a waiver of any kind (a `size-limit-ok` comment, a `nolints-style.txt` entry, `set_option linter.X false`, etc.) — unless explicitly asked. If a check fails, fix the code, not the check. This applies to everyone, and especially to AI agents. - **Branches.** `yourname/description` for solo work; `feature/`/`fix/` prefixes when shared. Open PRs early (draft + `WIP` is fine) and use `Closes #123` to link issues. ## Linting and testing -**Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `lake exe runLinter LeanPool`, `lake exe lint-style LeanPool`, and the quality checker (see [`lean_action_ci.yml`](.github/workflows/lean_action_ci.yml)). Conventions live in [`.github/CODE_QUALITY.md`](.github/CODE_QUALITY.md). +**Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `scripts/ci/build-challenges.sh` (the `Challenge`/`Solution` build, where only the expected `sorry` notices are tolerated), `lake exe runLinter` and `lake exe lint-style` on all three libraries, the quality checker (see [`lean_action_ci.yml`](.github/workflows/lean_action_ci.yml)), and comparator on every solved challenge (see [`challenge-verify.yml`](.github/workflows/challenge-verify.yml)). Conventions live in [`.github/CODE_QUALITY.md`](.github/CODE_QUALITY.md). **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`. diff --git a/Challenge.lean b/Challenge.lean new file mode 100644 index 0000000000..8b13789179 --- /dev/null +++ b/Challenge.lean @@ -0,0 +1 @@ + diff --git a/Challenge/README.md b/Challenge/README.md new file mode 100644 index 0000000000..1025a8f457 --- /dev/null +++ b/Challenge/README.md @@ -0,0 +1,18 @@ +# Challenges + +Open *statements* — theorems written in Mathlib vocabulary and left as `sorry` — that +Lean Pool is asking someone to prove. One module per challenge, each registered in +[`challenges.yml`](challenges.yml) alongside the English statement it is supposed to say. + +This is the only place in the repository where `sorry` is allowed, and only as the whole +proof body of a declaration the registry lists. Everything else in a statement file must be +closed, and imports must come from `Mathlib.*` so that reading a challenge never means +auditing pool code. Browse the board with `make challenges`. + +A statement never changes once merged: it is the text every solution is judged against. +Answers go in [`../Solution/`](../Solution) and are checked by +[`leanprover/comparator`](https://github.com/leanprover/comparator). + +See [Challenge mode](../CONTRIBUTING.md#challenge-mode) for how to propose one, and +[`../.github/CHALLENGE_REVIEW_RULES.md`](../.github/CHALLENGE_REVIEW_RULES.md) for what the +review asks of it. diff --git a/Makefile b/Makefile index 8aebb6d158..a4afb920e7 100644 --- a/Makefile +++ b/Makefile @@ -1,8 +1,17 @@ -.PHONY: build build-project setup lint lint-fix check test docs update agent-docs +.PHONY: build build-project build-challenges setup lint lint-fix check test docs \ + update agent-docs challenges comparator verify-challenge + +# Where `make comparator` keeps its checkouts. +COMPARATOR_CACHE ?= $(HOME)/.cache/lean-pool # Build the Lean project. build: lake build LeanPool + lake build Challenge Solution + +# Build only the challenge board and its solutions (seconds, not hours). +build-challenges: + lake build Challenge Solution # Build a single project against the Mathlib cache, e.g. # `make build-project P=Rupert`. Projects are independent, so this needs @@ -21,6 +30,8 @@ setup: # Run all CI-equivalent linters (Lean and Python). lint: lake exe runLinter LeanPool + lake exe runLinter Challenge + lake exe runLinter Solution cd python && uv run ruff check cd python && uv run ruff format --check @@ -41,6 +52,36 @@ test: docs: cd docbuild && lake build LeanPool:docs +# List the registered challenges (open statements awaiting a proof). +challenges: + cd python && uv run python -m lean_pool.challenge --repo .. list + +# Fetch and build the third-party judge used to verify challenge solutions: +# leanprover/comparator, plus a lean4export built at this project's toolchain +# (comparator pins its own, newer one, which cannot read our oleans). +comparator: + @mkdir -p $(COMPARATOR_CACHE) + @test -d $(COMPARATOR_CACHE)/comparator || \ + git clone https://github.com/leanprover/comparator $(COMPARATOR_CACHE)/comparator + cd $(COMPARATOR_CACHE)/comparator && git pull --ff-only && lake build comparator + @test -d $(COMPARATOR_CACHE)/lean4export || \ + git clone https://github.com/leanprover/lean4export $(COMPARATOR_CACHE)/lean4export + cd $(COMPARATOR_CACHE)/lean4export && git pull --ff-only + cp lean-toolchain $(COMPARATOR_CACHE)/lean4export/lean-toolchain + cd $(COMPARATOR_CACHE)/lean4export && lake build lean4export + @echo + @echo "comparator: $(COMPARATOR_CACHE)/comparator/.lake/build/bin/comparator" + @echo "lean4export: $(COMPARATOR_CACHE)/lean4export/.lake/build/bin/lean4export" + @echo "Export COMPARATOR_LEAN4EXPORT to the latter, or pass --lean4export." + +# Verify a solution against its challenge statement with comparator, e.g. +# `make verify-challenge C=two-plus-two`. SOLUTION defaults to the module the +# registry records; pass it to check one that is not registered yet. +verify-challenge: + @test -n "$(C)" || \ + { echo "usage: make verify-challenge C= [SOLUTION=]"; exit 1; } + scripts/challenge/verify-solution.sh $(C) $(SOLUTION) + # Update Lean and Python dependencies. Refreshes lake-manifest.json, # pulls the matching Mathlib oleans cache, and re-syncs the Python # environment with all dependency groups. diff --git a/README.md b/README.md index 65d3f790ee..94bbea2e1a 100644 --- a/README.md +++ b/README.md @@ -31,6 +31,21 @@ make setup # pull Mathlib oleans, build the whole pool (~1.5h), install Pytho To work on a single project you don't need the whole pool built — see the [fast per-project build](CONTRIBUTING.md#dev-setup) in `CONTRIBUTING.md`. +### Challenge mode + +[`Challenge/`](Challenge/) is the other half of the pool: open *statements* rather than finished proofs. A challenge is a theorem written in Mathlib vocabulary and left as `sorry`, registered in [`Challenge/challenges.yml`](Challenge/challenges.yml) alongside the English statement it is supposed to say. It is the only place `sorry` is allowed, and only for the declarations the registry lists — everything else in the file must be closed, and every other gate still applies. + +Anyone can propose one. The [LLM reviewer](.github/CHALLENGE_REVIEW_RULES.md) judges a challenge on different grounds than a project: whether the problem is significant, whether the Lean faithfully says what the prose says, whether a cited known result is stated the way its source states it, whether the statement is vacuous or gameable, and how many lines of Lean a solution would take. + +Anyone can answer one, too. A solution lands in [`Solution/`](Solution/), restating the statement and proving it, and [`leanprover/comparator`](https://github.com/leanprover/comparator) settles whether it counts: [CI](.github/workflows/challenge-verify.yml) exports the challenge and solution environments separately, checks that the statements agree, and replays the proof through the Lean kernel with no axiom beyond `propext`/`Quot.sound`/`Classical.choice`. Because a kernel decides correctness, the [solution review](.github/SOLUTION_REVIEW_RULES.md) is short — and is skipped entirely when the PR adds nothing but the answer. + +```bash +make challenges # what's on the board +make verify-challenge C= # replay a solution locally +``` + +See [Challenge mode](CONTRIBUTING.md#challenge-mode) in `CONTRIBUTING.md`. + ### Contributing See [`CONTRIBUTING.md`](CONTRIBUTING.md). diff --git a/Solution.lean b/Solution.lean new file mode 100644 index 0000000000..8b13789179 --- /dev/null +++ b/Solution.lean @@ -0,0 +1 @@ + diff --git a/Solution/README.md b/Solution/README.md new file mode 100644 index 0000000000..f0e1b49156 --- /dev/null +++ b/Solution/README.md @@ -0,0 +1,17 @@ +# Solutions + +Answers to the challenges in [`../Challenge/`](../Challenge) live here, one module per +solved challenge, named after the challenge it answers. + +A solution **restates** its challenge's statement under the same fully qualified name and +proves it. It must *not* import the challenge module: +[`leanprover/comparator`](https://github.com/leanprover/comparator) exports the two +environments separately and checks that the statements agree, which is what makes the +verdict independent of the statement file. A gate enforces this, and +[`challenge-verify.yml`](../.github/workflows/challenge-verify.yml) runs comparator over +every solved challenge on every relevant push. + +A solution that needs real work should prove it in a pooled project under +[`../LeanPool/`](../LeanPool) and leave a thin bridge module here. + +See [Solving a challenge](../CONTRIBUTING.md#solving-a-challenge). diff --git a/lakefile.toml b/lakefile.toml index 471a19d5bf..e0549c2ad9 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,7 +1,7 @@ name = "lean-pool" version = "0.1.0" keywords = ["math"] -defaultTargets = ["LeanPool"] +defaultTargets = ["LeanPool", "Challenge", "Solution"] [leanOptions] pp.unicode.fun = true # pretty-prints `fun a ↦ b` @@ -16,3 +16,16 @@ rev = "v4.32.0-rc1" [[lean_lib]] name = "LeanPool" + +# Challenge mode: open statements awaiting a proof. This is the only library +# where `sorry` is allowed, and only as the whole proof body of a declaration +# registered in `Challenge/challenges.yml`. See CONTRIBUTING.md#challenge-mode. +[[lean_lib]] +name = "Challenge" + +# Answers to challenges. A solution restates its challenge's statement under the +# same name and proves it, WITHOUT importing the challenge module: comparator +# exports the two environments separately and compares them, which is what makes +# the check independent of the statement file. +[[lean_lib]] +name = "Solution" diff --git a/python/lean_pool/challenge.py b/python/lean_pool/challenge.py new file mode 100644 index 0000000000..4b0f5ef06e --- /dev/null +++ b/python/lean_pool/challenge.py @@ -0,0 +1,780 @@ +"""Challenge mode: the registry, cards, and comparator configuration. + +Lean Pool's ``Challenge/`` library holds *open* statements — theorems (and +occasionally definitions) written in Mathlib vocabulary and left as +``sorry``. It is the only place in the repository where ``sorry`` is +allowed, and only as the whole proof body of a declaration registered in +``Challenge/challenges.yml``. Everything else about a challenge file is +held to the same standard as pooled content: file header, narrow imports, +no ``set_option``, no axioms, size limits. + +This module owns the challenge *domain*: + +- the registry schema and its validation (:func:`registry_errors`), +- the generated challenge card shown on the docs site + (:func:`challenge_card`), +- the JSON configuration consumed by `leanprover/comparator + `_, the third-party judge that + decides whether a claimed solution really proves the challenge statement + (:func:`comparator_configuration`). + +The deterministic gates that *enforce* all of this live in +``lean_pool.quality``, which imports this module; nothing here imports +``lean_pool.quality``. + +Run: + uv run python -m lean_pool.challenge list + uv run python -m lean_pool.challenge config --solution-module +""" + +from __future__ import annotations + +import argparse +import json +import sys +import textwrap +from pathlib import Path +from typing import Any + +import yaml + +# The library (and directory) holding open statements. +LIBRARY_NAME = "Challenge" +# The library holding answers. A solution restates its challenge's statement +# under the same name and proves it, and deliberately does NOT import the +# challenge module: comparator exports the two environments separately and +# compares them, which is what makes the verdict independent of the +# statement file. +SOLUTION_LIBRARY_NAME = "Solution" +REGISTRY_RELATIVE_PATH = f"{LIBRARY_NAME}/challenges.yml" +# Axioms a challenge solution may depend on. Passed verbatim to comparator +# as `permitted_axioms`; `lean_pool.quality.ALLOWED_AXIOMS` is derived from +# this tuple so the pool gate and the external judge cannot drift apart. +PERMITTED_AXIOMS: tuple[str, ...] = ("propext", "Quot.sound", "Classical.choice") +# `open` — nobody has proved it yet. `solved` — a solution exists and the +# `solution` block records where; the statement itself keeps its `sorry`, +# because it is the trusted text every solution is compared against. +STATUS_VALUES = ("open", "solved") +REQUIRED_FIELDS = ( + "slug", + "title", + "summary", + "branch", + "entry_module", + "proposers", + "source", + "license", + "provenance", + "status", + "statements", + "tags", + "msc", +) +LICENSE_VALUES = ("Apache-2.0", "MIT") +# Who wrote the Lean statement, mirroring `projects.yml`. +PROVENANCE_VALUES = ("human", "AI", "mix") +SOURCE_KEY_ORDER = ("arxiv", "doi", "url") +# Mathlib's style linter caps lines at 100 columns and the card is checked +# byte-for-byte, so wrapping has to be deterministic. +CARD_WIDTH = 100 + + +def registry_path(root: Path) -> Path: + """Return the path of the challenge registry inside ``root``.""" + return root / REGISTRY_RELATIVE_PATH + + +def challenge_files(root: Path) -> list[Path]: + """Return every Lean file of the challenge library, index file first.""" + files = [root / f"{LIBRARY_NAME}.lean"] + files.extend(sorted((root / LIBRARY_NAME).rglob("*.lean"))) + return [path for path in files if path.exists()] + + +def statement_files(root: Path) -> list[Path]: + """Return the challenge statement files (every file but the index).""" + index = root / f"{LIBRARY_NAME}.lean" + return [path for path in challenge_files(root) if path != index] + + +def solution_files(root: Path) -> list[Path]: + """Return every Lean file of the solution library, index file first.""" + files = [root / f"{SOLUTION_LIBRARY_NAME}.lean"] + files.extend(sorted((root / SOLUTION_LIBRARY_NAME).rglob("*.lean"))) + return [path for path in files if path.exists()] + + +def solution_proof_files(root: Path) -> list[Path]: + """Return the solution files (every file but the generated index).""" + index = root / f"{SOLUTION_LIBRARY_NAME}.lean" + return [path for path in solution_files(root) if path != index] + + +def solution_module(challenge: dict[str, Any]) -> str | None: + """Return the in-repo module proving a challenge, if it has one.""" + solution = challenge.get("solution") + if not isinstance(solution, dict): + return None + module = solution.get("module") + return module if isinstance(module, str) and module.strip() else None + + +def is_solved(challenge: dict[str, Any]) -> bool: + """Whether the registry records this challenge as solved.""" + return challenge.get("status") == "solved" + + +def load_challenges(root: Path) -> tuple[list[Any], list[tuple[Path, str]]]: + """Load the challenge registry. + + Args: + root: Repository root. + + Returns: + ``(challenges, errors)``. ``challenges`` is the raw ``challenges`` + list — entries are validated separately by :func:`registry_errors` + — and is empty whenever ``errors`` is non-empty. + """ + path = registry_path(root) + if not path.exists(): + return [], [(path, f"missing {REGISTRY_RELATIVE_PATH}")] + try: + data = yaml.safe_load(path.read_text()) or {} + except yaml.YAMLError as error: + return [], [(path, f"invalid YAML: {error}")] + if not isinstance(data, dict): + return [], [(path, f"{REGISTRY_RELATIVE_PATH} must contain a mapping")] + challenges = data.get("challenges", []) + if not isinstance(challenges, list): + return [], [(path, "`challenges` must be a list")] + return challenges, [] + + +def find_challenge(root: Path, slug: str) -> dict[str, Any] | None: + """Return the registered challenge with ``slug``, or ``None``.""" + challenges, _ = load_challenges(root) + for challenge in challenges: + if isinstance(challenge, dict) and challenge.get("slug") == slug: + return challenge + return None + + +def open_declarations(challenge: dict[str, Any]) -> list[dict[str, Any]]: + """Return the declarations a challenge leaves open, statements first. + + These are exactly the declarations allowed to be ``sorry`` — the + theorems under ``statements`` plus any definition holes under + ``definitions``. + """ + entries = [] + for key in ("statements", "definitions"): + value = challenge.get(key) + if isinstance(value, list): + entries.extend(item for item in value if isinstance(item, dict)) + return entries + + +def open_declaration_names(challenge: dict[str, Any]) -> list[str]: + """Return the names of every declaration a challenge leaves open.""" + return [ + entry["declaration"] + for entry in open_declarations(challenge) + if isinstance(entry.get("declaration"), str) + ] + + +def statement_names(challenge: dict[str, Any]) -> list[str]: + """Return the theorem names a solution has to prove.""" + statements = challenge.get("statements") + if not isinstance(statements, list): + return [] + return [ + item["declaration"] + for item in statements + if isinstance(item, dict) and isinstance(item.get("declaration"), str) + ] + + +def definition_names(challenge: dict[str, Any]) -> list[str]: + """Return the definition holes a solution has to fill in.""" + definitions = challenge.get("definitions") + if not isinstance(definitions, list): + return [] + return [ + item["declaration"] + for item in definitions + if isinstance(item, dict) and isinstance(item.get("declaration"), str) + ] + + +def comparator_configuration( + challenge: dict[str, Any], + solution_module: str, + *, + enable_nanoda: bool = False, +) -> dict[str, Any]: + """Build the JSON configuration `comparator`_ consumes. + + Comparator replays the solution environment through the Lean kernel and + checks that each listed theorem proves *the same statement* as the + challenge module, using no axiom outside ``permitted_axioms``. Passing + it is what turns "someone says they solved it" into a verified claim. + + Args: + challenge: A registry entry. + solution_module: Module name of the claimed solution, resolvable in + the Lake workspace comparator runs in. + enable_nanoda: Also replay through the external ``nanoda`` kernel. + Requires the ``nanoda_bin`` binary; off by default. + + Returns: + The configuration mapping, ready to be serialized to JSON. + + .. _comparator: https://github.com/leanprover/comparator + """ + configuration: dict[str, Any] = { + "challenge_module": challenge["entry_module"], + "solution_module": solution_module, + "theorem_names": statement_names(challenge), + "permitted_axioms": list(PERMITTED_AXIOMS), + "enable_nanoda": enable_nanoda, + } + holes = definition_names(challenge) + if holes: + # Definition holes are gameable by construction — comparator only + # checks that name, type, universes and safety level match — so a + # challenge that declares them needs human review of the solution + # too. See the "Definition Holes" section of comparator's README. + configuration["definition_names"] = holes + return configuration + + +def _format_source(source: Any) -> str: + """Render the source anchor the way project cards render theirs.""" + if isinstance(source, str): + return source + if not isinstance(source, dict): + return "" + return ", ".join( + f"{key}:{source[key]}" for key in SOURCE_KEY_ORDER if key in source + ) + + +def _format_solution(solution: Any) -> str: + """Render the `solution` block as one line of card text.""" + if not isinstance(solution, dict): + return str(solution) + parts = [] + if isinstance(solution.get("module"), str): + parts.append(f"`{solution['module']}`") + if isinstance(solution.get("project"), str): + parts.append(f"pool project `{solution['project']}`") + if isinstance(solution.get("url"), str): + parts.append(solution["url"]) + if isinstance(solution.get("authors"), list): + parts.append(f"by {', '.join(str(a) for a in solution['authors'])}") + if isinstance(solution.get("verified"), str): + parts.append(f"verified {solution['verified']}") + return ", ".join(parts) + + +def _wrap(text: str, *, indent: str = " ") -> list[str]: + """Wrap one card line to the style linter's column limit. + + Field lines indent their continuations two spaces so the label stays + readable; prose paragraphs pass ``indent=""``. Long unbreakable tokens + (URLs, qualified declaration names) are left intact rather than split, + matching how the style linter exempts bare URLs. + """ + wrapped = textwrap.wrap( + text, + width=CARD_WIDTH, + subsequent_indent=indent, + break_long_words=False, + break_on_hyphens=False, + ) + return wrapped or [text] + + +def _join(values: Any) -> str: + """Join a list field for display, tolerating a bare string.""" + if isinstance(values, list): + return ", ".join(str(value) for value in values) + return str(values) + + +def challenge_card(challenge: dict[str, Any]) -> str: + """Render the module docstring shown at the top of a challenge file. + + The card is the human-readable half of a challenge: it carries the + informal statement that the Lean is supposed to say, so a reader (and + the LLM reviewer) can judge faithfulness without leaving the file. + ``lean_pool.quality`` regenerates and gates it, so the format has to be + deterministic. + """ + lines = [f"# {challenge['title']}", ""] + fields = [ + ("Source", _format_source(challenge["source"])), + ("Proposed by", _join(challenge["proposers"])), + ("Status", str(challenge["status"])), + ("Open declarations", _join_declarations(challenge)), + ("Tags", _join(challenge["tags"])), + ("MSC", _join(challenge["msc"])), + ] + if challenge.get("estimated_lines") is not None: + estimated = challenge["estimated_lines"] + unit = "line" if estimated == 1 else "lines" + fields.append(("Estimated size", f"~{estimated} {unit} of Lean")) + if challenge.get("solution") is not None: + fields.append(("Solution", _format_solution(challenge["solution"]))) + for label, value in fields: + lines.extend(_wrap(f"{label}: {value}")) + lines.extend(["", "Informal statement:"]) + for entry in open_declarations(challenge): + lines.extend(_wrap(f"* `{entry['declaration']}` — {entry['informal']}")) + return "/-!\n" + "\n".join(lines) + "\n-/" + + +def _join_declarations(challenge: dict[str, Any]) -> str: + """Render the open declaration names as backticked card text.""" + return ", ".join(f"`{name}`" for name in open_declaration_names(challenge)) + + +def solution_card(challenge: dict[str, Any]) -> str: + """Render the module docstring for a challenge's solution file. + + The card exists to say what the file is for a reader who lands on it: + a restatement of somebody else's trusted text, proved. It also records + the verification date, so a stale claim is visible in the source. + """ + solution = challenge.get("solution") or {} + lines = [f"# Solution: {challenge['title']}", ""] + fields = [ + ("Challenge", f"`{challenge['slug']}` (`{challenge['entry_module']}`)"), + ("Proves", _join_declarations(challenge)), + ] + if isinstance(solution.get("authors"), list): + fields.append(("Solved by", _join(solution["authors"]))) + if isinstance(solution.get("project"), str): + fields.append(("Pool project", f"`{solution['project']}`")) + if isinstance(solution.get("verified"), str): + fields.append(("Verified with comparator", solution["verified"])) + for label, value in fields: + lines.extend(_wrap(f"{label}: {value}")) + lines.extend( + [ + "", + *_wrap( + "This module restates the challenge statement under its own name and " + "proves it. It must not import the challenge module: comparator " + "exports both environments separately and checks that the statements " + "agree, which is what makes the verdict independent of the statement " + "file.", + indent="", + ), + ] + ) + return "/-!\n" + "\n".join(lines) + "\n-/" + + +def registry_errors(root: Path) -> list[tuple[Path, str]]: + """Validate the challenge registry against the schema. + + Returns: + ``(path, message)`` pairs, empty when the registry is valid. The + caller turns these into whatever error type it reports. + """ + challenges, errors = load_challenges(root) + if errors: + return errors + path = registry_path(root) + errors = _uniqueness_errors(path, challenges) + errors.extend(_registration_errors(root, path, challenges)) + if errors: + return errors + for index, challenge in enumerate(challenges, start=1): + errors.extend(_challenge_errors(root, path, index, challenge)) + return errors + + +def _uniqueness_errors(path: Path, challenges: list[Any]) -> list[tuple[Path, str]]: + """Reject duplicate slugs, entry modules, or open declarations.""" + errors: list[tuple[Path, str]] = [] + for field in ("slug", "entry_module"): + seen: dict[str, int] = {} + for index, challenge in enumerate(challenges, start=1): + if not isinstance(challenge, dict): + continue + value = challenge.get(field) + if not isinstance(value, str): + continue + if value in seen: + errors.append( + ( + path, + f"duplicate `{field}` {value!r} in challenges " + f"#{seen[value]} and #{index}", + ) + ) + else: + seen[value] = index + declarations: dict[str, int] = {} + for index, challenge in enumerate(challenges, start=1): + if not isinstance(challenge, dict): + continue + for name in open_declaration_names(challenge): + if name in declarations: + errors.append( + ( + path, + f"duplicate open declaration {name!r} in challenges " + f"#{declarations[name]} and #{index}", + ) + ) + else: + declarations[name] = index + return errors + + +def _registration_errors( + root: Path, path: Path, challenges: list[Any] +) -> list[tuple[Path, str]]: + """Require every statement and solution file to be registered.""" + registered = { + challenge["entry_module"] + for challenge in challenges + if isinstance(challenge, dict) + and isinstance(challenge.get("entry_module"), str) + } + solutions = { + module + for challenge in challenges + if isinstance(challenge, dict) + and (module := solution_module(challenge)) is not None + } + errors: list[tuple[Path, str]] = [] + for file in solution_proof_files(root): + module = ".".join(file.relative_to(root).with_suffix("").parts) + if module not in solutions: + errors.append( + ( + path, + f"solution module {module} is not the recorded solution of any " + f"challenge in {REGISTRY_RELATIVE_PATH}", + ) + ) + for file in statement_files(root): + module = ".".join(file.relative_to(root).with_suffix("").parts) + if module not in registered: + errors.append( + ( + path, + f"challenge module {module} missing from {REGISTRY_RELATIVE_PATH}", + ) + ) + return errors + + +def _challenge_errors( + root: Path, path: Path, index: int, challenge: Any +) -> list[tuple[Path, str]]: + """Validate one registry entry.""" + if not isinstance(challenge, dict): + return [(path, f"challenge #{index} must be a mapping")] + missing = sorted(set(REQUIRED_FIELDS) - set(challenge)) + if missing: + return [(path, f"challenge #{index} missing fields: {', '.join(missing)}")] + errors = _value_errors(path, index, challenge) + module_path = _module_path(root, str(challenge["entry_module"])) + if not module_path.exists(): + errors.append((path, f"challenge #{index} entry_module does not exist")) + errors.extend(_declaration_errors(path, index, challenge)) + errors.extend(_solution_errors(path, index, challenge)) + return errors + + +def _value_errors( + path: Path, index: int, challenge: dict[str, Any] +) -> list[tuple[Path, str]]: + """Check the scalar and list-valued fields of one entry.""" + errors: list[tuple[Path, str]] = [] + if challenge["status"] not in STATUS_VALUES: + errors.append( + ( + path, + f"challenge #{index} has invalid status " + f"(expected one of {', '.join(STATUS_VALUES)})", + ) + ) + if challenge["license"] not in LICENSE_VALUES: + errors.append( + ( + path, + f"challenge #{index} has invalid license " + f"(expected one of {', '.join(LICENSE_VALUES)})", + ) + ) + if challenge["provenance"] not in PROVENANCE_VALUES: + errors.append( + ( + path, + f"challenge #{index} has invalid provenance " + f"(expected one of {', '.join(PROVENANCE_VALUES)})", + ) + ) + if not _source_is_valid(challenge["source"]): + errors.append( + ( + path, + f"challenge #{index} source needs at least one of " + f"{', '.join(SOURCE_KEY_ORDER)}", + ) + ) + for field in ("slug", "title", "summary", "branch", "entry_module"): + if not _nonempty_string(challenge[field]): + errors.append( + (path, f"challenge #{index} {field} must be a nonempty string") + ) + for field in ("proposers", "tags", "msc"): + if not _string_list(challenge[field]): + errors.append( + (path, f"challenge #{index} {field} must be nonempty strings") + ) + estimated = challenge.get("estimated_lines") + if estimated is not None and not (isinstance(estimated, int) and estimated > 0): + errors.append( + (path, f"challenge #{index} estimated_lines must be a positive integer") + ) + return errors + + +def _declaration_errors( + path: Path, index: int, challenge: dict[str, Any] +) -> list[tuple[Path, str]]: + """Check `statements` / `definitions` shape and namespacing.""" + errors: list[tuple[Path, str]] = [] + statements = challenge["statements"] + if not isinstance(statements, list) or not statements: + errors.append((path, f"challenge #{index} statements must be a nonempty list")) + return errors + definitions = challenge.get("definitions", []) + if not isinstance(definitions, list): + errors.append((path, f"challenge #{index} definitions must be a list")) + return errors + module = str(challenge["entry_module"]) + for entry in [*statements, *definitions]: + if not isinstance(entry, dict): + errors.append( + (path, f"challenge #{index} declaration entries must be mappings") + ) + continue + if not _nonempty_string(entry.get("declaration")): + errors.append( + (path, f"challenge #{index} declaration names must be nonempty strings") + ) + continue + if not _nonempty_string(entry.get("informal")): + errors.append( + ( + path, + f"challenge #{index} declaration {entry['declaration']} needs a " + "nonempty `informal` statement — it is what the Lean is judged " + "against", + ) + ) + if not entry["declaration"].startswith(f"{module}."): + errors.append( + ( + path, + f"challenge #{index} declaration {entry['declaration']} must live " + f"in the {module} namespace", + ) + ) + return errors + + +def _solution_errors( + path: Path, index: int, challenge: dict[str, Any] +) -> list[tuple[Path, str]]: + """Keep `status` and the `solution` block consistent.""" + solution = challenge.get("solution") + if challenge["status"] == "solved": + if not isinstance(solution, dict): + return [ + ( + path, + f"challenge #{index} is solved but has no `solution` mapping " + "recording where the proof lives", + ) + ] + if not any( + _nonempty_string(solution.get(key)) for key in ("module", "project", "url") + ): + return [ + ( + path, + f"challenge #{index} solution needs a `module` (in this " + "repository), a `project` slug, or a `url`", + ) + ] + module = solution.get("module") + if module is not None and not str(module).startswith( + f"{SOLUTION_LIBRARY_NAME}." + ): + return [ + ( + path, + f"challenge #{index} solution module {module} must live in the " + f"{SOLUTION_LIBRARY_NAME} library", + ) + ] + return [] + if solution is not None: + return [ + ( + path, + f"challenge #{index} is open but carries a `solution` block; set " + "status to solved", + ) + ] + return [] + + +def _module_path(root: Path, module: str) -> Path: + """Return the file backing a Lean module name.""" + return root.joinpath(*module.split(".")).with_suffix(".lean") + + +def _source_is_valid(source: Any) -> bool: + """Whether the source anchor names a paper, DOI, or URL.""" + if isinstance(source, str): + return any(source.startswith(f"{key}:") for key in SOURCE_KEY_ORDER) + if isinstance(source, dict): + return bool(set(SOURCE_KEY_ORDER) & set(source)) + return False + + +def _nonempty_string(value: Any) -> bool: + """Whether ``value`` is a string with non-whitespace content.""" + return isinstance(value, str) and bool(value.strip()) + + +def _string_list(value: Any) -> bool: + """Whether ``value`` is a nonempty list of nonempty strings.""" + return ( + isinstance(value, list) + and bool(value) + and all(isinstance(item, str) and item for item in value) + ) + + +def _render_listing(challenges: list[Any]) -> str: + """Render the `list` subcommand's human-readable output.""" + if not challenges: + return "No challenges registered." + rows = [] + for challenge in challenges: + if not isinstance(challenge, dict): + continue + names = ", ".join(open_declaration_names(challenge)) + row = ( + f"{challenge.get('slug', '?')} [{challenge.get('status', '?')}] " + f"{challenge.get('title', '?')}\n {challenge.get('entry_module', '?')}" + f" — {names}" + ) + module = solution_module(challenge) + if module is not None: + row += f"\n solved by {module}" + rows.append(row) + return "\n".join(rows) + + +def _parse_args(argv: list[str]) -> argparse.Namespace: + """Parse the challenge CLI arguments.""" + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--repo", + type=Path, + default=Path(__file__).resolve().parents[2], + help="Repository root. Defaults to the checkout containing this package.", + ) + subparsers = parser.add_subparsers(dest="command", required=True) + subparsers.add_parser("list", help="List registered challenges.") + subparsers.add_parser( + "solved", + help="Print the slug of every challenge with an in-repo solution, one " + "per line — the set CI hands to comparator.", + ) + configuration_parser = subparsers.add_parser( + "config", help="Emit a comparator JSON configuration for one challenge." + ) + configuration_parser.add_argument( + "slug", help="Challenge slug from Challenge/challenges.yml." + ) + configuration_parser.add_argument( + "--solution-module", + help="Module name of the claimed solution, as comparator will import it. " + "Defaults to the module recorded in the registry.", + ) + configuration_parser.add_argument( + "--out", type=Path, help="Write the configuration here instead of stdout." + ) + configuration_parser.add_argument( + "--enable-nanoda", + action="store_true", + help="Also replay the solution through the nanoda kernel.", + ) + return parser.parse_args(argv) + + +def main(argv: list[str] | None = None) -> int: + """Run the challenge CLI.""" + args = _parse_args(sys.argv[1:] if argv is None else argv) + root = args.repo.resolve() + if args.command in ("list", "solved"): + if not registry_path(root).exists(): + # An installed but empty board: nothing to list, nothing to + # verify. Only the quality gate treats a missing registry as an + # error, and only once a statement file exists. + if args.command == "list": + print("No challenges registered.") + return 0 + challenges, errors = load_challenges(root) + for path, message in errors: + print(f"{path}: {message}", file=sys.stderr) + if errors: + return 1 + if args.command == "solved": + for entry in challenges: + if isinstance(entry, dict) and solution_module(entry) is not None: + print(entry.get("slug", "")) + return 0 + print(_render_listing(challenges)) + return 0 + + challenge = find_challenge(root, args.slug) + if challenge is None: + print(f"Unknown challenge {args.slug!r}.", file=sys.stderr) + return 1 + module = args.solution_module or solution_module(challenge) + if module is None: + print( + f"Challenge {args.slug!r} records no solution module; pass " + "--solution-module.", + file=sys.stderr, + ) + return 1 + configuration = comparator_configuration( + challenge, module, enable_nanoda=args.enable_nanoda + ) + rendered = json.dumps(configuration, indent=4) + "\n" + if args.out is not None: + args.out.write_text(rendered) + print(f"Wrote {args.out}") + else: + print(rendered, end="") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index 6c1e4f5e22..11ece190c3 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -1,4 +1,17 @@ -"""Deterministic repository quality checks for Lean Pool.""" +"""Deterministic repository quality checks for Lean Pool. + +Two Lean libraries are checked, under almost the same rules: + +- ``LeanPool`` — completed formalizations. No ``sorry``, ever. +- ``Challenge`` — open statements awaiting a proof (see + :mod:`lean_pool.challenge`). ``sorry`` is allowed here and nowhere else, + and only as the whole proof body of a declaration registered in + ``Challenge/challenges.yml``. Every other rule (headers, narrow imports, + no ``set_option``, no axioms, size caps, the environment backdoor audit) + applies unchanged, and the Lean-backed audits additionally verify that + the registered open declarations are the *only* ones resting on + ``sorryAx``. +""" from __future__ import annotations @@ -13,7 +26,14 @@ import yaml -ALLOWED_AXIOMS = {"Classical.choice", "propext", "Quot.sound"} +from lean_pool import challenge + +# Derived from the challenge module so the pool gate and the axiom list +# handed to the external comparator judge cannot drift apart. +ALLOWED_AXIOMS = set(challenge.PERMITTED_AXIOMS) +# The `sorry` tactic/term compiles to this axiom. Permitted only for the +# declarations a challenge registers as open. +SORRY_AXIOM = "sorryAx" CODE_QUALITY_URL = ( "https://github.com/Vilin97/lean-pool/blob/main/.github/CODE_QUALITY.md" ) @@ -87,6 +107,17 @@ r"Authors: [^\n]+\n" r"-/\n" ) +# A `sorry` in a challenge file may only be the entire proof body — either +# `:= sorry` closing the declaration line, or a lone `sorry` on its own +# line after a `:=`. This rules out partially open proofs like +# `⟨sorry, trivial⟩` or `by simp [sorry]`, which would leave a challenge +# quietly easier than its statement suggests. +WHOLE_BODY_SORRY = re.compile(r"(?::=\s*sorry|^\s*sorry)\s*$") +# Challenge statements are read by every would-be solver and by the LLM +# reviewer judging faithfulness, so they stay small; a challenge needing +# more setup than this belongs in the pool as a project first. +CHALLENGE_CODE_LINE_LIMIT = 500 +POOL_CODE_LINE_LIMIT = 10000 @dataclass(frozen=True) @@ -184,6 +215,30 @@ def _lean_content_files(root: Path) -> list[Path]: return [path for path in files if path.exists()] +def _challenge_files(root: Path) -> list[Path]: + """Return every Lean file of the challenge library, index included.""" + return challenge.challenge_files(root) + + +def _solution_files(root: Path) -> list[Path]: + """Return every Lean file of the solution library, index included.""" + return challenge.solution_files(root) + + +def _all_lean_files(root: Path) -> list[Path]: + """Return the Lean files of all three libraries.""" + return [*_lean_content_files(root), *_challenge_files(root), *_solution_files(root)] + + +def _generated_index_files(root: Path) -> set[Path]: + """Return the `mk_all`-generated library index files.""" + return { + root / "LeanPool.lean", + root / f"{challenge.LIBRARY_NAME}.lean", + root / f"{challenge.SOLUTION_LIBRARY_NAME}.lean", + } + + def _module_to_path(root: Path, module: str) -> Path: return root.joinpath(*module.split(".")).with_suffix(".lean") @@ -201,6 +256,7 @@ def _parse_imports(text: str) -> list[str]: def _reachable_leanpool_files(root: Path, entry_module: str = "LeanPool") -> set[Path]: reachable: set[Path] = set() pending = [entry_module] + root_module = entry_module.split(".")[0] while pending: module = pending.pop() @@ -212,26 +268,41 @@ def _reachable_leanpool_files(root: Path, entry_module: str = "LeanPool") -> set pending.extend( imported for imported in _parse_imports(text) - if imported.startswith("LeanPool") + if imported.startswith(root_module) ) return reachable def _check_reachability(root: Path) -> list[_QualityError]: - expected = set(_lean_content_files(root)) - reachable = _reachable_leanpool_files(root) - missing = sorted(expected - reachable) + errors = _unreachable_errors(root, "LeanPool", _lean_content_files(root)) + errors.extend( + _unreachable_errors(root, challenge.LIBRARY_NAME, _challenge_files(root)) + ) + errors.extend( + _unreachable_errors( + root, challenge.SOLUTION_LIBRARY_NAME, _solution_files(root) + ) + ) + return errors + + +def _unreachable_errors( + root: Path, entry_module: str, expected: list[Path] +) -> list[_QualityError]: + """Report library files the generated index does not import.""" + reachable = _reachable_leanpool_files(root, entry_module) return [ - _QualityError(path, 1, "Lean file is not reachable from LeanPool.lean") - for path in missing + _QualityError(path, 1, f"Lean file is not reachable from {entry_module}.lean") + for path in sorted(set(expected) - reachable) ] def _check_headers(root: Path) -> list[_QualityError]: errors: list[_QualityError] = [] - for path in _lean_content_files(root): - if path == root / "LeanPool.lean": + generated = _generated_index_files(root) + for path in _all_lean_files(root): + if path in generated: continue text = path.read_text() if not HEADER_PATTERN.match(text): @@ -249,57 +320,98 @@ def _check_headers(root: Path) -> list[_QualityError]: def _check_forbidden_lean_text(root: Path) -> list[_QualityError]: + """Scan both libraries for forbidden tokens. + + Identical rules either side of the split, except that a challenge file + may use `sorry` — and only as a whole proof body, checked by + :func:`_sorry_errors`. + """ errors: list[_QualityError] = [] for path in _lean_content_files(root): - stripped = _strip_lean_comments(path.read_text()) - for line_number, line in enumerate(stripped.splitlines(), start=1): - if re.search(r"\bset_option\b", line): - errors.append( - _QualityError(path, line_number, "set_option is forbidden") - ) - if re.search(r"\bnolint\b", line): - errors.append( - _QualityError(path, line_number, "nolint waiver is forbidden") - ) - if FORBIDDEN_OPTION_APIS.search(line): - errors.append( - _QualityError( - path, - line_number, - "programmatic option manipulation is forbidden", - ) - ) - if FORBIDDEN_OPTION_NAMES.search(line): - errors.append( - _QualityError( - path, - line_number, - "gated option name in code is forbidden", - ) - ) - if re.match(r"^\s*(?:public\s+)?import\s+Mathlib\s*$", line): - errors.append( - _QualityError( - path, line_number, "broad import Mathlib is forbidden" - ) - ) - if re.search(r"\b(?:sorry|admit)\b", line): - errors.append( - _QualityError(path, line_number, "sorry/admit is forbidden") - ) - if FORBIDDEN_SOUNDNESS.search(line): - errors.append( - _QualityError( - path, line_number, "unchecked declaration is forbidden" - ) + errors.extend(_forbidden_text_errors(path, allow_sorry=False)) + for path in _challenge_files(root): + errors.extend(_forbidden_text_errors(path, allow_sorry=True)) + # A solution is a proof, so it is held to the pool's rules exactly. + for path in _solution_files(root): + errors.extend(_forbidden_text_errors(path, allow_sorry=False)) + return errors + + +def _forbidden_text_errors(path: Path, *, allow_sorry: bool) -> list[_QualityError]: + errors: list[_QualityError] = [] + stripped = _strip_lean_comments(path.read_text()) + for line_number, line in enumerate(stripped.splitlines(), start=1): + if re.search(r"\bset_option\b", line): + errors.append(_QualityError(path, line_number, "set_option is forbidden")) + if re.search(r"\bnolint\b", line): + errors.append( + _QualityError(path, line_number, "nolint waiver is forbidden") + ) + if FORBIDDEN_OPTION_APIS.search(line): + errors.append( + _QualityError( + path, + line_number, + "programmatic option manipulation is forbidden", ) - if FORBIDDEN_DIAGNOSTICS.search(line): - errors.append( - _QualityError(path, line_number, "diagnostic command is forbidden") + ) + if FORBIDDEN_OPTION_NAMES.search(line): + errors.append( + _QualityError( + path, + line_number, + "gated option name in code is forbidden", ) + ) + if re.match(r"^\s*(?:public\s+)?import\s+Mathlib\s*$", line): + errors.append( + _QualityError(path, line_number, "broad import Mathlib is forbidden") + ) + errors.extend(_sorry_errors(path, line_number, line, allow_sorry=allow_sorry)) + if FORBIDDEN_SOUNDNESS.search(line): + errors.append( + _QualityError(path, line_number, "unchecked declaration is forbidden") + ) + if FORBIDDEN_DIAGNOSTICS.search(line): + errors.append( + _QualityError(path, line_number, "diagnostic command is forbidden") + ) return errors +def _sorry_errors( + path: Path, line_number: int, line: str, *, allow_sorry: bool +) -> list[_QualityError]: + """Apply the `sorry` rule for one comment-stripped line. + + `admit` is forbidden everywhere: challenge statements use one spelling + so the open declarations stay easy to eyeball. + """ + if re.search(r"\badmit\b", line): + return [_QualityError(path, line_number, "admit is forbidden")] + if not re.search(r"\bsorry\b", line): + return [] + if not allow_sorry: + return [ + _QualityError( + path, + line_number, + "sorry is forbidden outside " + f"{challenge.LIBRARY_NAME}/ (see CONTRIBUTING.md#challenge-mode)", + ) + ] + if not WHOLE_BODY_SORRY.search(line): + return [ + _QualityError( + path, + line_number, + "sorry must be the whole proof body of an open declaration " + "(`:= sorry`), not part of a larger term", + ) + ] + return [] + + def _check_lake_options(root: Path) -> list[_QualityError]: errors: list[_QualityError] = [] forbidden_patterns = { @@ -350,13 +462,22 @@ def _non_comment_code_lines(text: str) -> int: def _check_file_sizes(root: Path) -> list[_QualityError]: + errors = _file_size_errors(_lean_content_files(root), POOL_CODE_LINE_LIMIT) + errors.extend(_file_size_errors(_challenge_files(root), CHALLENGE_CODE_LINE_LIMIT)) + # A solution that needs more than this is really a pooled project; it + # should live in `LeanPool/` with a thin bridge module here. + errors.extend(_file_size_errors(_solution_files(root), CHALLENGE_CODE_LINE_LIMIT)) + return errors + + +def _file_size_errors(paths: list[Path], limit: int) -> list[_QualityError]: errors: list[_QualityError] = [] - for path in _lean_content_files(root): + for path in paths: code_lines = _non_comment_code_lines(path.read_text()) - if code_lines > 10000: + if code_lines > limit: errors.append( _QualityError( - path, 1, f"file has {code_lines} code lines; limit is 10000" + path, 1, f"file has {code_lines} code lines; limit is {limit}" ) ) return errors @@ -373,7 +494,7 @@ def _declaration_starts(stripped: str) -> list[tuple[int, str]]: def _check_proof_sizes(root: Path) -> list[_QualityError]: errors: list[_QualityError] = [] - for path in _lean_content_files(root): + for path in _all_lean_files(root): original_lines = path.read_text().splitlines() stripped = _strip_lean_comments("\n".join(original_lines)) starts = _declaration_starts(stripped) @@ -404,6 +525,12 @@ def _check_proof_sizes(root: Path) -> list[_QualityError]: def _parse_declarations(root: Path) -> list[_Declaration]: + return _declarations_in(_lean_content_files(root)) + + +def _declarations_in( + paths: list[Path], *, include_private: bool = False +) -> list[_Declaration]: declarations: list[_Declaration] = [] keyword_pattern = "|".join(DECLARATION_KEYWORDS) # Use a negative lookahead instead of `\b`: `\b` does not treat `'` as a @@ -413,7 +540,7 @@ def _parse_declarations(root: Path) -> list[_Declaration]: rf"^\s*{DECLARATION_PREFIX}({keyword_pattern})\s+" rf"({LEAN_IDENT})(?![\w'.])" ) - for path in _lean_content_files(root): + for path in paths: # Track `namespace` and `section` opens together so that an # `end
` pops the section rather than the enclosing namespace. # Each entry is (is_namespace, name); only namespace entries qualify a @@ -437,7 +564,7 @@ def _parse_declarations(root: Path) -> list[_Declaration]: scope_stack.pop() continue match = decl_pattern.match(line) - if match and _is_private_declaration_line(line): + if match and not include_private and _is_private_declaration_line(line): continue if match and not match.group(2).startswith(":"): namespace_stack = [ @@ -550,12 +677,12 @@ def gatedLiteral? (e : Expr) : Option String := | some (.lit (.strVal s)) => some s | _ => none -def auditEnv (env : Environment) : IO Unit := do +def auditEnv (env : Environment) (roots : List Name) : IO Unit := do let manipulators := manipulatorCandidates.filter env.contains let injectors := axiomInjectorCandidates.filter env.contains let mut visited : NameSet := NameSet.empty for (moduleName, data) in env.header.moduleNames.zip env.header.moduleData do - unless moduleName.getRoot == `LeanPool do continue + unless roots.contains moduleName.getRoot do continue for declName in data.constNames do unless visited.contains declName do visited := visited.insert declName @@ -590,22 +717,44 @@ def main (args : List String) : IO UInt32 := do Lean.initSearchPath (<- Lean.findSysroot) let imports := modules.toArray.map fun module => ({ module } : Lean.Import) let env <- Lean.importModules imports {} (trustLevel := 1024) - LeanPoolQuality.OptionAudit.auditEnv env + LeanPoolQuality.OptionAudit.auditEnv env (modules.map (·.getRoot)) return 0 """ +# Detail emitted by the audit when a declaration is a `sorry`. Tolerated +# for — and only for — the declarations a challenge registers as open. +_SORRY_INJECTOR_DETAIL = ( + f"references forbidden axiom-injecting constants: {SORRY_AXIOM}" +) def _check_option_backdoors(root: Path) -> list[_QualityError]: - """Audit every declaration compiled into the pool for backdoors.""" + """Audit every declaration compiled into the libraries for backdoors. + + Two passes, because a solution declares the same names as the challenge + it answers: importing `Challenge` and `Solution` into one environment is + a name clash by construction. + """ + pool_modules = ["LeanPool"] + if (root / f"{challenge.LIBRARY_NAME}.lean").exists(): + pool_modules.append(challenge.LIBRARY_NAME) + errors = _run_option_audit(root, pool_modules) + if (root / f"{challenge.SOLUTION_LIBRARY_NAME}.lean").exists(): + errors.extend(_run_option_audit(root, [challenge.SOLUTION_LIBRARY_NAME])) + return errors + + +def _run_option_audit(root: Path, modules: list[str]) -> list[_QualityError]: + """Run the environment audit over one set of importable modules.""" with tempfile.NamedTemporaryFile("w", suffix=".lean", delete=False) as temp_file: temp_path = Path(temp_file.name) temp_file.write(_OPTION_AUDIT_LEAN) temp_file.flush() + index_path = root / f"{modules[0]}.lean" try: try: process = subprocess.run( - ["lake", "env", "lean", "--run", str(temp_path)], + ["lake", "env", "lean", "--run", str(temp_path), *modules], cwd=root, check=False, capture_output=True, @@ -616,7 +765,7 @@ def _check_option_backdoors(root: Path) -> list[_QualityError]: # than crashing the whole quality run. return [ _QualityError( - root / "LeanPool.lean", + index_path, 1, "option-manipulation audit skipped: `lake` not found", ) @@ -624,28 +773,76 @@ def _check_option_backdoors(root: Path) -> list[_QualityError]: finally: temp_path.unlink(missing_ok=True) - return _parse_option_audit_output(root, process.stdout, process.stderr) + return _parse_option_audit_output( + root, + process.stdout, + process.stderr, + open_declarations=_open_declarations(root), + index_path=index_path, + ) + + +def _open_declarations(root: Path) -> set[str]: + """Return every declaration the challenge registry leaves open.""" + challenges, errors = challenge.load_challenges(root) + if errors: + return set() + return { + name + for entry in challenges + if isinstance(entry, dict) + for name in challenge.open_declaration_names(entry) + } + + +def _is_open_declaration(name: str, open_declarations: set[str]) -> bool: + """Whether ``name`` is a registered open declaration or its companion. + + Lean generates companions for a sorried declaration (`foo.eq_def`, + equation lemmas, hygienic auxiliaries); they carry the same `sorryAx` + reference and live under the same name prefix. + """ + return any( + name == declaration or name.startswith(f"{declaration}.") + for declaration in open_declarations + ) def _parse_option_audit_output( - root: Path, stdout: str, stderr: str + root: Path, + stdout: str, + stderr: str, + open_declarations: set[str] | None = None, + index_path: Path | None = None, ) -> list[_QualityError]: - """Turn environment-audit findings (and non-completion) into errors.""" + """Turn environment-audit findings (and non-completion) into errors. + + A finding that says nothing but "this declaration is a `sorry`" is + dropped for declarations the challenge registry lists as open — that is + the whole point of a challenge. Findings that combine `sorryAx` with + anything else still surface. + """ + permitted = open_declarations or set() errors: list[_QualityError] = [] for match in _OPTION_AUDIT_FINDING_RE.finditer(stdout): module, declaration, detail = match.groups() + detail = detail.strip() + if detail == _SORRY_INJECTOR_DETAIL and _is_open_declaration( + declaration, permitted + ): + continue errors.append( _QualityError( _module_to_path(root, module), 1, - f"{declaration} {detail.strip()}", + f"{declaration} {detail}", ) ) if _OPTION_AUDIT_COMPLETE_MARKER not in stdout: snippet = stderr.strip().splitlines() errors.append( _QualityError( - root / "LeanPool.lean", + index_path or root / "LeanPool.lean", 1, "option-manipulation audit did not complete: " f"{snippet[0] if snippet else '(no stderr)'}", @@ -655,11 +852,61 @@ def _parse_option_audit_output( def _check_axioms(root: Path) -> list[_QualityError]: - declarations = _parse_declarations(root) + """Audit pooled declarations: allowlisted axioms only, never `sorry`.""" + return _audit_axioms(root, _parse_declarations(root), "LeanPool", set()) + + +def _check_challenge_axioms(root: Path) -> list[_QualityError]: + """Audit the challenge library's declarations. + + A registered open declaration must actually rest on `sorryAx` — the + statement file is the trusted text every solution is compared against, + so it stays open and stable, and a solution lives elsewhere. Every + other declaration in the library (the definitions a statement is + phrased in terms of) must be closed, or the challenge would be resting + on unproved scaffolding nobody declared. + """ + files = challenge.statement_files(root) + if not files: + return [] + return _audit_axioms( + root, + _declarations_in(files), + challenge.LIBRARY_NAME, + _open_declarations(root), + ) + + +def _check_solution_axioms(root: Path) -> list[_QualityError]: + """Audit the solution library: real proofs, allowed axioms, no `sorry`. + + Run in its own Lean process, never alongside `Challenge`: a solution + declares the same names as the challenge it answers, so importing both + environments at once is a name clash by construction. + """ + files = challenge.solution_proof_files(root) + if not files: + return [] + return _audit_axioms( + root, + _declarations_in(files), + challenge.SOLUTION_LIBRARY_NAME, + set(), + ) + + +def _audit_axioms( + root: Path, + declarations: list[_Declaration], + import_module: str, + open_declarations: set[str], +) -> list[_QualityError]: + """Run `#print axioms` over ``declarations`` and grade the results.""" if not declarations: return [] - commands = "import LeanPool\n" + "\n".join( + index_path = root / f"{import_module}.lean" + commands = f"import {import_module}\n" + "\n".join( f"#print axioms _root_.{declaration.name}" for declaration in declarations ) with tempfile.NamedTemporaryFile("w", suffix=".lean", delete=False) as temp_file: @@ -681,7 +928,7 @@ def _check_axioms(root: Path) -> list[_QualityError]: # than crashing the whole quality run. return [ _QualityError( - root / "LeanPool.lean", + index_path, 1, "axiom audit skipped: `lake` not found", ) @@ -689,7 +936,7 @@ def _check_axioms(root: Path) -> list[_QualityError]: finally: temp_path.unlink(missing_ok=True) - errors = _parse_axiom_output(root, declarations, process.stdout) + errors = _parse_axiom_output(root, declarations, process.stdout, open_declarations) resolved = _axiom_audit_resolved(process.stdout) missing = [ declaration for declaration in declarations if declaration.name not in resolved @@ -700,7 +947,7 @@ def _check_axioms(root: Path) -> list[_QualityError]: if missing and not resolved and process.returncode != 0: return errors + [ _QualityError( - root / "LeanPool.lean", + index_path, 1, f"axiom audit failed before any declaration was checked: " f"{process.stderr.strip() or '(no stderr)'}", @@ -714,7 +961,9 @@ def _parse_axiom_output( root: Path, declarations: list[_Declaration], output: str, + open_declarations: set[str] | None = None, ) -> list[_QualityError]: + permitted = open_declarations or set() errors: list[_QualityError] = [] by_name = {declaration.name: declaration for declaration in declarations} by_name.update( @@ -722,20 +971,73 @@ def _parse_axiom_output( ) # Names may contain `'` (e.g. `foo'`); see _axiom_audit_resolved comment. pattern = re.compile(r"^'(.+?)' depends on axioms: \[(.*)\]$", re.MULTILINE) + seen: set[str] = set() for match in pattern.finditer(output): name = match.group(1) + if name not in by_name: + continue + declaration = by_name[name] + seen.add(declaration.name) axioms = {item.strip() for item in match.group(2).split(",") if item.strip()} - extra_axioms = sorted(axioms - ALLOWED_AXIOMS) - if extra_axioms and name in by_name: - declaration = by_name[name] - errors.append( - _QualityError( - declaration.path, - declaration.line, - f"{name} depends on unallowlisted axioms: " - f"{', '.join(extra_axioms)}", - ) + errors.extend( + _axiom_errors( + declaration, name, axioms, is_open=declaration.name in permitted ) + ) + # Only for declarations Lean actually resolved: an unresolved name is + # already reported once by `_axiom_audit_missing`. + resolved = _axiom_audit_resolved(output) + errors.extend( + _not_open_error(declaration) + for declaration in declarations + if declaration.name in permitted + and declaration.name not in seen + and declaration.name in resolved + ) + return errors + + +def _not_open_error(declaration: _Declaration) -> _QualityError: + """Report a registered challenge statement that is no longer open.""" + return _QualityError( + declaration.path, + declaration.line, + f"{declaration.name} is registered as an open challenge declaration " + f"but does not depend on `{SORRY_AXIOM}`; challenge statements keep " + "their `sorry` and solutions live outside the statement file", + ) + + +def _axiom_errors( + declaration: _Declaration, name: str, axioms: set[str], *, is_open: bool +) -> list[_QualityError]: + """Grade one declaration's axiom set.""" + allowed = ALLOWED_AXIOMS | ({SORRY_AXIOM} if is_open else set()) + extra_axioms = sorted(axioms - allowed) + errors: list[_QualityError] = [] + if is_open and SORRY_AXIOM not in axioms: + # Proved in place, using nothing worse than the allowed axioms — so + # the checks below are all happy, and the challenge has silently + # stopped being one. + errors.append(_not_open_error(declaration)) + if SORRY_AXIOM in extra_axioms: + extra_axioms.remove(SORRY_AXIOM) + errors.append( + _QualityError( + declaration.path, + declaration.line, + f"{name} depends on `{SORRY_AXIOM}` but is not registered as an " + "open declaration in Challenge/challenges.yml", + ) + ) + if extra_axioms: + errors.append( + _QualityError( + declaration.path, + declaration.line, + f"{name} depends on unallowlisted axioms: {', '.join(extra_axioms)}", + ) + ) return errors @@ -1137,14 +1439,7 @@ def _check_project_card( ) -> list[_QualityError]: if not entry_path.exists(): return [] - text = entry_path.read_text() - expected = _project_card(project) - # The project card is the first module docstring (`/-!`) after the file - # header. Mathlib convention places imports between the header and the - # module docstring, so we skip past those. - body = text[_initial_header_end(text) :] - idx = body.find("/-!") - if idx >= 0 and body[idx:].startswith(expected): + if _card_is_current(entry_path.read_text(), _project_card(project)): return [] return [ _QualityError( @@ -1153,6 +1448,223 @@ def _check_project_card( ] +def _card_is_current(text: str, expected: str) -> bool: + """Whether a file's generated card matches ``expected``. + + The card is the first module docstring (`/-!`) after the file header. + Mathlib convention places imports between the header and the module + docstring, so we skip past those. + """ + body = text[_initial_header_end(text) :] + index = body.find("/-!") + return index >= 0 and body[index:].startswith(expected) + + +def _check_challenges(root: Path) -> list[_QualityError]: + """Validate the challenge registry, its cards, and its imports. + + These are the checks that need no Lean subprocess; the axiom side of + challenge mode lives in :func:`_check_challenge_axioms`. + """ + registry = challenge.registry_path(root) + if not challenge.statement_files(root) and not registry.exists(): + # An empty board is fine: the libraries can exist with nothing on + # them, which is how challenge mode ships before its first entry. + return [] + errors = [ + _QualityError(path, 1, message) + for path, message in challenge.registry_errors(root) + ] + if errors: + return errors + errors.extend(_check_challenge_imports(root)) + errors.extend(_check_challenge_open_declarations(root)) + errors.extend(_check_solution_imports(root)) + challenges, _ = challenge.load_challenges(root) + for entry in challenges: + if not isinstance(entry, dict): + continue + entry_path = _module_to_path(root, str(entry["entry_module"])) + errors.extend(_check_challenge_statements(entry_path, registry, entry)) + errors.extend(_check_challenge_card(entry_path, registry, entry)) + errors.extend(_check_solution(root, registry, entry)) + return errors + + +def _check_solution_imports(root: Path) -> list[_QualityError]: + """Forbid a solution from importing the challenge it answers. + + Comparator exports the challenge and solution environments separately + and compares the statements. A solution that imports the challenge + module would inherit the statement (and its `sorry`) instead of + restating it, which is precisely the check being skipped. + """ + errors: list[_QualityError] = [] + prefix = f"{challenge.LIBRARY_NAME}." + for path in challenge.solution_proof_files(root): + stripped = _strip_lean_comments(path.read_text()) + for line_number, line in enumerate(stripped.splitlines(), start=1): + match = re.match(r"^\s*(?:public\s+)?import\s+([A-Za-z0-9_'.]+)\s*$", line) + if match and match.group(1).startswith(prefix): + errors.append( + _QualityError( + path, + line_number, + f"a solution may not import the challenge module " + f"({match.group(1)}); restate the statement and prove it", + ) + ) + return errors + + +def _check_solution( + root: Path, + registry: Path, + entry: dict[str, Any], +) -> list[_QualityError]: + """Check the in-repo solution module of a solved challenge.""" + module = challenge.solution_module(entry) + if module is None: + return [] + path = _module_to_path(root, module) + if not path.exists(): + return [_QualityError(registry, 1, f"solution module {module} does not exist")] + errors: list[_QualityError] = [] + declared = {declaration.name for declaration in _declarations_in([path])} + errors.extend( + _QualityError( + registry, + 1, + f"solution {module} does not declare {name}; comparator compares the " + "challenge and solution environments by declaration name", + ) + for name in challenge.open_declaration_names(entry) + if name not in declared + ) + if not _card_is_current(path.read_text(), challenge.solution_card(entry)): + errors.append( + _QualityError( + registry, + 1, + f"solution card for {entry['slug']} is out of date; regenerate with " + "`python -m lean_pool.quality --write-challenge-cards`", + ) + ) + return errors + + +def _check_challenge_imports(root: Path) -> list[_QualityError]: + """Require challenge statements to be phrased in Mathlib vocabulary. + + A challenge is a contract: whoever attempts it, and whoever reviews the + attempt, has to be able to read the statement without auditing pool + code. Restricting imports to Mathlib keeps that boundary small and + keeps a statement from resting on a pooled project that may later be + refactored underneath it. + """ + errors: list[_QualityError] = [] + for path in challenge.statement_files(root): + text = path.read_text() + stripped = _strip_lean_comments(text) + for line_number, line in enumerate(stripped.splitlines(), start=1): + match = re.match(r"^\s*(?:public\s+)?import\s+([A-Za-z0-9_'.]+)\s*$", line) + if match and not match.group(1).startswith("Mathlib."): + errors.append( + _QualityError( + path, + line_number, + f"challenge statements may import only Mathlib modules; " + f"found {match.group(1)}", + ) + ) + return errors + + +def _check_challenge_open_declarations(root: Path) -> list[_QualityError]: + """Require every `sorry` to belong to a declaration the registry lists. + + The Lean-backed audits establish this from the compiled environment, + which is the authoritative check. Doing it textually as well points at + the offending line for a contributor running without Lean, and covers + `private` declarations that `#print axioms` never enumerates. + """ + permitted = _open_declarations(root) + errors: list[_QualityError] = [] + for path in challenge.statement_files(root): + declarations = _declarations_in([path], include_private=True) + stripped = _strip_lean_comments(path.read_text()) + for line_number, line in enumerate(stripped.splitlines(), start=1): + if not WHOLE_BODY_SORRY.search(line): + continue + owner = _enclosing_declaration(declarations, line_number) + if owner is not None and owner.name in permitted: + continue + owner_name = owner.name if owner is not None else "no declaration" + errors.append( + _QualityError( + path, + line_number, + f"sorry belongs to {owner_name}, which " + f"{challenge.REGISTRY_RELATIVE_PATH} does not list as an open " + "declaration", + ) + ) + return errors + + +def _enclosing_declaration( + declarations: list[_Declaration], line_number: int +) -> _Declaration | None: + """Return the declaration a line belongs to, or ``None`` before the first.""" + enclosing = None + for declaration in declarations: + if declaration.line > line_number: + break + enclosing = declaration + return enclosing + + +def _check_challenge_statements( + entry_path: Path, + registry: Path, + entry: dict[str, Any], +) -> list[_QualityError]: + """Require every registered open declaration to exist in the file.""" + if not entry_path.exists(): + return [] + declared = {declaration.name for declaration in _declarations_in([entry_path])} + return [ + _QualityError( + registry, + 1, + f"challenge {entry['slug']} declares {name}, which is not declared " + f"in {entry['entry_module']}", + ) + for name in challenge.open_declaration_names(entry) + if name not in declared + ] + + +def _check_challenge_card( + entry_path: Path, + registry: Path, + entry: dict[str, Any], +) -> list[_QualityError]: + """Keep the generated challenge card in sync with the registry.""" + if not entry_path.exists(): + return [] + if _card_is_current(entry_path.read_text(), challenge.challenge_card(entry)): + return [] + return [ + _QualityError( + registry, + 1, + f"challenge card for {entry['slug']} is out of date; regenerate with " + "`python -m lean_pool.quality --write-challenge-cards`", + ) + ] + + def _initial_header_end(text: str) -> int: if not text.startswith("/-"): return 0 @@ -1206,12 +1718,33 @@ def _write_project_cards(root: Path) -> None: _write_project_card(entry_path, _project_card(project)) +def _write_challenge_cards(root: Path) -> None: + """Regenerate challenge and solution cards from the registry.""" + challenges, errors = challenge.load_challenges(root) + if errors: + raise SystemExit("\n".join(f"{path}: {message}" for path, message in errors)) + for entry in challenges: + if not isinstance(entry, dict) or "entry_module" not in entry: + continue + entry_path = _module_to_path(root, str(entry["entry_module"])) + if entry_path.exists(): + _write_project_card(entry_path, challenge.challenge_card(entry)) + module = challenge.solution_module(entry) + if module is None: + continue + solution_path = _module_to_path(root, module) + if solution_path.exists(): + _write_project_card(solution_path, challenge.solution_card(entry)) + + _PROJECT_CARD_RE = re.compile( - # A project card is a `/-! ... -/` block whose first content line is an - # h1 heading and which contains a `Source:` line. Matching on `Source:` + # A generated card is a `/-! ... -/` block whose first content line is an + # h1 heading and which contains a `Source:` line (projects and + # challenges) or a `Challenge:` line (solutions). Matching on those keys # distinguishes it from sibling docstrings like `/-! ## Mathematical # overview ... -/`. Non-greedy + DOTALL so we capture exactly one block. - r"/-!\s*\n#\s+[^\n]+\n(?:[^\n]*\n)*?Source:[^\n]+\n(?:[^\n]*\n)*?-/\n*", + r"/-!\s*\n#\s+[^\n]+\n(?:[^\n]*\n)*?(?:Source|Challenge):[^\n]+\n" + r"(?:[^\n]*\n)*?-/\n*", re.MULTILINE, ) _IMPORT_LINE_RE = re.compile(r"^\s*(?:public\s+)?import\s+\S+\s*$") @@ -1281,10 +1814,13 @@ def run_checks(root: Path, *, skip_lean_axioms: bool = False) -> list[_QualityEr _check_file_sizes, _check_proof_sizes, _check_projects, + _check_challenges, ] errors = [error for check in checks for error in check(root)] if not skip_lean_axioms: errors.extend(_check_axioms(root)) + errors.extend(_check_challenge_axioms(root)) + errors.extend(_check_solution_axioms(root)) errors.extend(_check_option_backdoors(root)) return sorted( errors, key=lambda error: (str(error.path), error.line, error.message) @@ -1310,6 +1846,11 @@ def _parse_args(argv: list[str]) -> argparse.Namespace: action="store_true", help="Rewrite project-card module docstrings from LeanPool/projects.yml.", ) + parser.add_argument( + "--write-challenge-cards", + action="store_true", + help="Rewrite challenge-card module docstrings from Challenge/challenges.yml.", + ) return parser.parse_args(argv) @@ -1319,6 +1860,8 @@ def main(argv: list[str] | None = None) -> int: root = args.repo.resolve() if args.write_project_cards: _write_project_cards(root) + if args.write_challenge_cards: + _write_challenge_cards(root) errors = run_checks(root, skip_lean_axioms=args.skip_lean_axioms) if errors: diff --git a/python/lean_pool/review.py b/python/lean_pool/review.py index 814a57d614..fa3cc988d5 100644 --- a/python/lean_pool/review.py +++ b/python/lean_pool/review.py @@ -1,14 +1,28 @@ """LLM-driven pull request review for Lean Pool. -Detects whether the PR adds a new project or refactors projects already in -the pool — the same added-vs-modified split ``/profile`` uses — and reviews -it under the matching rules. New-project PRs are judged on fit and -significance (``.github/REVIEW_RULES.md``); refactor PRs are judged on tech -debt and maintainability (``.github/REFACTOR_REVIEW_RULES.md``). Either way -it fetches the PR diff via the GitHub CLI, asks the configured OpenAI model -to evaluate the contribution, and posts or updates a sticky PR comment with -the reviewed head SHA, a one-paragraph summary, a structured assessment -table, a verdict, and any specific findings. +Detects what kind of PR this is and reviews it under the matching rules: + +- **project** — adds a new project to the pool. Judged on fit and + significance (``.github/REVIEW_RULES.md``). +- **refactor** — only touches projects already in the pool, the same + added-vs-modified split ``/profile`` uses. Judged on tech debt and + maintainability (``.github/REFACTOR_REVIEW_RULES.md``). +- **challenge** — adds or edits an open statement under ``Challenge/``. + Judged on whether the problem is worth stating, whether the Lean says + what the prose says, whether a cited known result is stated correctly, + whether it is vacuous or gameable, and how much Lean a solution would + take (``.github/CHALLENGE_REVIEW_RULES.md``). +- **solution** — answers a challenge. Correctness belongs to + ``leanprover/comparator``, which replays the proof through the Lean + kernel in its own CI check, so this review is short and narrow + (``.github/SOLUTION_REVIEW_RULES.md``) — and is skipped outright when the + PR touches nothing but the answer and its registry entry and the + challenge left no definition hole. See :func:`solution_needs_llm_review`. + +Otherwise it fetches the PR diff via the GitHub CLI, asks the configured +OpenAI model to evaluate the contribution, and posts or updates a sticky PR +comment with the reviewed head SHA, a one-paragraph summary, a structured +assessment table, a verdict, and any specific findings. The reviewer prefers OpenAI's ``flex`` tier (cheaper, slower, occasionally unavailable). When flex returns 429 Resource Unavailable, the request is @@ -48,6 +62,7 @@ import json import os +import re import subprocess import sys from dataclasses import dataclass @@ -57,13 +72,24 @@ from openai import APIStatusError, BadRequestError, OpenAI, RateLimitError +from lean_pool import challenge + REPO_ROOT = Path(__file__).resolve().parents[2] PROJECT_RULES_PATH = REPO_ROOT / ".github" / "REVIEW_RULES.md" REFACTOR_RULES_PATH = REPO_ROOT / ".github" / "REFACTOR_REVIEW_RULES.md" +CHALLENGE_RULES_PATH = REPO_ROOT / ".github" / "CHALLENGE_REVIEW_RULES.md" +SOLUTION_RULES_PATH = REPO_ROOT / ".github" / "SOLUTION_REVIEW_RULES.md" DEFAULT_MODEL = "gpt-5.5" # Flex tier requests can take longer than the default 10-minute timeout. REQUEST_TIMEOUT_SECONDS = 6000.0 LLM_REVIEW_MARKER = "" +# Said up front on every solution comment: whatever the model writes, the +# proof itself was judged by a kernel, not by a language model. +COMPARATOR_DISCLAIMER = ( + "> Correctness is decided by the **Verify challenge solutions** check " + "(`leanprover/comparator` replays the proof through the Lean kernel and " + "compares it against the challenge statement), not by this review." +) # Input-token guardrail. OpenAI rejected PR #278's review at a configured # limit of 922k input tokens; its 3,112,190-character diff measured ~2.0 @@ -101,6 +127,14 @@ "request_changes": "🛑", "needs_discussion": "🤔", } +# Rules document each PR kind is reviewed against, linked in the comment +# footer and read as the model's user message. +RULES_DOC_NAME = { + "project": "REVIEW_RULES.md", + "refactor": "REFACTOR_REVIEW_RULES.md", + "challenge": "CHALLENGE_REVIEW_RULES.md", + "solution": "SOLUTION_REVIEW_RULES.md", +} FIT_ICON = { "good_fit": "✅", "borderline": "🟡", @@ -120,6 +154,22 @@ "more_brittle": "🛑", } RISK_ICON = {"low": "✅", "medium": "🟡", "high": "🛑"} +# Challenge-assessment icons. A challenge is only as good as the match +# between its Lean and its prose, so faithfulness and vacuity get the +# loudest markers. +SIGNIFICANCE_ICON = {"high": "✅", "moderate": "🟡", "low": "🛑"} +FAITHFULNESS_ICON = {"faithful": "✅", "drifts": "🟡", "mismatch": "🛑"} +SOURCE_MATCH_ICON = { + "matches": "✅", + "mismatch": "🛑", + "unverifiable": "🟡", + "not_a_known_result": "➖", +} +VACUITY_ICON = {"none": "✅", "possible": "🟡", "vacuous": "🛑"} +# Solution-assessment icons. Statement tampering is the one thing a +# solution PR can do that comparator cannot catch on its own. +TAMPERING_ICON = {True: "🛑", False: "✅"} +HOLE_RISK_ICON = {"none": "✅", "review_needed": "🟡", "gamed": "🛑"} SYSTEM_PROMPT_PROJECT = dedent( """\ @@ -173,6 +223,82 @@ ) +SYSTEM_PROMPT_CHALLENGE = dedent( + """\ + You are a senior mathematician and Lean engineer reviewing a challenge + pull request to Lean Pool. A challenge is an OPEN statement: a theorem + written in Mathlib vocabulary, left as `sorry`, that the pool is asking + someone to prove. Nothing in this PR is proved, and that is correct — + never treat the `sorry` as a defect. + + Your job is to tell the maintainer whether this belongs on the board. + Judge four things above all: whether the problem is significant (a + recognized open problem or a genuinely hard unformalized result, not a + pet conjecture or an exercise); whether the Lean statement faithfully + says what the informal statement says, quantifier by quantifier and + definition by definition; whether a cited known result is stated the way + its source states it; and whether the statement is vacuous, trivial, or + gameable. Then estimate how many lines of Lean a solution would take and + say what the estimate rests on. + + A merged challenge is a contract — `leanprover/comparator` compares + submitted solutions against exactly this text — so quote the Lean when + you claim it means something other than the prose does. + + Write to a colleague: direct, no encouragement, no editorializing. + Mechanical issues (headers, naming, line length, the sorry policy, + registry schema, axiom audits) are enforced by CI gates elsewhere. Do + NOT flag those. + + Always respond with a single JSON object matching the schema in the + rules document. The `assessment` block is the core deliverable. + `findings` is for specific, actionable concerns; an empty list is fine + for a well-stated challenge. + """ +) + + +SYSTEM_PROMPT_SOLUTION = dedent( + """\ + You are reviewing a solution pull request to Lean Pool: it answers a + challenge already on the board. Be brief. + + Correctness is NOT your call. `leanprover/comparator` replays the + solution through the Lean kernel and checks that it proves the same + statement as the challenge with no axiom beyond propext, Quot.sound, + and Classical.choice; that runs as its own CI check. You usually cannot + even see the challenge statement — it is not in the diff. Never assert + that a proof is correct or incorrect. + + Three things are yours. First, statement tampering: if the diff touches + anything under `Challenge/`, quote it and say plainly whether the + statement changed — editing the text a solver is being judged against, + in the PR that claims to meet it, is the one way to fake a solution + past comparator. Second, definition holes: comparator matches a hole + only by name and type, so a filled hole may restate the question + instead of answering it. Third, proof quality by the pool's usual + standard — agent slop, brittle one-shot automation, dead branches. + + Everything else is gated by CI: sorry, axioms, headers, imports, sizes, + registry schema, card sync. Do not flag those. Do not re-litigate + whether the problem was worth stating. + + Always respond with a single JSON object matching the schema in the + rules document. A clean solution deserves a two-sentence summary and an + empty `findings` list. + """ +) + + +# Rules document and system prompt per PR kind, keyed by `classify_pr`. +REVIEW_MODES: dict[str, tuple[Path, str]] = { + "project": (PROJECT_RULES_PATH, SYSTEM_PROMPT_PROJECT), + "refactor": (REFACTOR_RULES_PATH, SYSTEM_PROMPT_REFACTOR), + "challenge": (CHALLENGE_RULES_PATH, SYSTEM_PROMPT_CHALLENGE), + "solution": (SOLUTION_RULES_PATH, SYSTEM_PROMPT_SOLUTION), +} + + def run_gh(*args: str, stdin: str | None = None) -> str: """Run ``gh`` with the given arguments and return stdout. @@ -298,20 +424,52 @@ def project_of(path: str) -> str | None: return None +def is_challenge_statement(path: str) -> bool: + """Whether ``path`` is a challenge statement file. + + Statements live at ``Challenge/.lean``; the auto-generated root + ``Challenge.lean`` index is not one. + """ + return path.startswith("Challenge/") and path.endswith(".lean") + + +def is_solution_file(path: str) -> bool: + """Whether ``path`` is an in-repo answer to a challenge.""" + return path.startswith("Solution/") and path.endswith(".lean") + + def classify_pr(files: list[tuple[str, str]]) -> str: - """Classify a PR as ``"refactor"`` or ``"project"``. - - Mirrors ``/profile``'s added-vs-modified split lifted to the PR level: a - PR that adds a *new project* (a project directory that appears only - through added ``.lean`` files) is a ``"project"`` PR and gets the full - fit/significance review. A PR that only changes files in projects - already in the pool — the pure-golf / reorganization case — is a - ``"refactor"`` and gets the tech-debt review. When no project files are - touched at all, default to ``"project"`` (the conservative review). + """Classify a PR by what it is asking the maintainer to accept. + + - ``"challenge"`` — puts an open statement on the board, or edits one + already there, without touching pooled Lean content. Judged on + significance, faithfulness of the Lean to the prose, and cost; there + is no proof in it to judge. + - ``"solution"`` — answers a challenge. Correctness is settled by + comparator, so the review is short and narrow. + - ``"project"`` — adds a new project (a project directory that appears + only through added ``.lean`` files). The full fit/significance review. + - ``"refactor"`` — only changes files in projects already in the pool, + the pure-golf / reorganization case. The tech-debt review. + + A *new* challenge statement wins over everything else: whatever else is + in the PR, the board entry is what needs judging. Otherwise a mixed PR + falls through to the content classification, which is the conservative + choice — a Lean/Mathlib bump repairing every library should not be + reviewed as a challenge. When no Lean content is touched at all, default + to ``"project"``. """ added_projects: set[str] = set() existing_projects: set[str] = set() + added_statements = False + touched_statements = False + touched_solutions = False for name, status in files: + if is_challenge_statement(name): + touched_statements = True + added_statements = added_statements or status == "added" + if is_solution_file(name): + touched_solutions = True if not name.endswith(".lean"): continue project = project_of(name) @@ -321,12 +479,61 @@ def classify_pr(files: list[tuple[str, str]]) -> str: added_projects.add(project) else: # modified / removed / renamed / changed / copied existing_projects.add(project) + pool_content = bool(added_projects or existing_projects) + if added_statements: + return "challenge" + if touched_solutions: + return "solution" + if touched_statements and not pool_content: + return "challenge" new_projects = added_projects - existing_projects if not new_projects and existing_projects: return "refactor" return "project" +# Paths a plain solution PR may touch: the answer, the regenerated index, +# and the registry entry recording it. Anything else — a statement edit, +# a pooled project, tooling — means there is something to read. +SOLUTION_ONLY_PATH = re.compile( + r"^(Solution\.lean|Solution/.+\.lean|Challenge/challenges\.yml)$" +) + + +def solution_needs_llm_review(files: list[tuple[str, str]], root: Path) -> str | None: + """Return why a solution PR still needs a reading, or ``None``. + + Comparator decides whether a solution proves the challenge, and the + quality gates decide the rest, so most solution PRs have nothing left + for a language model to weigh in on. Two things do: + + - the PR touches something beyond the answer itself, or + - the challenge leaves a *definition hole*, which comparator can only + check by name and type — a solver can define the hole in terms of the + object the challenge asks about, so a human (or a model) has to look. + """ + extra = sorted(name for name, _ in files if not SOLUTION_ONLY_PATH.match(name)) + if extra: + return f"the PR also touches {', '.join(extra[:5])}" + touched = {name for name, _ in files if is_solution_file(name)} + challenges, errors = challenge.load_challenges(root) + if errors: + return "the challenge registry could not be read" + for entry in challenges: + if not isinstance(entry, dict): + continue + module = challenge.solution_module(entry) + if module is None: + continue + path = "/".join(module.split(".")) + ".lean" + if path in touched and challenge.definition_names(entry): + return ( + f"challenge `{entry.get('slug')}` leaves a definition hole, which " + "comparator only checks by name and type" + ) + return None + + def estimate_tokens(text: str) -> int: """Conservatively estimate how many model tokens ``text`` costs. @@ -670,6 +877,85 @@ def render_refactor_assessment(payload: dict) -> str: return table +def render_challenge_assessment(payload: dict) -> str: + """Render a challenge assessment block as a Markdown table.""" + a = payload.get("assessment") or {} + if not a: + return "" + + significance = a.get("significance", "") + faithfulness = a.get("faithfulness", "") + source_match = a.get("source_match", "") + vacuity = a.get("vacuity_risk", "") + estimate = a.get("estimated_lines") + estimate_cell = f"~{estimate:,} lines" if isinstance(estimate, int) else "?" + basis = (a.get("estimate_basis") or "").strip() + if basis: + estimate_cell += f" — {basis}" + + rows = [ + ("Significance", _icon_cell(SIGNIFICANCE_ICON, significance)), + ("Faithful to the prose", _icon_cell(FAITHFULNESS_ICON, faithfulness)), + ("Matches cited source", _icon_cell(SOURCE_MATCH_ICON, source_match)), + ("Vacuity risk", _icon_cell(VACUITY_ICON, vacuity)), + ("Difficulty", f"`{a.get('difficulty', '?')}`"), + ("Estimated solution size", estimate_cell), + ] + already = (a.get("already_formalized") or "").strip() + if already: + rows.append(("Already formalized", f"🛑 `{already}`")) + + table = "| Aspect | Value |\n|---|---|\n" + for key, value in rows: + table += f"| {key} | {value} |\n" + + note = (a.get("faithfulness_note") or "").strip() + if note: + table += f"\n**Statement check:** {note}\n" + sentence = (a.get("assessment_one_sentence") or "").strip() + if sentence: + table += f"\n_{sentence}_" + return table + + +def _icon_cell(icons: dict[str, str], value: str) -> str: + """Render one assessment value with its status icon.""" + if not value: + return "?" + return f"{icons.get(value, '•')} `{value}`" + + +def render_solution_assessment(payload: dict) -> str: + """Render a solution assessment block as a Markdown table.""" + a = payload.get("assessment") or {} + if not a: + return "" + + tampering = a.get("touches_challenge_statement") + tampering_cell = ( + f"{TAMPERING_ICON.get(bool(tampering), '•')} {'yes' if tampering else 'no'}" + if tampering is not None + else "?" + ) + quality = a.get("proof_quality") + rows = [ + ("Touches the challenge statement", tampering_cell), + ( + "Definition-hole risk", + _icon_cell(HOLE_RISK_ICON, a.get("definition_hole_risk", "")), + ), + ("Proof quality", f"{quality} / 5" if quality is not None else "?"), + ] + table = "| Aspect | Value |\n|---|---|\n" + for key, value in rows: + table += f"| {key} | {value} |\n" + + sentence = (a.get("assessment_one_sentence") or "").strip() + if sentence: + table += f"\n_{sentence}_" + return table + + def render_comment( payload: dict, model: str, @@ -681,21 +967,25 @@ def render_comment( ) -> str: """Render the model's payload as a Markdown PR comment body. - ``kind`` is ``"project"`` (fit/significance review) or ``"refactor"`` - (tech-debt review); it selects the header, the assessment table, and - the rules doc linked in the footer. When ``truncation`` is set, the - comment states up front that the model reviewed a reduced diff. + ``kind`` is ``"project"`` (fit/significance review), ``"refactor"`` + (tech-debt review), or ``"challenge"`` (open-statement review); it + selects the header, the assessment table, and the rules doc linked in + the footer. When ``truncation`` is set, the comment states up front + that the model reviewed a reduced diff. """ summary = (payload.get("summary") or "").strip() verdict = (payload.get("verdict") or "").strip() findings = payload.get("findings") or [] - heading = ( - f"## 🤖 LLM review — refactor (`{model}`)" - if kind == "refactor" - else f"## 🤖 LLM review (`{model}`)" - ) + headings = { + "refactor": f"## 🤖 LLM review — refactor (`{model}`)", + "challenge": f"## 🤖 LLM review — challenge (`{model}`)", + "solution": f"## 🤖 LLM review — challenge solution (`{model}`)", + } + heading = headings.get(kind, f"## 🤖 LLM review (`{model}`)") lines = [LLM_REVIEW_MARKER, heading, ""] + if kind == "solution": + lines.extend([COMPARATOR_DISCLAIMER, ""]) if reviewed_head_sha: lines.extend([f"**Reviewed head:** `{reviewed_head_sha}`", ""]) @@ -720,11 +1010,12 @@ def render_comment( if summary: lines.extend([summary, ""]) - assessment = ( - render_refactor_assessment(payload) - if kind == "refactor" - else render_project_assessment(payload) - ) + renderers = { + "refactor": render_refactor_assessment, + "challenge": render_challenge_assessment, + "solution": render_solution_assessment, + } + assessment = renderers.get(kind, render_project_assessment)(payload) if assessment: lines.extend([assessment, ""]) @@ -750,7 +1041,7 @@ def render_comment( usage_line = render_usage(usage, model, tier) if usage_line: lines.append(usage_line) - rules_doc = "REFACTOR_REVIEW_RULES.md" if kind == "refactor" else "REVIEW_RULES.md" + rules_doc = RULES_DOC_NAME.get(kind, "REVIEW_RULES.md") lines.append( "_Automated review against " f"[`.github/{rules_doc}`](../blob/main/.github/{rules_doc}). " @@ -759,6 +1050,40 @@ def render_comment( return "\n".join(lines) +def render_solution_skip_comment(reviewed_head_sha: str) -> str: + """Render the comment posted instead of reviewing a plain solution PR. + + A solution PR that touches nothing but the answer, the generated index, + and the registry entry has no judgment left in it: comparator decides + whether the proof proves the challenge, and the quality gates decide + everything else. Spending a model call to say so would only add noise + the maintainer has to read. + """ + return "\n".join( + [ + LLM_REVIEW_MARKER, + "## 🤖 LLM review — challenge solution (skipped)", + "", + f"**Reviewed head:** `{reviewed_head_sha}`" if reviewed_head_sha else "", + "", + "No model review: this PR only adds an answer to a challenge that is " + "already on the board, and everything about it is machine-checkable.", + "", + COMPARATOR_DISCLAIMER, + "", + "The quality gates cover the rest — no `sorry` or axioms in the " + "solution, the solution does not import the challenge module, the " + "registry records it, and the generated cards match.", + "", + "---", + "_Skip rule: a solution PR is reviewed by a model only when it touches " + "more than the answer and its registry entry, or when the challenge " + "leaves a definition hole. See " + "[`.github/SOLUTION_REVIEW_RULES.md`](../blob/main/.github/SOLUTION_REVIEW_RULES.md)._", + ] + ) + + def post_comment(pr_number: str, body: str, repo_full_name: str) -> None: """Create or update the sticky LLM review PR comment.""" comments_json = run_gh( @@ -810,27 +1135,41 @@ def main() -> int: model = os.environ.get("REVIEW_MODEL", DEFAULT_MODEL) repo_full_name = resolve_repo_full_name().strip() - # Detect whether this is a new-project PR or a refactor of projects - # already in the pool, and review it under the matching rules. - kind = classify_pr(fetch_pr_files(pr_number, repo_full_name)) - if kind == "refactor": - rules = REFACTOR_RULES_PATH.read_text(encoding="utf-8") - system_prompt = SYSTEM_PROMPT_REFACTOR - else: - rules = PROJECT_RULES_PATH.read_text(encoding="utf-8") - system_prompt = SYSTEM_PROMPT_PROJECT + # Detect what this PR is asking for — a new project, a refactor, a new + # challenge, or an answer to one — and review it under the matching + # rules. + files = fetch_pr_files(pr_number, repo_full_name) + kind = classify_pr(files) + rules_path, system_prompt = REVIEW_MODES[kind] + rules = rules_path.read_text(encoding="utf-8") print(f"Reviewing PR #{pr_number} as a {kind} PR.", file=sys.stderr) + reviewed_head_sha = ( + os.environ.get("REVIEW_HEAD_SHA") + or fetch_head_sha(pr_number, repo_full_name).strip() + ) + + if kind == "solution": + reason = solution_needs_llm_review(files, REPO_ROOT) + if reason is None: + print( + "Solution PR with nothing left to judge; posting the skip " + "note instead of calling the model.", + file=sys.stderr, + ) + post_comment( + pr_number, + render_solution_skip_comment(reviewed_head_sha), + repo_full_name=repo_full_name, + ) + return 0 + print(f"Reviewing this solution PR because {reason}.", file=sys.stderr) + diff = fetch_diff(pr_number, repo_full_name) if not diff.strip(): print("Empty diff; nothing to review.", file=sys.stderr) return 0 - - reviewed_head_sha = ( - os.environ.get("REVIEW_HEAD_SHA") - or fetch_head_sha(pr_number, repo_full_name).strip() - ) payload, usage, tier, truncation = request_review( model=model, rules=rules, diff=diff, system_prompt=system_prompt ) diff --git a/python/lean_pool/stats.py b/python/lean_pool/stats.py index 5e3f01ccef..9deaae4985 100644 --- a/python/lean_pool/stats.py +++ b/python/lean_pool/stats.py @@ -47,6 +47,7 @@ class Stats: projects: int lines_of_lean: int + open_challenges: int = 0 def count_projects(projects_yml_path: Path) -> int: @@ -97,20 +98,50 @@ def count_lean_loc(pool_dir: Path) -> int: return total +def count_open_challenges(challenges_yml_path: Path) -> int: + """Return the number of unsolved challenges on the board. + + Args: + challenges_yml_path: Path to ``Challenge/challenges.yml``. + + Returns: + How many registered challenges have ``status: open``, or ``0`` if + the file is missing, malformed, or has no ``challenges`` key. + """ + if not challenges_yml_path.is_file(): + return 0 + data = yaml.safe_load(challenges_yml_path.read_text()) or {} + if not isinstance(data, dict): + return 0 + challenges = data.get("challenges") or [] + if not isinstance(challenges, list): + return 0 + return sum( + 1 + for challenge in challenges + if isinstance(challenge, dict) and challenge.get("status") == "open" + ) + + def collect_stats(root: Path) -> Stats: """Gather all README statistics for the checkout at ``root``.""" return Stats( projects=count_projects(root / "LeanPool" / "projects.yml"), lines_of_lean=count_lean_loc(root / "LeanPool"), + open_challenges=count_open_challenges(root / "Challenge" / "challenges.yml"), ) def render_stats(stats: Stats) -> str: """Render the stats block body (without the surrounding markers).""" - return ( - f"**{stats.projects}** formalization projects · " - f"**{stats.lines_of_lean:,}** lines of Lean" - ) + parts = [ + f"**{stats.projects}** formalization projects", + f"**{stats.lines_of_lean:,}** lines of Lean", + ] + # An empty board says nothing worth a README line; omit it entirely. + if stats.open_challenges: + parts.append(f"**{stats.open_challenges}** open challenges") + return " · ".join(parts) def apply_stats(readme_text: str, stats: Stats) -> str: diff --git a/python/tests/test_challenge.py b/python/tests/test_challenge.py new file mode 100644 index 0000000000..29956d8382 --- /dev/null +++ b/python/tests/test_challenge.py @@ -0,0 +1,587 @@ +"""Tests for challenge mode: registry, cards, comparator configuration, and gates.""" + +from __future__ import annotations + +from pathlib import Path + +from lean_pool import challenge +from lean_pool.quality import ( + _Declaration, + _parse_axiom_output, + _parse_option_audit_output, + run_checks, +) + +HEADER = """/- +Copyright (c) 2026 Test Author. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Test Author +-/ +""" + +STATEMENT_BODY = """ +namespace Challenge.Widget + +/-- A test challenge. -/ +theorem widget_exists : True := sorry + +end Challenge.Widget +""" + +CHALLENGE_ENTRY = { + "slug": "widget", + "title": "Widget conjecture", + "summary": "Prove that a widget exists.", + "branch": "test mathematics", + "entry_module": "Challenge.Widget", + "proposers": ["Test Author"], + "source": {"url": "https://example.invalid/widget"}, + "license": "Apache-2.0", + "provenance": "human", + "status": "open", + "statements": [ + { + "declaration": "Challenge.Widget.widget_exists", + "informal": "A widget exists.", + } + ], + "tags": ["test"], + "msc": ["00A35"], +} + + +def _write_minimal_repo(root: Path) -> None: + """Create the smallest LeanPool tree accepted by static checks.""" + (root / "LeanPool").mkdir() + (root / "LeanPool.lean").write_text("import LeanPool.Basic\n") + (root / "LeanPool" / "Basic.lean").write_text(f'{HEADER}\ndef hello := "world"\n') + (root / "LeanPool" / "projects.yml").write_text("projects: []\n") + (root / "lakefile.toml").write_text( + 'name = "lean-pool"\nversion = "0.1.0"\ndefaultTargets = ["LeanPool"]\n' + ) + + +def _write_challenge( + root: Path, + *, + body: str = STATEMENT_BODY, + registry: str | None = None, + write_card: bool = True, + entry: dict[str, object] | None = None, +) -> None: + """Add a one-challenge library to a minimal repo.""" + (root / "Challenge").mkdir(exist_ok=True) + (root / "Challenge.lean").write_text("import Challenge.Widget\n") + card = ( + f"{challenge.challenge_card(entry or CHALLENGE_ENTRY)}\n" if write_card else "" + ) + (root / "Challenge" / "Widget.lean").write_text(f"{HEADER}\n{card}{body}") + (root / "Challenge" / "challenges.yml").write_text( + registry if registry is not None else _registry_text() + ) + + +def _registry_text(**overrides: object) -> str: + """Render `challenges.yml` for the fixture entry, with overrides.""" + entry = {**CHALLENGE_ENTRY, **overrides} + statements = "\n".join( + f" - declaration: {item['declaration']}\n" + f" informal: {item['informal']}" + for item in entry["statements"] + ) + return ( + "challenges:\n" + f" - slug: {entry['slug']}\n" + f" title: {entry['title']}\n" + f" summary: {entry['summary']}\n" + f" branch: {entry['branch']}\n" + f" entry_module: {entry['entry_module']}\n" + f" proposers: [{', '.join(entry['proposers'])}]\n" + " source:\n" + f" url: {entry['source']['url']}\n" + f" license: {entry['license']}\n" + f" provenance: {entry['provenance']}\n" + f" status: {entry['status']}\n" + " statements:\n" + f"{statements}\n" + f" tags: [{', '.join(entry['tags'])}]\n" + f" msc: ['{entry['msc'][0]}']\n" + ) + + +def test_comparator_config_lists_statements_and_axioms() -> None: + """The generated configuration is what `leanprover/comparator` consumes.""" + configuration = challenge.comparator_configuration( + CHALLENGE_ENTRY, "LeanPool.Solution" + ) + + assert configuration == { + "challenge_module": "Challenge.Widget", + "solution_module": "LeanPool.Solution", + "theorem_names": ["Challenge.Widget.widget_exists"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": False, + } + + +def test_comparator_config_declares_definition_holes() -> None: + """Definition holes are passed through as `definition_names`.""" + entry = { + **CHALLENGE_ENTRY, + "definitions": [ + {"declaration": "Challenge.Widget.answer", "informal": "The answer."} + ], + } + + configuration = challenge.comparator_configuration( + entry, "Solution", enable_nanoda=True + ) + + assert configuration["definition_names"] == ["Challenge.Widget.answer"] + assert configuration["enable_nanoda"] is True + + +def test_challenge_card_wraps_and_carries_the_informal_statement() -> None: + """The card pairs each open declaration with the prose it must match.""" + entry = { + **CHALLENGE_ENTRY, + "statements": [ + { + "declaration": "Challenge.Widget.widget_exists", + "informal": "A widget exists " + "and is very interesting " * 8, + } + ], + } + + card = challenge.challenge_card(entry) + + assert card.startswith("/-!\n# Widget conjecture\n") + assert "Source: url:https://example.invalid/widget" in card + assert "Open declarations: `Challenge.Widget.widget_exists`" in card + assert "Informal statement:" in card + assert all(len(line) <= challenge.CARD_WIDTH for line in card.splitlines()) + + +def test_challenge_repo_passes_static_quality_checks(tmp_path: Path) -> None: + """A well-formed challenge library passes without invoking Lean.""" + _write_minimal_repo(tmp_path) + _write_challenge(tmp_path) + + assert run_checks(tmp_path, skip_lean_axioms=True) == [] + + +def test_sorry_is_rejected_outside_the_challenge_library(tmp_path: Path) -> None: + """`sorry` in pooled content stays forbidden.""" + _write_minimal_repo(tmp_path) + (tmp_path / "LeanPool" / "Basic.lean").write_text( + f"{HEADER}\ntheorem hello : True := sorry\n" + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any("sorry is forbidden outside Challenge/" in e.message for e in errors) + + +def test_partial_sorry_is_rejected_inside_the_challenge_library( + tmp_path: Path, +) -> None: + """A `sorry` buried in a term leaves a challenge quietly half-open.""" + _write_minimal_repo(tmp_path) + _write_challenge( + tmp_path, + body=( + "\nnamespace Challenge.Widget\n\n" + "/-- A test challenge. -/\n" + "theorem widget_exists : True ∧ True := ⟨sorry, trivial⟩\n\n" + "end Challenge.Widget\n" + ), + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any("must be the whole proof body" in e.message for e in errors) + + +def test_admit_is_rejected_inside_the_challenge_library(tmp_path: Path) -> None: + """Challenge mode allows exactly one spelling of an open proof.""" + _write_minimal_repo(tmp_path) + _write_challenge( + tmp_path, + body=( + "\nnamespace Challenge.Widget\n\n" + "/-- A test challenge. -/\n" + "theorem widget_exists : True := by admit\n\n" + "end Challenge.Widget\n" + ), + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any("admit is forbidden" in e.message for e in errors) + + +def test_unregistered_sorry_is_rejected_without_lean(tmp_path: Path) -> None: + """A second `sorry` nobody registered is caught by the static gate too.""" + _write_minimal_repo(tmp_path) + _write_challenge( + tmp_path, + body=( + "\nnamespace Challenge.Widget\n\n" + "/-- A test challenge. -/\n" + "theorem widget_exists : True := sorry\n\n" + "/-- Scaffolding nobody declared open. -/\n" + "private theorem scaffolding : True := sorry\n\n" + "end Challenge.Widget\n" + ), + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any( + "sorry belongs to Challenge.Widget.scaffolding" in e.message for e in errors + ) + assert not any("widget_exists" in e.message for e in errors) + + +def test_challenge_imports_are_restricted_to_mathlib(tmp_path: Path) -> None: + """A statement resting on pool code is not a stable contract.""" + _write_minimal_repo(tmp_path) + _write_challenge(tmp_path) + path = tmp_path / "Challenge" / "Widget.lean" + path.write_text( + path.read_text().replace(HEADER, f"{HEADER}import LeanPool.Basic\n") + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any( + "may import only Mathlib modules" in e.message and "LeanPool.Basic" in e.message + for e in errors + ) + + +def test_unregistered_challenge_module_is_rejected(tmp_path: Path) -> None: + """Every statement file has to be on the board.""" + _write_minimal_repo(tmp_path) + _write_challenge(tmp_path) + (tmp_path / "Challenge" / "Stray.lean").write_text( + f"{HEADER}\n/-! # Stray\n\nSource: url:https://example.invalid\n-/\n" + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any("Challenge.Stray missing from" in e.message for e in errors) + + +def test_registry_declaration_must_exist_in_the_module(tmp_path: Path) -> None: + """A registry naming a declaration the file lacks is caught statically.""" + _write_minimal_repo(tmp_path) + _write_challenge( + tmp_path, + registry=_registry_text( + statements=[ + { + "declaration": "Challenge.Widget.missing", + "informal": "Nothing declares this.", + } + ] + ), + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any("which is not declared in Challenge.Widget" in e.message for e in errors) + + +def test_open_challenge_may_not_claim_a_solution(tmp_path: Path) -> None: + """`status` and the `solution` block have to agree.""" + _write_minimal_repo(tmp_path) + _write_challenge( + tmp_path, + registry=_registry_text() + + " solution:\n url: https://example.invalid\n", + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any("carries a `solution` block" in e.message for e in errors) + + +def test_solved_challenge_needs_a_solution_pointer(tmp_path: Path) -> None: + """A solved challenge records where the proof lives.""" + _write_minimal_repo(tmp_path) + _write_challenge(tmp_path, registry=_registry_text(status="solved")) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any("has no `solution` mapping" in e.message for e in errors) + + +def test_stale_challenge_card_is_rejected(tmp_path: Path) -> None: + """The card is generated, so drift from the registry is an error.""" + _write_minimal_repo(tmp_path) + _write_challenge(tmp_path, write_card=False) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any("challenge card for widget is out of date" in e.message for e in errors) + + +def _declaration(name: str) -> _Declaration: + """Build a declaration record pointing at a throwaway path.""" + return _Declaration( + name=name, path=Path("Challenge/Widget.lean"), line=7, kind="theorem" + ) + + +def test_axiom_audit_allows_sorry_only_for_registered_declarations() -> None: + """Registered statements may rest on `sorryAx`; their neighbours may not.""" + declarations = [ + _declaration("Challenge.Widget.widget_exists"), + _declaration("Challenge.Widget.helper"), + ] + output = ( + "'Challenge.Widget.widget_exists' depends on axioms: [propext, sorryAx]\n" + "'Challenge.Widget.helper' depends on axioms: [sorryAx]\n" + ) + + errors = _parse_axiom_output( + Path("/repo"), declarations, output, {"Challenge.Widget.widget_exists"} + ) + + assert len(errors) == 1 + assert "Challenge.Widget.helper depends on `sorryAx`" in errors[0].message + + +def test_axiom_audit_requires_registered_statements_to_stay_open() -> None: + """A statement proved in place is no longer the contract solvers took on.""" + declarations = [_declaration("Challenge.Widget.widget_exists")] + output = "'Challenge.Widget.widget_exists' does not depend on any axioms\n" + + errors = _parse_axiom_output( + Path("/repo"), declarations, output, {"Challenge.Widget.widget_exists"} + ) + + assert len(errors) == 1 + assert "does not depend on `sorryAx`" in errors[0].message + + +def test_axiom_audit_catches_a_statement_proved_classically() -> None: + """A proof that uses only permitted axioms still closes the statement. + + The axiom set is inside the allowlist, so the extra-axiom check has + nothing to say and the declaration *is* reported by `#print axioms` — + the gap is closed by demanding `sorryAx` outright. + """ + declarations = [_declaration("Challenge.Widget.widget_exists")] + output = ( + "'Challenge.Widget.widget_exists' depends on axioms: [propext, " + "Classical.choice]\n" + ) + + errors = _parse_axiom_output( + Path("/repo"), declarations, output, {"Challenge.Widget.widget_exists"} + ) + + assert len(errors) == 1 + assert "does not depend on `sorryAx`" in errors[0].message + + +def test_option_audit_tolerates_sorry_in_registered_declarations( + tmp_path: Path, +) -> None: + """A definition hole surfaces in the environment audit; that is expected.""" + stdout = ( + "LEANPOOL_OPTION_AUDIT|Challenge.Widget|Challenge.Widget.answer|" + "references forbidden axiom-injecting constants: sorryAx\n" + "LEANPOOL_OPTION_AUDIT|Challenge.Widget|Challenge.Widget.answer.eq_def|" + "references forbidden axiom-injecting constants: sorryAx\n" + "LEANPOOL_OPTION_AUDIT_COMPLETE\n" + ) + + errors = _parse_option_audit_output( + tmp_path, stdout, "", open_declarations={"Challenge.Widget.answer"} + ) + + assert errors == [] + + +def test_option_audit_still_reports_unregistered_sorry(tmp_path: Path) -> None: + """The tolerance is scoped to declarations the registry lists.""" + stdout = ( + "LEANPOOL_OPTION_AUDIT|Challenge.Widget|Challenge.Widget.sneaky|" + "references forbidden axiom-injecting constants: sorryAx\n" + "LEANPOOL_OPTION_AUDIT_COMPLETE\n" + ) + + errors = _parse_option_audit_output( + tmp_path, stdout, "", open_declarations={"Challenge.Widget.answer"} + ) + + assert len(errors) == 1 + assert "Challenge.Widget.sneaky" in errors[0].message + + +SOLVED_REGISTRY_SUFFIX = ( + " solution:\n" + " module: Solution.Widget\n" + " authors: [Test Author]\n" + ' verified: "2026-07-26"\n' +) + +SOLUTION_BODY = """ +namespace Challenge.Widget + +/-- A test challenge. -/ +theorem widget_exists : True := trivial + +end Challenge.Widget +""" + + +def _solved_entry() -> dict[str, object]: + """The fixture entry, marked solved by an in-repo module.""" + return { + **CHALLENGE_ENTRY, + "status": "solved", + "solution": { + "module": "Solution.Widget", + "authors": ["Test Author"], + "verified": "2026-07-26", + }, + } + + +def _write_solution(root: Path, *, body: str = SOLUTION_BODY) -> None: + """Add a solution library answering the fixture challenge.""" + (root / "Solution").mkdir(exist_ok=True) + (root / "Solution.lean").write_text("import Solution.Widget\n") + card = challenge.solution_card(_solved_entry()) + (root / "Solution" / "Widget.lean").write_text(f"{HEADER}\n{card}\n{body}") + + +def _write_solved_challenge(root: Path, **solution_kwargs: str) -> None: + """Write a solved challenge plus its in-repo solution.""" + _write_challenge( + root, + registry=_registry_text(status="solved") + SOLVED_REGISTRY_SUFFIX, + entry=_solved_entry(), + ) + _write_solution(root, **solution_kwargs) + + +def test_solved_challenge_with_solution_passes_static_checks(tmp_path: Path) -> None: + """The whole solved-challenge shape is accepted without invoking Lean.""" + _write_minimal_repo(tmp_path) + _write_solved_challenge(tmp_path) + + assert run_checks(tmp_path, skip_lean_axioms=True) == [] + + +def test_solution_may_not_import_the_challenge(tmp_path: Path) -> None: + """Importing the challenge would inherit the statement, not restate it.""" + _write_minimal_repo(tmp_path) + _write_solved_challenge(tmp_path) + path = tmp_path / "Solution" / "Widget.lean" + path.write_text( + path.read_text().replace(HEADER, f"{HEADER}import Challenge.Widget\n") + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any("may not import the challenge module" in e.message for e in errors) + + +def test_solution_must_declare_the_challenge_statement(tmp_path: Path) -> None: + """Comparator matches by name, so the name has to be there.""" + _write_minimal_repo(tmp_path) + _write_solved_challenge( + tmp_path, + body=( + "\nnamespace Challenge.Widget\n\n" + "/-- Something else entirely. -/\n" + "theorem widget_exists' : True := trivial\n\n" + "end Challenge.Widget\n" + ), + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any( + "does not declare Challenge.Widget.widget_exists" in e.message for e in errors + ) + + +def test_sorry_is_rejected_in_a_solution(tmp_path: Path) -> None: + """A solution is a proof; the challenge library's licence stops here.""" + _write_minimal_repo(tmp_path) + _write_solved_challenge( + tmp_path, + body=( + "\nnamespace Challenge.Widget\n\n" + "/-- A test challenge. -/\n" + "theorem widget_exists : True := sorry\n\n" + "end Challenge.Widget\n" + ), + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any("sorry is forbidden outside Challenge/" in e.message for e in errors) + + +def test_unregistered_solution_module_is_rejected(tmp_path: Path) -> None: + """Every file under Solution/ answers a registered challenge.""" + _write_minimal_repo(tmp_path) + _write_solved_challenge(tmp_path) + (tmp_path / "Solution" / "Stray.lean").write_text( + f"{HEADER}\n/-! # Stray\n\nChallenge: none\n-/\n" + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any( + "solution module Solution.Stray is not the recorded solution" in e.message + for e in errors + ) + + +def test_solution_module_must_live_in_the_solution_library(tmp_path: Path) -> None: + """A `module:` pointing outside `Solution/` is a registry error.""" + _write_minimal_repo(tmp_path) + _write_challenge( + tmp_path, + registry=_registry_text(status="solved") + + " solution:\n module: LeanPool.Basic\n", + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any("must live in the Solution library" in e.message for e in errors) + + +def test_solution_card_records_the_challenge_it_answers() -> None: + """The card tells a reader what the restated statement is for.""" + card = challenge.solution_card(_solved_entry()) + + assert card.startswith("/-!\n# Solution: Widget conjecture\n") + assert "Challenge: `widget` (`Challenge.Widget`)" in card + assert "Verified with comparator: 2026-07-26" in card + assert "must not import" in card + assert all(len(line) <= challenge.CARD_WIDTH for line in card.splitlines()) + + +def test_option_audit_still_reports_combined_findings(tmp_path: Path) -> None: + """`sorryAx` plus anything else is never tolerated.""" + stdout = ( + "LEANPOOL_OPTION_AUDIT|Challenge.Widget|Challenge.Widget.answer|" + "references forbidden axiom-injecting constants: sorryAx; declares an axiom\n" + "LEANPOOL_OPTION_AUDIT_COMPLETE\n" + ) + + errors = _parse_option_audit_output( + tmp_path, stdout, "", open_declarations={"Challenge.Widget.answer"} + ) + + assert len(errors) == 1 + assert "declares an axiom" in errors[0].message diff --git a/python/tests/test_review.py b/python/tests/test_review.py index 70c22abc2c..b05b383528 100644 --- a/python/tests/test_review.py +++ b/python/tests/test_review.py @@ -100,6 +100,248 @@ def test_classify_pr_without_project_files_defaults_to_project() -> None: assert classify_pr([("README.md", "modified")]) == "project" +def test_classify_pr_new_challenge_is_challenge() -> None: + """Putting an open statement on the board gets the challenge review.""" + from lean_pool.review import classify_pr + + files = [ + ("Challenge/TwinPrimes.lean", "added"), + ("Challenge/challenges.yml", "modified"), + ("Challenge.lean", "modified"), + ] + assert classify_pr(files) == "challenge" + + +def test_classify_pr_edited_challenge_is_challenge() -> None: + """Editing a live statement is reviewed as a challenge, not a refactor.""" + from lean_pool.review import classify_pr + + assert classify_pr([("Challenge/TwinPrimes.lean", "modified")]) == "challenge" + + +def test_classify_pr_challenge_plus_pool_content_is_not_challenge() -> None: + """A bump repairing both libraries keeps the content classification.""" + from lean_pool.review import classify_pr + + files = [ + ("Challenge/TwinPrimes.lean", "modified"), + ("LeanPool/Foo/A.lean", "modified"), + ] + assert classify_pr(files) == "refactor" + + +def test_classify_pr_answer_is_solution() -> None: + """Adding an answer to a challenge already on the board is a solution.""" + from lean_pool.review import classify_pr + + files = [ + ("Solution/TwoPlusTwo.lean", "added"), + ("Solution.lean", "modified"), + ("Challenge/challenges.yml", "modified"), + ] + assert classify_pr(files) == "solution" + + +def test_classify_pr_new_challenge_with_its_answer_is_challenge() -> None: + """A new board entry is judged as one even when its proof rides along.""" + from lean_pool.review import classify_pr + + files = [ + ("Challenge/Widget.lean", "added"), + ("Solution/Widget.lean", "added"), + ("Challenge/challenges.yml", "modified"), + ] + assert classify_pr(files) == "challenge" + + +def test_classify_pr_delegated_solution_is_solution() -> None: + """A solution backed by a pooled project is still a solution PR.""" + from lean_pool.review import classify_pr + + files = [ + ("Solution/Widget.lean", "added"), + ("LeanPool/WidgetProof/A.lean", "added"), + ("LeanPool/projects.yml", "modified"), + ("Challenge/challenges.yml", "modified"), + ] + assert classify_pr(files) == "solution" + + +def test_plain_solution_pr_skips_the_model(tmp_path) -> None: + """Nothing but an answer and its registry entry: nothing to review.""" + from lean_pool.review import solution_needs_llm_review + + (tmp_path / "Challenge").mkdir() + (tmp_path / "Challenge" / "challenges.yml").write_text( + "challenges:\n" + " - slug: widget\n" + " entry_module: Challenge.Widget\n" + " statements:\n" + " - declaration: Challenge.Widget.widget_exists\n" + " informal: A widget exists.\n" + " solution:\n" + " module: Solution.Widget\n" + ) + files = [ + ("Solution/Widget.lean", "added"), + ("Solution.lean", "modified"), + ("Challenge/challenges.yml", "modified"), + ] + + assert solution_needs_llm_review(files, tmp_path) is None + + +def test_solution_pr_touching_the_statement_is_reviewed(tmp_path) -> None: + """Anything beyond the answer itself gets a reading.""" + from lean_pool.review import solution_needs_llm_review + + (tmp_path / "Challenge").mkdir() + (tmp_path / "Challenge" / "challenges.yml").write_text("challenges: []\n") + files = [ + ("Solution/Widget.lean", "added"), + ("Challenge/Widget.lean", "modified"), + ] + + reason = solution_needs_llm_review(files, tmp_path) + + assert reason is not None + assert "Challenge/Widget.lean" in reason + + +def test_solution_pr_for_a_definition_hole_is_reviewed(tmp_path) -> None: + """Comparator matches a hole by name and type only, so a human looks.""" + from lean_pool.review import solution_needs_llm_review + + (tmp_path / "Challenge").mkdir() + (tmp_path / "Challenge" / "challenges.yml").write_text( + "challenges:\n" + " - slug: widget\n" + " entry_module: Challenge.Widget\n" + " statements:\n" + " - declaration: Challenge.Widget.widget_bound\n" + " informal: The answer exceeds 37.\n" + " definitions:\n" + " - declaration: Challenge.Widget.answer\n" + " informal: The answer.\n" + " solution:\n" + " module: Solution.Widget\n" + ) + files = [("Solution/Widget.lean", "added")] + + reason = solution_needs_llm_review(files, tmp_path) + + assert reason is not None + assert "definition hole" in reason + + +def test_render_comment_solution_mode() -> None: + """A solution review defers correctness to the comparator check.""" + from lean_pool.review import LLM_REVIEW_MARKER, render_comment + + body = render_comment( + { + "summary": "Proves the two-plus-two fixture by decide.", + "assessment": { + "touches_challenge_statement": False, + "definition_hole_risk": "none", + "proof_quality": 4, + "assessment_one_sentence": "One-line proof, nothing to flag.", + }, + "verdict": "approve", + "findings": [], + }, + model="gpt-5.5", + usage=None, + tier="flex", + reviewed_head_sha="deadbeef", + kind="solution", + ) + + assert body.startswith(LLM_REVIEW_MARKER) + assert "LLM review — challenge solution" in body + assert "Correctness is decided by" in body + assert "| Touches the challenge statement | ✅ no |" in body + assert "| Definition-hole risk | ✅ `none` |" in body + assert "SOLUTION_REVIEW_RULES.md" in body + assert "| Fit |" not in body + + +def test_render_solution_skip_comment_is_sticky_and_explains_itself() -> None: + """The skip note replaces the review and says what did the checking.""" + from lean_pool.review import LLM_REVIEW_MARKER, render_solution_skip_comment + + body = render_solution_skip_comment("deadbeef") + + assert body.startswith(LLM_REVIEW_MARKER) + assert "skipped" in body + assert "Correctness is decided by" in body + assert "deadbeef" in body + + +def test_render_comment_challenge_mode() -> None: + """A challenge review shows faithfulness, vacuity, and a size estimate.""" + from lean_pool.review import LLM_REVIEW_MARKER, render_comment + + body = render_comment( + { + "summary": "Adds the twin prime conjecture as an open statement.", + "assessment": { + "significance": "high", + "faithfulness": "faithful", + "faithfulness_note": "Set.Infinite over {p | p.Prime ∧ (p+2).Prime}.", + "source_match": "matches", + "vacuity_risk": "none", + "difficulty": "open_problem", + "estimated_lines": 25000, + "estimate_basis": "No known proof; Zhang-style machinery is absent.", + "already_formalized": "", + "assessment_one_sentence": "A correctly stated famous open problem.", + }, + "verdict": "approve", + "findings": [], + }, + model="gpt-5.5", + usage=None, + tier="flex", + reviewed_head_sha="deadbeef", + kind="challenge", + ) + + assert body.startswith(LLM_REVIEW_MARKER) + assert "LLM review — challenge" in body + assert "| Faithful to the prose | ✅ `faithful` |" in body + assert "| Vacuity risk | ✅ `none` |" in body + assert "~25,000 lines" in body + assert "Zhang-style machinery is absent" in body + assert "CHALLENGE_REVIEW_RULES.md" in body + # Project- and refactor-only fields must not leak into a challenge review. + assert "| Fit |" not in body + assert "| Brittleness |" not in body + + +def test_render_challenge_assessment_flags_existing_formalization() -> None: + """A challenge that duplicates existing work says so in the table.""" + from lean_pool.review import render_challenge_assessment + + table = render_challenge_assessment( + { + "assessment": { + "significance": "low", + "faithfulness": "mismatch", + "source_match": "unverifiable", + "vacuity_risk": "possible", + "difficulty": "exercise", + "estimated_lines": 40, + "already_formalized": "Nat.exists_infinite_primes", + } + } + ) + + assert "🛑 `mismatch`" in table + assert "🛑 `Nat.exists_infinite_primes`" in table + assert "~40 lines" in table + + def test_render_comment_refactor_mode() -> None: """A refactor review shows the tech-debt table and refactor rules link.""" from lean_pool.review import LLM_REVIEW_MARKER, render_comment diff --git a/python/tests/test_stats.py b/python/tests/test_stats.py index 555c8bed68..721cbf7020 100644 --- a/python/tests/test_stats.py +++ b/python/tests/test_stats.py @@ -11,6 +11,7 @@ apply_stats, collect_stats, count_lean_loc, + count_open_challenges, count_projects, main, render_stats, @@ -67,6 +68,28 @@ def test_collect_stats(tmp_path: Path) -> None: assert collect_stats(tmp_path) == Stats(projects=2, lines_of_lean=4) +def test_count_open_challenges(tmp_path: Path) -> None: + """Only unsolved challenges count toward the headline number.""" + registry = tmp_path / "challenges.yml" + registry.write_text( + "challenges:\n" + " - slug: open-one\n" + " status: open\n" + " - slug: done-one\n" + " status: solved\n" + ) + assert count_open_challenges(registry) == 1 + + +def test_render_stats_omits_an_empty_challenge_board() -> None: + """A repository with no open challenges says nothing about them.""" + rendered = render_stats(Stats(projects=2, lines_of_lean=4)) + assert "challenge" not in rendered + assert "open challenges" in render_stats( + Stats(projects=2, lines_of_lean=4, open_challenges=3) + ) + + def test_apply_stats_replaces_block() -> None: """Only the marked block is rewritten; surrounding text is kept.""" readme = "intro\n\nold\n\noutro\n" diff --git a/scripts/challenge/verify-solution.sh b/scripts/challenge/verify-solution.sh new file mode 100755 index 0000000000..cec5fe4aff --- /dev/null +++ b/scripts/challenge/verify-solution.sh @@ -0,0 +1,141 @@ +#!/usr/bin/env bash +# Verify a claimed solution to a Lean Pool challenge with `leanprover/comparator`. +# +# Comparator is a trustworthy judge: it replays the solution environment through +# the Lean kernel and checks that the theorems it claims really do prove the +# statements in the challenge module, using no axiom outside the permitted set. +# A green run here is what turns "I solved it" into a verified claim. +# +# scripts/challenge/verify-solution.sh [] +# +# The module defaults to the one the registry records for that challenge. It has +# to be importable from this workspace and must restate the challenge statement +# rather than import it — comparator exports the two environments separately and +# compares them. Everything comparator needs beyond that comes from +# `make comparator` (see CONTRIBUTING.md#challenge-mode). +# +# Options: +# --comparator PATH comparator binary (default: $COMPARATOR_BIN, then the +# `make comparator` cache directory) +# --lean4export PATH lean4export binary built at this project's toolchain +# --landrun PATH landrun sandbox binary +# --nanoda additionally replay through the nanoda kernel +# --insecure-no-sandbox +# run without landrun. Compiling a solution executes its +# code; only pass this for a solution you already trust. +set -euo pipefail + +repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)" +cache_dir="${XDG_CACHE_HOME:-$HOME/.cache}/lean-pool" +comparator_bin="${COMPARATOR_BIN:-$cache_dir/comparator/.lake/build/bin/comparator}" +lean4export_bin="${COMPARATOR_LEAN4EXPORT:-}" +landrun_bin="${COMPARATOR_LANDRUN:-}" +enable_nanoda=false +allow_no_sandbox=false + +usage() { + sed -n '3,25p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//' + exit "${1:-1}" +} + +positional=() +while [ $# -gt 0 ]; do + case "$1" in + --comparator) comparator_bin="$2"; shift 2 ;; + --lean4export) lean4export_bin="$2"; shift 2 ;; + --landrun) landrun_bin="$2"; shift 2 ;; + --nanoda) enable_nanoda=true; shift ;; + --insecure-no-sandbox) allow_no_sandbox=true; shift ;; + -h|--help) usage 0 ;; + -*) echo "Unknown option: $1" >&2; usage ;; + *) positional+=("$1"); shift ;; + esac +done + +if [ "${#positional[@]}" -lt 1 ] || [ "${#positional[@]}" -gt 2 ]; then + usage +fi +slug="${positional[0]}" +solution_module="" +if [ "${#positional[@]}" -eq 2 ]; then + solution_module="${positional[1]}" +fi + +if [ ! -x "$comparator_bin" ]; then + cat >&2 </dev/null 2>&1; then + lean4export_bin="$(command -v lean4export)" +fi +if [ -z "$lean4export_bin" ] || [ ! -x "$lean4export_bin" ]; then + cat >&2 </dev/null 2>&1; then + landrun_bin="$(command -v landrun)" +fi +if [ -z "$landrun_bin" ]; then + if [ "$allow_no_sandbox" = false ]; then + cat >&2 <&2 + exit 2 + fi + echo "warning: running without a sandbox; the solution's code will execute." >&2 +fi + +config="$(mktemp -t lean-pool-comparator)" +trap 'rm -f "$config"' EXIT + +# Plain string, not an array: bash 3.2 (macOS) treats an empty array as +# unbound under `set -u`, and `${var:+...}` expands to nothing when unset. +nanoda_flag="" +if [ "$enable_nanoda" = true ]; then + nanoda_flag="--enable-nanoda" +fi + +cd "$repo_root" +(cd python && uv run python -m lean_pool.challenge --repo .. config "$slug" \ + ${solution_module:+--solution-module "$solution_module"} --out "$config" \ + ${nanoda_flag:+"$nanoda_flag"}) >/dev/null + +echo "Comparator configuration:" +cat "$config" + +# Build only the challenge side: comparator builds the solution itself, inside +# the sandbox, and pre-compiling an untrusted solution here would defeat that. +echo "Building the challenge library..." +lake build Challenge + +echo "Running comparator..." +COMPARATOR_LANDRUN="$landrun_bin" COMPARATOR_LEAN4EXPORT="$lean4export_bin" \ + lake env "$comparator_bin" "$config" +echo "Verified: challenge '$slug' is proved by the solution comparator checked." diff --git a/scripts/ci/build-challenges.sh b/scripts/ci/build-challenges.sh new file mode 100755 index 0000000000..6e9fa352c1 --- /dev/null +++ b/scripts/ci/build-challenges.sh @@ -0,0 +1,31 @@ +#!/usr/bin/env bash +# Build the Challenge and Solution libraries and gate their warnings. +# +# Challenge statements are `sorry` by design, so Lean's "declaration uses +# `sorry`" notice is expected here — and only here. Every other warning fails +# the build exactly as it does for the pool, including anything from a +# solution, which is an ordinary sorry-free proof. Which declarations are +# allowed to be open is not decided here: `lean_pool.quality` checks each +# `sorry` against `Challenge/challenges.yml` and verifies via `#print axioms` +# that nothing else in either library rests on `sorryAx`. +set -euo pipefail + +lake="${LAKE:-$HOME/.elan/bin/lake}" +log="${RUNNER_TEMP:-/tmp}/challenge-build.log" + +"$lake" build Challenge Solution 2>&1 | tee "$log" + +# Both greps exit 1 on no match, and both no-matches are the clean case: a +# build with no warnings at all (an empty board), or one whose only warnings +# are the expected sorry notices. Under `set -o pipefail` an unguarded first +# stage would kill the script on the quietest possible build. +unexpected="$( + { grep -nE '(^|: )warning:' "$log" || true; } | + { grep -vE "declaration uses .sorry." || true; } +)" +if [ -n "$unexpected" ]; then + printf '%s\n' "$unexpected" + echo "::error::Challenge build emitted warnings beyond the expected sorry notices." + exit 1 +fi +echo "Challenge and Solution libraries built; only the expected sorry notices."