diff --git a/.github/CHALLENGE_REVIEW_RULES.md b/.github/CHALLENGE_REVIEW_RULES.md deleted file mode 100644 index ea6509e5f2..0000000000 --- a/.github/CHALLENGE_REVIEW_RULES.md +++ /dev/null @@ -1,160 +0,0 @@ -# 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 229de263a0..36c9ced71d 100644 --- a/.github/CODE_QUALITY.md +++ b/.github/CODE_QUALITY.md @@ -8,12 +8,11 @@ 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 --module --check` (all three library indexes must use `module` and `public import`) +- `lake exe mk_all --module --check` (the pool and project indexes must use `module` and `public import`) - `lake build LeanPool` - a warning scan over the build log -- [`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` +- `lake exe runLinter` on `LeanPool` +- `lake exe lint-style` on `LeanPool` - `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. @@ -60,28 +59,7 @@ 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) -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 -- a challenge card carries no lifecycle: no `status`, no solution pointer. A statement file must not change once merged, and the PR guard rejects a solution PR that edits one — so a card that moved with the status would make solving a challenge impossible (regenerate it and the guard refuses the PR; leave it stale and the card check refuses it). The solved state lives in the registry, on the answering module's card, and in `make challenges` -- `#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). +The checker also has `--write-project-cards` to regenerate entry-point module docstrings from `LeanPool/projects.yml`. ### 3. PR Separation @@ -92,15 +70,8 @@ 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. 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. +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 these checks before merge is future work. @@ -128,10 +99,6 @@ The rules applied depend on what the PR does: |---|---|---| | 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. @@ -143,7 +110,7 @@ Current behavior: - checks out the PR head - restores Lake caches and fetches Mathlib cache if needed -- profiles new and modified Lean files under `LeanPool/`, `Challenge/`, and `Solution/` +- profiles new and modified Lean files under `LeanPool/` - posts or updates a sticky PR comment - uploads the raw profile log as an artifact @@ -172,47 +139,12 @@ 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 in -[`scripts/challenge/pins.env`](../scripts/challenge/pins.env), which both this -workflow and `make comparator` read — so a local verification and a CI -verification run the same judge. They once did not, and the difference hid a -real failure: comparator's `main` resolves its tools from `COMPARATOR_*` -environment variables, while the pinned commit hardcodes `landrun` and -`lean4export` as PATH lookups, so passing paths worked locally and failed in -CI. The pins are: - -- `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 deleted file mode 100644 index 5e4d842c0c..0000000000 --- a/.github/SOLUTION_REVIEW_RULES.md +++ /dev/null @@ -1,94 +0,0 @@ -# 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 and cost.** 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. Compile cost matters too, and you - do not have to guess at it — the `/profile` comment on the PR reports - heartbeats and wall time for every added file. Cite it when a solution is - expensive enough that the pool would feel it on every build. A correct - proof can still be too slow, too large, or too messy to merge as it - stands. -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 deleted file mode 100644 index 04516ecf18..0000000000 --- a/.github/workflows/challenge-verify.yml +++ /dev/null @@ -1,196 +0,0 @@ -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: - # Deliberately not restricted to PRs targeting `main`. A solution lands - # wherever the work is happening — during a Lean/Mathlib bump, solution PRs - # stack on the bump branch — and whether a proof proves the challenge has - # nothing to do with which branch it is heading for. PR #301 (the first - # solution to the Odlyzko challenge) got no verification at all because it - # targeted `bump/v4.33.0-rc1`. - pull_request: - 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 - - -jobs: - verify: - runs-on: ubuntu-latest - name: Verify challenge solutions - steps: - - name: Checkout project - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd - - # `make comparator` reads the same file, so a local verification and a - # CI verification run the same judge. - - name: Load tool pins - run: cat scripts/challenge/pins.env | grep -E '^[A-Z0-9_]+=' >> "$GITHUB_ENV" - - - name: Restore Lean dependencies - id: dependency-cache - uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae - with: - path: | - ~/.elan - .lake/packages - key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} - - - name: Restore pool build - uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae - with: - path: .lake/build - key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} - restore-keys: | - LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- - - - name: Install Lean - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 - with: - auto-config: false - use-github-cache: false - use-mathlib-cache: false - - - name: Install uv - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff - with: - enable-cache: true - - - name: 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 }}-${{ - hashFiles('scripts/challenge/pins.env', '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" - - # lean4export reads the oleans this repository's build produced, so its - # version has to track `lean-toolchain`. That coupling is invisible in a - # commit pin: a version bump that forgets it fails later, inside an - # export, with an error about the file format rather than the pin. Say - # it here instead, with the replacement SHA already resolved. - - name: Check the lean4export pin matches the toolchain - run: | - set -euo pipefail - toolchain="$(cut -d: -f2 lean-toolchain)" - # Annotated tags need the `^{}` dereference to reach the commit; - # lightweight ones (what lean4export uses today) answer only the - # plain query. Ask for both rather than depend on which it is. - expected="$(git ls-remote https://github.com/leanprover/lean4export \ - "refs/tags/$toolchain^{}" | cut -f1)" - if [ -z "$expected" ]; then - expected="$(git ls-remote https://github.com/leanprover/lean4export \ - "refs/tags/$toolchain" | cut -f1)" - fi - if [ -z "$expected" ]; then - echo "::warning::lean4export has no $toolchain tag; leaving the pin alone." - exit 0 - fi - if [ "$expected" != "$LEAN4EXPORT_COMMIT" ]; then - echo "::error::LEAN4EXPORT_COMMIT is pinned to a lean4export that does" - echo "not match lean-toolchain ($toolchain). Comparator would fail" - echo "reading this repository's oleans. Set it in this workflow to:" - echo " LEAN4EXPORT_COMMIT: $expected" - exit 1 - fi - echo "lean4export pin matches $toolchain." - - - 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 - run: | - set -euo pipefail - # The pinned comparator hardcodes `landrun` and `lean4export` as - # PATH lookups — the COMPARATOR_* environment variables are a newer - # feature — so the binaries have to be *on PATH*, not merely passed. - export PATH="$PWD/.ci/lean4export/.lake/build/bin:$HOME/go/bin:$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 78d3f96cbc..ef0200a79f 100644 --- a/.github/workflows/content-pr-guard.yml +++ b/.github/workflows/content-pr-guard.yml @@ -1,40 +1,7 @@ name: PR Separation Guard -# PRs must not mix pooled formalization content with repository infrastructure. -# Content files are: -# - 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. -# -# Version-bump exemption: a Lean/Mathlib bump is inherently both content -# (LeanPool/**/*.lean API repairs) and infra (toolchain + manifest), and -# neither half builds without the other, so it cannot satisfy the split. A PR -# may therefore carry content alongside ONLY these bump files: -# - lean-toolchain -# - lake-manifest.json -# - lakefile.toml -# - docbuild/lean-toolchain -# - docbuild/lake-manifest.json -# - docbuild/lakefile.toml -# - scripts/challenge/pins.env -# - .github/workflows/content-pr-guard.yml -# (scripts/challenge/pins.env pins lean4export to this repository's -# toolchain, so a toolchain bump has to move it in the same PR.) -# Any other non-content file alongside content still fails the gate. +# Pooled Lean content and repository infrastructure must be reviewed separately. +# Lean/Mathlib version bumps may also include their Lake/toolchain metadata. on: pull_request: @@ -75,40 +42,12 @@ jobs: printf '%s\n' "$files" | sed 's/^/ /' echo - # 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_re='^(LeanPool\.lean|LeanPool/.+\.lean|LeanPool/projects\.yml)$' content="$(printf '%s\n' "$files" | { grep -E "$content_re" || true; })" non_content="$(printf '%s\n' "$files" | { grep -vE "$content_re" || true; })" if [ -n "$content" ] && [ -n "$non_content" ]; then - bump_metadata_re='^(lean-toolchain|lakefile\.toml|lake-manifest\.json|docbuild/(lean-toolchain|lakefile\.toml|lake-manifest\.json)|scripts/challenge/pins\.env|\.github/workflows/content-pr-guard\.yml)$' + bump_metadata_re='^(lean-toolchain|lakefile\.toml|lake-manifest\.json|docbuild/(lean-toolchain|lakefile\.toml|lake-manifest\.json)|\.github/workflows/content-pr-guard\.yml)$' non_bump_metadata="$(printf '%s\n' "$non_content" | { grep -vE "$bump_metadata_re" || true; })" bump_metadata="$(printf '%s\n' "$non_content" | { grep -E "$bump_metadata_re" || true; })" @@ -127,11 +66,6 @@ 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 @@ -142,7 +76,6 @@ jobs: echo " - docbuild/lean-toolchain" echo " - docbuild/lakefile.toml" echo " - docbuild/lake-manifest.json" - echo " - scripts/challenge/pins.env" echo echo "Content files in this PR:" while IFS= read -r f; do diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 43fad47bbc..b18dae1d6c 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -7,14 +7,12 @@ on: paths: - '**/*.lean' - 'LeanPool/projects.yml' - - 'Challenge/challenges.yml' - 'lakefile.toml' - 'lake-manifest.json' - 'lean-toolchain' - 'docbuild/**' - 'python/lean_pool/exposition/**' - 'python/lean_pool/quality.py' - - 'python/lean_pool/challenge.py' - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' - 'python/lean_pool/rebase_fastpath.py' @@ -32,14 +30,12 @@ on: - 'scripts/ci/**' - '**/*.lean' - 'LeanPool/projects.yml' - - 'Challenge/challenges.yml' - 'lakefile.toml' - 'lake-manifest.json' - 'lean-toolchain' - 'docbuild/**' - 'python/lean_pool/exposition/**' - 'python/lean_pool/quality.py' - - 'python/lean_pool/challenge.py' - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' - 'python/lean_pool/rebase_fastpath.py' @@ -500,14 +496,13 @@ jobs: # writes through one WAL database, so these targets intentionally share a # single job instead of unsafe parallel shards. - name: Build documentation data - run: cd docbuild && ~/.elan/bin/lake build LeanPool:docInfo Challenge:docInfo + run: cd docbuild && ~/.elan/bin/lake build LeanPool:docInfo - name: Validate pool documentation checkpoint run: | set -euo pipefail test -s docbuild/.lake/build/api-docs.db test -n "$(find docbuild/.lake/build/doc-data -type f -name 'LeanPool*.doc' -print -quit)" - test -n "$(find docbuild/.lake/build/doc-data -type f -name 'Challenge*.doc' -print -quit)" python3 - <<'PY' import sqlite3 @@ -533,21 +528,14 @@ jobs: .lake/packages/MD4Lean key: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ github.sha }} - # 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 - run: cd docbuild && ~/.elan/bin/lake build LeanPool:docs Challenge:docs + run: cd docbuild && ~/.elan/bin/lake build LeanPool:docs - name: Validate documentation site run: | set -euo pipefail test -s docbuild/.lake/build/doc/index.html test -s docbuild/.lake/build/doc/LeanPool.html - test -s docbuild/.lake/build/doc/Challenge.html test -s docbuild/.lake/build/doc/declarations/declaration-data.bmp - name: Remove cached exposition diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index a70d46cd1d..d05a622b0d 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -33,8 +33,6 @@ on: - 'lean-toolchain' - 'lake-manifest.json' - 'LeanPool/projects.yml' - - 'Challenge/challenges.yml' - - 'python/lean_pool/challenge.py' - 'python/lean_pool/quality.py' - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' @@ -62,8 +60,6 @@ on: - 'lean-toolchain' - 'lake-manifest.json' - 'LeanPool/projects.yml' - - 'Challenge/challenges.yml' - - 'python/lean_pool/challenge.py' - 'python/lean_pool/quality.py' - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' @@ -252,9 +248,6 @@ jobs: exit 1 fi - - name: Build challenges and solutions - run: ./scripts/ci/build-challenges.sh - # Publish once compilation succeeds, so docs can overlap the later # linters/quality checks without compiling the same PR a second time. - name: Package build for documentation @@ -289,14 +282,10 @@ jobs: cd python uv run python -m lean_pool.validation_cache lint --repo .. cd .. - ~/.elan/bin/lake exe runLinter Challenge - ~/.elan/bin/lake exe runLinter Solution - name: Text style lint 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: | @@ -530,9 +519,6 @@ jobs: exit 1 fi - - name: Build challenges and solutions - run: ./scripts/ci/build-challenges.sh - # Publish once compilation succeeds, so docs can overlap the later # linters/quality checks without compiling the same PR a second time. - name: Package build for documentation @@ -567,14 +553,10 @@ jobs: cd python uv run python -m lean_pool.validation_cache lint --repo .. cd .. - ~/.elan/bin/lake exe runLinter Challenge - ~/.elan/bin/lake exe runLinter Solution - name: Text style lint 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: | @@ -727,13 +709,8 @@ jobs: if: steps.project-build.outcome != 'success' run: | set -euo pipefail - ./scripts/ci/build-challenges.sh (cd python && uv run python -m lean_pool.validation_cache lint --repo ..) - ~/.elan/bin/lake exe runLinter Challenge - ~/.elan/bin/lake exe runLinter Solution ~/.elan/bin/lake exe lint-style LeanPool - ~/.elan/bin/lake exe lint-style Challenge - ~/.elan/bin/lake exe lint-style Solution (cd python && uv run python -m lean_pool.validation_cache quality --repo ..) - name: Package PR project build for later rebases diff --git a/.github/workflows/notice.yml b/.github/workflows/notice.yml index b24fa45c4c..08956468a5 100644 --- a/.github/workflows/notice.yml +++ b/.github/workflows/notice.yml @@ -12,7 +12,6 @@ on: # is an input below, so it cannot trigger a commit loop. paths: - 'LeanPool/**' - - 'Challenge/challenges.yml' - 'NOTICE.extra.yml' - 'python/lean_pool/notice.py' - 'python/lean_pool/stats.py' diff --git a/.github/workflows/proof-profile.yml b/.github/workflows/proof-profile.yml index 3653d41d6b..33cbcba1c8 100644 --- a/.github/workflows/proof-profile.yml +++ b/.github/workflows/proof-profile.yml @@ -174,18 +174,12 @@ jobs: CACHE_MATCHED: ${{ steps.lake-cache.outputs.cache-matched-key }} run: | set -euo pipefail - # Solutions are profiled for the same reason projects are: a - # green comparator run says a solution proves the challenge, not - # that it is a reasonable thing to keep building. Challenge - # statements are measured too — their proofs are `sorry`, but a - # statement resting on expensive definitions still costs the board - # something on every build. added=$(git diff --name-only --diff-filter=A "$BASE_SHA"...HEAD \ - -- LeanPool Challenge Solution \ + -- LeanPool \ | grep '\.lean$' \ | tr '\n' ' ' || true) modified=$(git diff --name-only --diff-filter=M "$BASE_SHA"...HEAD \ - -- LeanPool Challenge Solution \ + -- LeanPool \ | grep '\.lean$' \ | tr '\n' ' ' || true) files="${added}${modified}" diff --git a/AGENTS.md b/AGENTS.md index aa63011a62..20b87c50e3 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -9,13 +9,18 @@ This file is a concatenation of README.md and CONTRIBUTING.md. [![Lean Action CI](https://github.com/Vilin97/lean-pool/actions/workflows/lean_action_ci.yml/badge.svg)](https://github.com/Vilin97/lean-pool/actions/workflows/lean_action_ci.yml) [![Documentation](https://img.shields.io/badge/docs-online-blue)](https://vilin97.github.io/lean-pool/) [![Exposition](https://img.shields.io/badge/exposition-online-8a4fff)](https://vilin97.github.io/lean-pool/exposition/) +[![Zulip](https://img.shields.io/badge/Zulip-Lean_Pool-6492FE?logo=zulip&logoColor=white)](https://leanprover.zulipchat.com/#narrow/channel/619231-Lean-Pool) +[![Semantic Search](https://img.shields.io/badge/semantic_search-Octo-2f80ed)](https://octo.axiomatic-ai.com/search?scopes=repo%3AVilin97%2Flean-pool) [![License](https://img.shields.io/github/license/Vilin97/lean-pool)](LICENSE) [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.20513444.svg)](https://doi.org/10.5281/zenodo.20513444) +[![arXiv](https://img.shields.io/badge/arXiv-2609.25199-b31b1b)](https://arxiv.org/abs/2609.25199) Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at , and explore each project's dependency graph and declarations in the [exposition site](https://vilin97.github.io/lean-pool/exposition/). +Semantic search is also available via the [API](https://search.octo.axiomatic-ai.com/api/search). + -**159** formalization projects · **1,373,827** lines of Lean · **2** open challenges +**273** formalization projects · **5,801,081** lines of Lean (stats above are refreshed automatically by the [generated-metadata workflow](.github/workflows/notice.yml) — edit [`python/lean_pool/stats.py`](python/lean_pool/stats.py), not the numbers) @@ -37,25 +42,26 @@ 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. +To regenerate the preserved Zeta5 numerical certificates, see the +[certificate reproduction guide](scripts/zeta5-certificates/README.md). -```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`. +The [moving-sofa certificate recipe](python/lean_pool/sofa_certificates/README.md) +regenerates its optimized certificate modules from pinned public inputs. ### Contributing See [`CONTRIBUTING.md`](CONTRIBUTING.md). +The PR author or a maintainer can comment `/profile` to request an advisory +compile-cost report. Failed or zero-phase timed runs show unavailable timing +and are excluded from totals; errors and any successfully measured heartbeat +counts remain visible. + +Import PRs can be refreshed automatically after other projects merge. The +[rebase helper](python/lean_pool/rebase.py) resolves conflicts in the project registry +and generated index, preserving module headers and public imports when the index uses them. +Conflicts in proof files require a manual rebase. + ### Credits Created as part of the [UW Lean Hackathon](https://uw2026leanhackathon.github.io/) by [Vasily Ilin](https://github.com/Vilin97) and [Justin Asher](https://github.com/justincasher). @@ -67,6 +73,30 @@ Created as part of the [UW Lean Hackathon](https://uw2026leanhackathon.github.io - Lean Pool is not a unified library like mathlib. Most projects are independent of each other. - Lean Pool only accepts completed formalization projects. +[Palomar Registry](https://palomar-registry.org/) is also similar to Lean Pool. The differences are: +- Lean Pool maintains accepted projects. +- Lean Pool provides tools like search and documentation. +- Palomar is a registry, not a unified repository. + +Projects accepted to the Palomar Registry may be submitted to Lean Pool, and priority will be given to them. + +### Citation + +To cite Lean Pool, use the [paper](https://arxiv.org/abs/2609.25199): + +```bibtex +@misc{ilin2026leanpool, + title = {{Lean Pool}: An {AI}-Maintained Archive of Formalized Mathematics}, + author = {Vasily Ilin}, + year = {2026}, + eprint = {2609.25199}, + archivePrefix = {arXiv}, + primaryClass = {cs.AI}, + doi = {10.48550/arXiv.2609.25199}, + url = {https://arxiv.org/abs/2609.25199} +} +``` + # Contributing to Lean Pool Lean Pool welcomes serious, medium- to large-scale formalizations of mathematics and related disciplines (see [`MOTIVATION.md`](MOTIVATION.md)). Browse [`LeanPool/`](LeanPool/) for examples and [`candidates/CRITERIA.txt`](candidates/CRITERIA.txt) for what we include. @@ -80,45 +110,10 @@ If you would like to withdraw your project from Lean Pool, open an issue. There are two paths: - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt). -- **Open a content PR.** Add your project under `LeanPool//`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the index with `lake exe mk_all`. +- **Open a content PR.** Add your project under `LeanPool//`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the indexes with `lake exe mk_all`. Commit `LeanPool//Imports.lean`, which publicly imports every project source, and the single project import added to `LeanPool.lean`. 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. The challenge statement file is **not** touched by any of that: its card carries the contract (source, proposers, open declarations, the informal statement) and never the lifecycle, so solving a challenge leaves it byte-identical. 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. - -A green comparator run is necessary, not sufficient: a solution is still content entering the repository, so it gets the same `/profile` compile-cost comment as any other Lean change, and can be sent back for being too large, too messy, or too slow to build. 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/). @@ -134,20 +129,19 @@ 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`, `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). +- **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). - **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`, `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). +**Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `lake exe runLinter` and `lake exe lint-style` on `LeanPool`, 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). **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 148465b152..20b87c50e3 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -9,19 +9,26 @@ This file is a concatenation of README.md and CONTRIBUTING.md. [![Lean Action CI](https://github.com/Vilin97/lean-pool/actions/workflows/lean_action_ci.yml/badge.svg)](https://github.com/Vilin97/lean-pool/actions/workflows/lean_action_ci.yml) [![Documentation](https://img.shields.io/badge/docs-online-blue)](https://vilin97.github.io/lean-pool/) [![Exposition](https://img.shields.io/badge/exposition-online-8a4fff)](https://vilin97.github.io/lean-pool/exposition/) +[![Zulip](https://img.shields.io/badge/Zulip-Lean_Pool-6492FE?logo=zulip&logoColor=white)](https://leanprover.zulipchat.com/#narrow/channel/619231-Lean-Pool) +[![Semantic Search](https://img.shields.io/badge/semantic_search-Octo-2f80ed)](https://octo.axiomatic-ai.com/search?scopes=repo%3AVilin97%2Flean-pool) [![License](https://img.shields.io/github/license/Vilin97/lean-pool)](LICENSE) [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.20513444.svg)](https://doi.org/10.5281/zenodo.20513444) +[![arXiv](https://img.shields.io/badge/arXiv-2609.25199-b31b1b)](https://arxiv.org/abs/2609.25199) Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at , and explore each project's dependency graph and declarations in the [exposition site](https://vilin97.github.io/lean-pool/exposition/). +Semantic search is also available via the [API](https://search.octo.axiomatic-ai.com/api/search). + -**159** formalization projects · **1,373,827** lines of Lean · **2** open challenges +**273** formalization projects · **5,801,081** lines of Lean (stats above are refreshed automatically by the [generated-metadata workflow](.github/workflows/notice.yml) — edit [`python/lean_pool/stats.py`](python/lean_pool/stats.py), not the numbers) So far, projects have been added by hand: each is a suitable, permissively licensed (Apache-2.0 or MIT) Lean repository, bumped to the latest Lean and Mathlib, made to pass [CI](.github/workflows/lean_action_ci.yml) — it builds warning-free and clears Mathlib's linters, the style checker, and the repository quality gates (no `sorry`/`admit`, no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, no `unsafe`/`partial`, file headers, size limits) — and an [LLM review](.github/REVIEW_RULES.md) of fit and significance, then merged. +LLM reviews use GPT-6-Astra at `xhigh` reasoning effort through a privately operated Codex worker, without paid OpenAI API requests or an API fallback. Reviews also show an estimated dollar cost at official Standard API token rates, labeled separately from Codex quota billing. See [review operations](python/review-operations.md) for deployment and diagnostics. + Project PRs also receive an advisory Greptile review, configured in [`.greptile/`](.greptile/), for cross-file integration, reusable abstractions, completeness, maintainability, and measured cost. It supplements rather than replaces the independent LLM verdict. ### Getting started @@ -35,25 +42,26 @@ 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. +To regenerate the preserved Zeta5 numerical certificates, see the +[certificate reproduction guide](scripts/zeta5-certificates/README.md). -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`. +The [moving-sofa certificate recipe](python/lean_pool/sofa_certificates/README.md) +regenerates its optimized certificate modules from pinned public inputs. ### Contributing See [`CONTRIBUTING.md`](CONTRIBUTING.md). +The PR author or a maintainer can comment `/profile` to request an advisory +compile-cost report. Failed or zero-phase timed runs show unavailable timing +and are excluded from totals; errors and any successfully measured heartbeat +counts remain visible. + +Import PRs can be refreshed automatically after other projects merge. The +[rebase helper](python/lean_pool/rebase.py) resolves conflicts in the project registry +and generated index, preserving module headers and public imports when the index uses them. +Conflicts in proof files require a manual rebase. + ### Credits Created as part of the [UW Lean Hackathon](https://uw2026leanhackathon.github.io/) by [Vasily Ilin](https://github.com/Vilin97) and [Justin Asher](https://github.com/justincasher). @@ -65,6 +73,30 @@ Created as part of the [UW Lean Hackathon](https://uw2026leanhackathon.github.io - Lean Pool is not a unified library like mathlib. Most projects are independent of each other. - Lean Pool only accepts completed formalization projects. +[Palomar Registry](https://palomar-registry.org/) is also similar to Lean Pool. The differences are: +- Lean Pool maintains accepted projects. +- Lean Pool provides tools like search and documentation. +- Palomar is a registry, not a unified repository. + +Projects accepted to the Palomar Registry may be submitted to Lean Pool, and priority will be given to them. + +### Citation + +To cite Lean Pool, use the [paper](https://arxiv.org/abs/2609.25199): + +```bibtex +@misc{ilin2026leanpool, + title = {{Lean Pool}: An {AI}-Maintained Archive of Formalized Mathematics}, + author = {Vasily Ilin}, + year = {2026}, + eprint = {2609.25199}, + archivePrefix = {arXiv}, + primaryClass = {cs.AI}, + doi = {10.48550/arXiv.2609.25199}, + url = {https://arxiv.org/abs/2609.25199} +} +``` + # Contributing to Lean Pool Lean Pool welcomes serious, medium- to large-scale formalizations of mathematics and related disciplines (see [`MOTIVATION.md`](MOTIVATION.md)). Browse [`LeanPool/`](LeanPool/) for examples and [`candidates/CRITERIA.txt`](candidates/CRITERIA.txt) for what we include. @@ -78,45 +110,10 @@ If you would like to withdraw your project from Lean Pool, open an issue. There are two paths: - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt). -- **Open a content PR.** Add your project under `LeanPool//`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the index with `lake exe mk_all`. +- **Open a content PR.** Add your project under `LeanPool//`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the indexes with `lake exe mk_all`. Commit `LeanPool//Imports.lean`, which publicly imports every project source, and the single project import added to `LeanPool.lean`. 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. The challenge statement file is **not** touched by any of that: its card carries the contract (source, proposers, open declarations, the informal statement) and never the lifecycle, so solving a challenge leaves it byte-identical. 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. - -A green comparator run is necessary, not sufficient: a solution is still content entering the repository, so it gets the same `/profile` compile-cost comment as any other Lean change, and can be sent back for being too large, too messy, or too slow to build. 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/). @@ -132,20 +129,19 @@ 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`, `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). +- **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). - **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`, `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). +**Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `lake exe runLinter` and `lake exe lint-style` on `LeanPool`, 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). **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 8a401dcf3e..6a9a282d86 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -15,41 +15,6 @@ 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. The challenge statement file is **not** touched by any of that: its card carries the contract (source, proposers, open declarations, the informal statement) and never the lifecycle, so solving a challenge leaves it byte-identical. 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. - -A green comparator run is necessary, not sufficient: a solution is still content entering the repository, so it gets the same `/profile` compile-cost comment as any other Lean change, and can be sent back for being too large, too messy, or too slow to build. 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/). @@ -65,20 +30,19 @@ 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`, `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). +- **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). - **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`, `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). +**Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `lake exe runLinter` and `lake exe lint-style` on `LeanPool`, 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). **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`. diff --git a/Challenge/README.md b/Challenge/README.md deleted file mode 100644 index 1025a8f457..0000000000 --- a/Challenge/README.md +++ /dev/null @@ -1,18 +0,0 @@ -# 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 75fb3e4f6e..8aebb6d158 100644 --- a/Makefile +++ b/Makefile @@ -1,17 +1,8 @@ -.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 +.PHONY: build build-project setup lint lint-fix check test docs update agent-docs # 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 @@ -30,8 +21,6 @@ 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 @@ -52,38 +41,6 @@ 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 fetch --quiet origin && \ - git checkout --quiet $$(. $(CURDIR)/scripts/challenge/pins.env && echo $$COMPARATOR_COMMIT) && \ - lake build comparator - @test -d $(COMPARATOR_CACHE)/lean4export || \ - git clone https://github.com/leanprover/lean4export $(COMPARATOR_CACHE)/lean4export - cd $(COMPARATOR_CACHE)/lean4export && git fetch --quiet origin && \ - git checkout --quiet $$(. $(CURDIR)/scripts/challenge/pins.env && echo $$LEAN4EXPORT_COMMIT) && \ - 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 fc1f378eb7..fa8f6493b0 100644 --- a/README.md +++ b/README.md @@ -18,7 +18,7 @@ Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathl Semantic search is also available via the [API](https://search.octo.axiomatic-ai.com/api/search). -**273** formalization projects · **5,801,081** lines of Lean · **3** open challenges +**273** formalization projects · **5,801,081** lines of Lean (stats above are refreshed automatically by the [generated-metadata workflow](.github/workflows/notice.yml) — edit [`python/lean_pool/stats.py`](python/lean_pool/stats.py), not the numbers) @@ -46,21 +46,6 @@ To regenerate the preserved Zeta5 numerical certificates, see the The [moving-sofa certificate recipe](python/lean_pool/sofa_certificates/README.md) regenerates its optimized certificate modules from pinned public inputs. -### 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/README.md b/Solution/README.md deleted file mode 100644 index f0e1b49156..0000000000 --- a/Solution/README.md +++ /dev/null @@ -1,17 +0,0 @@ -# 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 9920af1daa..a260cee58d 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,7 +1,7 @@ name = "lean-pool" version = "0.1.0" keywords = ["math"] -defaultTargets = ["LeanPool", "Challenge", "Solution"] +defaultTargets = ["LeanPool"] requiresModuleSystem = true [leanOptions] @@ -18,19 +18,6 @@ rev = "v4.35.0-rc3" [[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" - [[lean_exe]] name = "mk_all" root = "ProjectIndexes" diff --git a/python/ci-performance.md b/python/ci-performance.md index 5b60c20c55..16e754f387 100644 --- a/python/ci-performance.md +++ b/python/ci-performance.md @@ -86,7 +86,7 @@ lint, axiom audits and option-backdoor audits import all owned modules; each compiled declaration is checked in its owning unit. Registry declarations use separate per-entry receipts. Static checks (registry/card consistency, reachability, forbidden constructs, size limits and Lake options), text style -lint, and Challenge/Solution validation still run every time. +and lint still run every time. `.lake/validation-cache/v1/passes.json` contains successful receipts keyed by source contents, each module's transitive compiler import inventory, toolchain, diff --git a/python/lean_pool/challenge.py b/python/lean_pool/challenge.py deleted file mode 100644 index e467fb8d27..0000000000 --- a/python/lean_pool/challenge.py +++ /dev/null @@ -1,787 +0,0 @@ -"""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. - - It deliberately carries none of the challenge's *lifecycle* — no - status, no solution pointer. Those live in the registry, because a - statement file must not change once merged: it is the text every - solution is judged against, and the PR guard rejects a solution PR - that edits it. Putting `status: solved` in the card would have made - solving a challenge impossible — regenerate the card and the guard - refuses the PR, leave it stale and the card check refuses it. The - solved state is recorded in `challenges.yml`, on the answering module's - own card, and by `make challenges`. - """ - lines = [f"# {challenge['title']}", ""] - fields = [ - ("Source", _format_source(challenge["source"])), - ("Proposed by", _join(challenge["proposers"])), - ("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")) - 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/indexes.py b/python/lean_pool/indexes.py index 66c7459182..afc679fe60 100644 --- a/python/lean_pool/indexes.py +++ b/python/lean_pool/indexes.py @@ -127,7 +127,7 @@ def _write_indexes(contents: dict[Path, str], *, check: bool) -> int: def _library_index(root: Path, library: str, *, use_module: bool) -> str: - """Keep the ordinary flat indexes for Challenge and Solution unchanged.""" + """Render a flat pool index for repositories without project roots.""" existing = root / f"{library}.lean" source = existing.read_text(encoding="utf-8") if existing.exists() else "" module_style = use_module or code_view(source).lstrip().startswith("module") @@ -148,19 +148,17 @@ def main(argv: list[str] | None = None) -> int: parser.add_argument("--check", action="store_true") parser.add_argument("--module", action="store_true") parser.add_argument("--project-roots", action="store_true") - parser.add_argument("--lib", choices=("LeanPool", "Challenge", "Solution")) + parser.add_argument("--lib", choices=("LeanPool",)) args = parser.parse_args(argv) root = args.repo.resolve() - contents = {} - for library in [args.lib] if args.lib else ["LeanPool", "Challenge", "Solution"]: - if library == "LeanPool" and ( - args.project_roots or requires_project_roots(root) - ): - contents.update(render_project_indexes(root)) - else: - contents[root / f"{library}.lean"] = _library_index( - root, library, use_module=args.module + if args.project_roots or requires_project_roots(root): + contents = render_project_indexes(root) + else: + contents = { + root / "LeanPool.lean": _library_index( + root, "LeanPool", use_module=args.module ) + } try: return _write_indexes(contents, check=args.check) except ValueError as error: diff --git a/python/lean_pool/prior_art.py b/python/lean_pool/prior_art.py index a64fadbc01..3b7b178c84 100644 --- a/python/lean_pool/prior_art.py +++ b/python/lean_pool/prior_art.py @@ -117,7 +117,7 @@ def _claims_of(entry: dict, results_key: str) -> list[Claim]: return claims -def new_claims(head_text: str, base_text: str, kind: str) -> list[Claim]: +def new_claims(head_text: str, base_text: str) -> list[Claim]: """Return the headlines this PR adds that were not there before. Only *new* entries are searched. A refactor or a bump touches cards @@ -127,17 +127,11 @@ def new_claims(head_text: str, base_text: str, kind: str) -> list[Claim]: Args: head_text: The registry file as of the PR head. base_text: The same file on the base branch. - kind: ``"project"`` (``projects.yml``) or ``"challenge"`` - (``challenges.yml``), which differ only in their keys. Returns: Up to :data:`MAX_CLAIMS` claims, in registry order. """ - list_key, results_key = ( - ("projects", "main_results") - if kind == "project" - else ("challenges", "statements") - ) + list_key, results_key = "projects", "main_results" known = { claim.declaration for entry in _entries(base_text, list_key) diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index a99abfda09..cb06a211f0 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -1,17 +1,4 @@ -"""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``. -""" +"""Deterministic repository quality checks for completed Lean Pool formalizations.""" from __future__ import annotations @@ -26,16 +13,10 @@ import yaml -from lean_pool import challenge from lean_pool.indexes import requires_project_roots, structure_errors from lean_pool.validation_cache import ValidationCache, pool_units -# 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" +ALLOWED_AXIOMS = {"propext", "Quot.sound", "Classical.choice"} CODE_QUALITY_URL = ( "https://github.com/Vilin97/lean-pool/blob/main/.github/CODE_QUALITY.md" ) @@ -109,16 +90,6 @@ 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 @@ -217,28 +188,9 @@ 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", - } + """Return the generated pool library index.""" + return {root / "LeanPool.lean"} def _module_to_path(root: Path, module: str) -> Path: @@ -277,16 +229,7 @@ def _reachable_leanpool_files(root: Path, entry_module: str = "LeanPool") -> set def _check_reachability(root: Path) -> list[_QualityError]: - 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 + return _unreachable_errors(root, "LeanPool", _lean_content_files(root)) def _unreachable_errors( @@ -303,7 +246,7 @@ def _unreachable_errors( def _check_headers(root: Path) -> list[_QualityError]: errors: list[_QualityError] = [] generated = _generated_index_files(root) - for path in _all_lean_files(root): + for path in _lean_content_files(root): if path in generated: continue text = path.read_text() @@ -322,24 +265,15 @@ 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): - 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 + """Scan completed formalizations for forbidden tokens.""" + return [ + error + for path in _lean_content_files(root) + for error in _forbidden_text_errors(path) + ] -def _forbidden_text_errors(path: Path, *, allow_sorry: bool) -> list[_QualityError]: +def _forbidden_text_errors(path: Path) -> list[_QualityError]: errors: list[_QualityError] = [] stripped = _strip_lean_comments(path.read_text()) for line_number, line in enumerate(stripped.splitlines(), start=1): @@ -369,7 +303,7 @@ def _forbidden_text_errors(path: Path, *, allow_sorry: bool) -> list[_QualityErr errors.append( _QualityError(path, line_number, "broad import Mathlib is forbidden") ) - errors.extend(_sorry_errors(path, line_number, line, allow_sorry=allow_sorry)) + errors.extend(_sorry_errors(path, line_number, line)) if FORBIDDEN_SOUNDNESS.search(line): errors.append( _QualityError(path, line_number, "unchecked declaration is forbidden") @@ -381,36 +315,11 @@ def _forbidden_text_errors(path: Path, *, allow_sorry: bool) -> list[_QualityErr 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", - ) - ] +def _sorry_errors(path: Path, line_number: int, line: str) -> list[_QualityError]: + """Reject unproved terms in comment-stripped source.""" + for token in ("admit", "sorry"): + if re.search(rf"\b{token}\b", line): + return [_QualityError(path, line_number, f"{token} is forbidden")] return [] @@ -464,12 +373,7 @@ 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 + return _file_size_errors(_lean_content_files(root), POOL_CODE_LINE_LIMIT) def _file_size_errors(paths: list[Path], limit: int) -> list[_QualityError]: @@ -496,7 +400,7 @@ def _declaration_starts(stripped: str) -> list[tuple[int, str]]: def _check_proof_sizes(root: Path) -> list[_QualityError]: errors: list[_QualityError] = [] - for path in _all_lean_files(root): + for path in _lean_content_files(root): original_lines = path.read_text().splitlines() stripped = _strip_lean_comments("\n".join(original_lines)) starts = _declaration_starts(stripped) @@ -729,27 +633,11 @@ def main (args : List String) : IO UInt32 := do LeanPoolQuality.OptionAudit.auditEnv env (modules.map (·.getRoot)) onlyModules 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 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 + """Audit every compiled pool declaration for backdoors.""" + return _run_option_audit(root, ["LeanPool"]) def _run_option_audit( @@ -789,60 +677,21 @@ def _run_option_audit( 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, - open_declarations: set[str] | None = None, index_path: Path | None = None, ) -> list[_QualityError]: - """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() + """Turn all environment-audit findings and non-completion into errors.""" 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), @@ -865,53 +714,13 @@ def _parse_option_audit_output( def _check_axioms(root: Path) -> list[_QualityError]: """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(), - ) + return _audit_axioms(root, _parse_declarations(root), "LeanPool") def _audit_axioms( root: Path, declarations: list[_Declaration], import_module: str | list[str], - open_declarations: set[str], ) -> list[_QualityError]: """Run `#print axioms` over ``declarations`` and grade the results.""" if not declarations: @@ -949,7 +758,7 @@ def _audit_axioms( finally: temp_path.unlink(missing_ok=True) - errors = _parse_axiom_output(root, declarations, process.stdout, open_declarations) + errors = _parse_axiom_output(root, declarations, process.stdout) resolved = _axiom_audit_resolved(process.stdout) missing = [ declaration for declaration in declarations if declaration.name not in resolved @@ -974,84 +783,38 @@ 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( {f"_root_.{declaration.name}": declaration for declaration in declarations} ) # Names may contain `'` (e.g. `foo'`); see _axiom_audit_resolved comment. - pattern = re.compile(r"^'(.+?)' depends on axioms: \[(.*)\]$", re.MULTILINE) - seen: set[str] = set() + pattern = re.compile(r"^'(.+?)' depends on axioms: \[([^\]]*)\]", re.MULTILINE) 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()} - 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 - ) + errors.extend(_axiom_errors(declaration, name, axioms)) 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 + declaration: _Declaration, name: str, axioms: set[str] ) -> 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)}", - ) + """Grade one declaration's axiom set without proof-hole exceptions.""" + extra_axioms = sorted(axioms - ALLOWED_AXIOMS) + if not extra_axioms: + return [] + return [ + _QualityError( + declaration.path, + declaration.line, + f"{name} depends on unallowlisted axioms: {', '.join(extra_axioms)}", ) - return errors + ] def _axiom_audit_resolved(stdout: str) -> set[str]: @@ -1548,211 +1311,6 @@ def _card_is_current(text: str, expected: str) -> bool: 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 @@ -1806,32 +1364,12 @@ 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 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 + # h1 heading and which contains a `Source:` line. Matching on that key # 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|Challenge):[^\n]+\n" + r"/-!\s*\n#\s+[^\n]+\n(?:[^\n]*\n)*?Source:[^\n]+\n" r"(?:[^\n]*\n)*?-/\n*", re.MULTILINE, ) @@ -1908,7 +1446,6 @@ def run_checks( _check_style_nolints, _check_file_sizes, _check_proof_sizes, - _check_challenges, ] errors = [error for check in checks for error in check(root)] errors.extend( @@ -1922,11 +1459,6 @@ def run_checks( errors.extend(_check_option_backdoors(root)) else: errors.extend(_cached_pool_audits(root, validation_cache)) - for library in (challenge.LIBRARY_NAME, challenge.SOLUTION_LIBRARY_NAME): - if (root / f"{library}.lean").exists(): - errors.extend(_run_option_audit(root, [library])) - errors.extend(_check_challenge_axioms(root)) - errors.extend(_check_solution_axioms(root)) return sorted( errors, key=lambda error: (str(error.path), error.line, error.message) ) @@ -1941,7 +1473,7 @@ def _cached_pool_audits(root: Path, cache: ValidationCache) -> list[_QualityErro cache.check( "axioms", modules, - lambda: _audit_axioms(root, _declarations_in(paths), modules, set()), + lambda: _audit_axioms(root, _declarations_in(paths), modules), ) ) errors.extend( @@ -1979,11 +1511,6 @@ 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) @@ -1993,8 +1520,6 @@ 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, diff --git a/python/lean_pool/review.py b/python/lean_pool/review.py index 5457069cf1..fc9a381363 100644 --- a/python/lean_pool/review.py +++ b/python/lean_pool/review.py @@ -12,17 +12,7 @@ - **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 and the PR's own title and description via the GitHub CLI, asks the configured OpenAI model to evaluate the @@ -93,15 +83,13 @@ from openai import APIStatusError, BadRequestError, OpenAI, RateLimitError -from lean_pool import challenge, codex_review, prior_art, review_portions +from lean_pool import codex_review, prior_art, review_portions logger = logging.getLogger(__name__) 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" # Reviews default to the authenticated Codex account pool on the Azure VM. DEFAULT_MODEL = "gpt-6-astra" # Preserve the existing review depth. @@ -110,13 +98,7 @@ # and xhigh reasoning stretches generation further. 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." -) + # Per-call input ceiling, including instructions, PR context, and evidence. # Source portions shrink on a context rejection; source is never discarded. @@ -203,8 +185,12 @@ def pricing_rates( RULES_DOC_NAME = { "project": "REVIEW_RULES.md", "refactor": "REFACTOR_REVIEW_RULES.md", - "challenge": "CHALLENGE_REVIEW_RULES.md", - "solution": "SOLUTION_REVIEW_RULES.md", +} +SOURCE_MATCH_ICON = { + "matches": "✅", + "mismatch": "🛑", + "unverifiable": "🟡", + "not_a_known_result": "➖", } FIT_ICON = { "good_fit": "✅", @@ -235,22 +221,7 @@ def pricing_rates( "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_REFACTOR = dedent( """\ @@ -282,82 +253,7 @@ def pricing_rates( ) -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. - """ -) - - -# Appended to every system prompt. The first challenge review (PR #289) -# came back with the mathematics unreadable: `over ^R09` for `over ℚ`, -# `|(discr K : ^])| ^U 8.25 ^ finrank ^R0a K` for -# `|(discr K : ℝ)| ≥ 8.25 ^ finrank ℚ K`. The mangling is the model's own — -# nothing between `json.loads` and the posted comment touches those -# strings — and it is not a systematic escape (`ℚ` came out as both `^R0a` -# and `^R09`), so it cannot be decoded after the fact. Ask for the -# characters directly, with a graceful fallback to words, since a review of -# Lean that cannot render `ℚ` or `≥` is worth much less in this repository. +# Keep quoted Lean notation readable in every review mode. NOTATION_RULE = dedent( """\ Notation: when you quote Lean, copy the characters exactly as they @@ -394,8 +290,6 @@ def pricing_rates( # PROJECT_RUBRICS) rather than in one monolithic call. REVIEW_MODES: dict[str, tuple[Path, str]] = { "refactor": (REFACTOR_RULES_PATH, SYSTEM_PROMPT_REFACTOR), - "challenge": (CHALLENGE_RULES_PATH, SYSTEM_PROMPT_CHALLENGE), - "solution": (SOLUTION_RULES_PATH, SYSTEM_PROMPT_SOLUTION), } RUBRICS_DIR = REPO_ROOT / ".github" / "review-rubrics" @@ -666,55 +560,11 @@ 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 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. - - ``"infra"`` — touches Lean somewhere outside the three content trees - (tooling under ``scripts/``, for instance). There is no - contribution to judge, so no model is called. - - 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. A PR that touches no Lean in any of the three - content trees is ``"infra"``; anything left is ``"project"``. - """ + """Choose project review for new projects, refactor review for existing ones.""" 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) @@ -722,87 +572,20 @@ def classify_pr(files: list[tuple[str, str]]) -> str: continue if status == "added": added_projects.add(project) - else: # modified / removed / renamed / changed / copied + else: 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" - if not touches_reviewable_content(files): + if not added_projects and not existing_projects: return "infra" - return "project" + return "project" if added_projects - existing_projects else "refactor" def touches_reviewable_content(files: list[tuple[str, str]]) -> bool: - """Whether the PR changes Lean content any review mode is about. - - A ``.lean`` file under ``scripts/`` is tooling, not mathematics, but - it is enough to clear the workflow's "does this PR touch Lean?" filter - — so exposition and CI PRs used to arrive at the project rules and be - graded for mathematical fit. PRs #279 and #282 came back `not_a_fit` / - `undergraduate` and merged anyway; PR #283, the next increment of the - same pipeline, came back `good_fit` / `graduate` / `approve` over a - summary that opened "This is not a mathematics contribution." - """ + """Whether the PR changes Lean source belonging to a pooled project.""" return any( - name.endswith(".lean") - and ( - project_of(name) is not None - or is_challenge_statement(name) - or is_solution_file(name) - ) - for name, _ in files + name.endswith(".lean") and project_of(name) is not None for name, _ in files ) -# 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. @@ -1588,47 +1371,6 @@ 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", _prior_art_cell(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: @@ -1651,37 +1393,6 @@ def _prior_art_cell(value: str) -> str: return f"🛑 `{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 - - RUBRIC_VERDICT_ICON = {"pass": "✅", "block": "🛑", "discuss": "🤔"} @@ -1928,7 +1639,7 @@ def render_comment( """Render the model's payload as a Markdown PR comment body. ``kind`` is ``"project"`` (fit/significance review), ``"refactor"`` - (tech-debt review), or ``"challenge"`` (open-statement review); it + (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. @@ -1939,13 +1650,9 @@ def render_comment( 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}`", ""]) @@ -1988,8 +1695,6 @@ def render_comment( renderers = { "refactor": render_refactor_assessment, - "challenge": render_challenge_assessment, - "solution": render_solution_assessment, } assessment = renderers.get(kind, lambda _payload: "")(payload) if assessment: @@ -2032,40 +1737,6 @@ 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 fetch_file_at(path: str, ref: str, repo_full_name: str) -> str: """Return the contents of ``path`` at ``ref``, or ``""`` if absent. @@ -2092,16 +1763,13 @@ def fetch_file_at(path: str, ref: str, repo_full_name: str) -> str: def gather_prior_art(kind: str, head_sha: str, repo_full_name: str) -> str | None: """Search Mathlib and the pool for what this PR claims is new. - Only project and challenge PRs put a new headline on the board; - refactors and solutions re-open a question that was settled when the - thing they touch was merged. A search that cannot run degrades to a + Only project PRs add new headlines; refactors change projects whose + prior art was settled when they merged. A search that cannot run degrades to a note saying so — never to a failed review. """ - if kind not in ("project", "challenge"): + if kind != "project": return None - registry = ( - "LeanPool/projects.yml" if kind == "project" else "Challenge/challenges.yml" - ) + registry = "LeanPool/projects.yml" head_text = fetch_file_at(registry, head_sha, repo_full_name) base_text = (REPO_ROOT / registry).read_text(encoding="utf-8") if not head_text.strip(): @@ -2112,7 +1780,7 @@ def gather_prior_art(kind: str, head_sha: str, repo_full_name: str) -> str | Non print(f"Mathlib prior-art search skipped: {unreadable}", file=sys.stderr) projects = (REPO_ROOT / "LeanPool" / "projects.yml").read_text(encoding="utf-8") return prior_art.render([], {}, projects, unreadable) - claims = prior_art.new_claims(head_text, base_text, kind) + claims = prior_art.new_claims(head_text, base_text) hits, unavailable = prior_art.search_mathlib(claims) if unavailable is not None: print(f"Mathlib prior-art search skipped: {unavailable}", file=sys.stderr) @@ -2127,8 +1795,8 @@ def gather_prior_art(kind: str, head_sha: str, repo_full_name: str) -> str | Non def render_infra_skip_comment(reviewed_head_sha: str) -> str: """Render the comment posted instead of reviewing a non-content PR. - A PR whose only Lean is tooling has no project, challenge, or - solution in it, and grading it for mathematical fit produces a verdict + A PR whose only Lean is tooling has no project in it, and grading it + for mathematical fit produces a verdict about a contribution that was never made. """ return "\n".join( @@ -2138,9 +1806,9 @@ def render_infra_skip_comment(reviewed_head_sha: str) -> str: "", f"**Reviewed head:** `{reviewed_head_sha}`" if reviewed_head_sha else "", "", - "No model review: this PR changes Lean only outside `LeanPool/`, " - "`Challenge/`, and `Solution/`, so there is no project, challenge, " - "or solution here to judge. The build, linters, and quality gates " + "No model review: this PR changes no pooled project Lean source, " + "so there is no project here to judge. The build, linters, " + "and quality gates " "still apply as usual.", "", "---", @@ -2225,9 +1893,7 @@ def main() -> int: effort = None repo_full_name = resolve_repo_full_name().strip() - # 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. + # Select the rules for a new project or a refactor of existing content. files = fetch_pr_files(pr_number, repo_full_name) kind = classify_pr(files) print(f"Reviewing PR #{pr_number} as a {kind} PR.", file=sys.stderr) @@ -2239,7 +1905,7 @@ def main() -> int: if kind == "infra": print( - "PR touches no Lean under LeanPool/, Challenge/, or Solution/; " + "PR touches no pooled project Lean source; " "posting the skip note instead of calling the model.", file=sys.stderr, ) @@ -2250,22 +1916,6 @@ def main() -> int: ) return 0 - 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) - _check_review_head(pr_number, repo_full_name, reviewed_head_sha) diff = fetch_diff(pr_number, repo_full_name) _check_review_head(pr_number, repo_full_name, reviewed_head_sha) diff --git a/python/lean_pool/review_portions.py b/python/lean_pool/review_portions.py index 76ef952c0b..af0d576ba2 100644 --- a/python/lean_pool/review_portions.py +++ b/python/lean_pool/review_portions.py @@ -87,7 +87,7 @@ def shared_context(diff: str, character_budget: int) -> str: for chunk in chunks: header = chunk.split("\n", 1)[0] if not re.search( - r" b/(?:LeanPool|Challenge|Solution)/(?:[^/]+\.lean|[^/]+\.yml)$", + r" b/LeanPool/(?:[^/]+\.lean|[^/]+\.yml)$", header, ): continue diff --git a/python/lean_pool/stats.py b/python/lean_pool/stats.py index 9deaae4985..3fb906d5e2 100644 --- a/python/lean_pool/stats.py +++ b/python/lean_pool/stats.py @@ -47,7 +47,6 @@ class Stats: projects: int lines_of_lean: int - open_challenges: int = 0 def count_projects(projects_yml_path: Path) -> int: @@ -98,37 +97,11 @@ 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"), ) @@ -138,9 +111,6 @@ def render_stats(stats: Stats) -> str: 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) diff --git a/python/lean_pool/validation_cache.py b/python/lean_pool/validation_cache.py index b9fe844067..57392d1c82 100644 --- a/python/lean_pool/validation_cache.py +++ b/python/lean_pool/validation_cache.py @@ -26,7 +26,6 @@ "scripts/nolints-style.txt", "scripts/ci/lint-project.lean", "python/lean_pool/quality.py", - "python/lean_pool/challenge.py", "python/lean_pool/validation_cache.py", "python/pyproject.toml", "python/uv.lock", @@ -63,17 +62,16 @@ def source_inventory(root: Path, modules: list[str]) -> set[Path]: path = root / (imported.replace(".", "/") + ".lean") if path.is_file(): paths.add(path) - elif imported.split(".")[0] in {"LeanPool", "Challenge", "Solution"}: + elif imported.split(".")[0] == "LeanPool": raise ValueError(f"missing imported source: {imported}") except (OSError, ValueError, KeyError, TypeError): LOGGER.warning( "%s: missing import inventory; hashing all local sources", modules[0] ) - for library in ("LeanPool", "Challenge", "Solution"): - paths.update((root / library).rglob("*.lean")) - index = root / f"{library}.lean" - if index.exists(): - paths.add(index) + paths.update((root / "LeanPool").rglob("*.lean")) + index = root / "LeanPool.lean" + if index.exists(): + paths.add(index) return paths diff --git a/python/tests/test_challenge.py b/python/tests/test_challenge.py deleted file mode 100644 index 95ed389ed8..0000000000 --- a/python/tests/test_challenge.py +++ /dev/null @@ -1,604 +0,0 @@ -"""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 - - -def test_challenge_card_does_not_change_when_the_challenge_is_solved() -> None: - """Solving a challenge must not require editing its statement file. - - The PR guard rejects a solution PR that edits a challenge statement, - and the card check rejects a stale card — so any lifecycle field in - the card makes solving a challenge impossible to do cleanly. PR #301 - hit exactly that: the contributor preserved the statement, as the - rules ask, and the stale-card gate failed them for it. - """ - open_card = challenge.challenge_card(CHALLENGE_ENTRY) - solved_card = challenge.challenge_card(_solved_entry()) - - assert open_card == solved_card - assert "Status:" not in open_card - assert "Solution:" not in open_card diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index 3a754ae900..68ff4f9926 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -112,7 +112,5 @@ def test_single_and_sharded_builds_use_validation_cache() -> None: assert "if" not in save # normal success guard, including PR updates contracts.append(restore["with"]) assert "validation_cache lint" in steps[names.index("Lint")]["run"] - assert "runLinter Challenge" in steps[names.index("Lint")]["run"] - assert "runLinter Solution" in steps[names.index("Lint")]["run"] assert "lint-style LeanPool" in steps[names.index("Text style lint")]["run"] assert contracts[0] == contracts[1] diff --git a/python/tests/test_indexes.py b/python/tests/test_indexes.py index c8bcb27579..8ad1f654bf 100644 --- a/python/tests/test_indexes.py +++ b/python/tests/test_indexes.py @@ -41,6 +41,8 @@ def test_complete_public_indexes(tmp_path: Path) -> None: + "public import LeanPool.Beta.Core\n" + "public import LeanPool.Beta.Nested.Other\n" ) + assert not (tmp_path / "Challenge.lean").exists() + assert not (tmp_path / "Solution.lean").exists() assert indexes.structure_errors(tmp_path) == [] assert _check_project_indexes(tmp_path) == [] assert check_index(tmp_path) @@ -179,3 +181,12 @@ def test_lean_public_exports(tmp_path: Path) -> None: capture_output=True, timeout=30, ) + + +def test_default_generation_only_writes_pool_indexes(tmp_path: Path) -> None: + """Default regeneration never recreates retired library roots.""" + _sources(tmp_path) + assert indexes.main(["--repo", str(tmp_path), "--module"]) == 0 + assert (tmp_path / "LeanPool.lean").exists() + assert not (tmp_path / "Challenge.lean").exists() + assert not (tmp_path / "Solution.lean").exists() diff --git a/python/tests/test_prior_art.py b/python/tests/test_prior_art.py index ed2fc13d3b..52b5da4ac5 100644 --- a/python/tests/test_prior_art.py +++ b/python/tests/test_prior_art.py @@ -29,7 +29,7 @@ def test_new_claims_only_covers_what_the_pr_adds() -> None: """A card already on main is settled; only new headlines are searched.""" from lean_pool.prior_art import new_claims - claims = new_claims(PROJECTS_HEAD, PROJECTS_BASE, "project") + claims = new_claims(PROJECTS_HEAD, PROJECTS_BASE) assert [claim.declaration for claim in claims] == [ "LeanPool.DeBruijnErdos.colorable_of_forall_finite" @@ -37,24 +37,6 @@ def test_new_claims_only_covers_what_the_pr_adds() -> None: assert "finite subgraph" in claims[0].informal -def test_new_claims_reads_the_challenge_registry_too() -> None: - """Challenges carry the same pairs under different keys.""" - from lean_pool.prior_art import new_claims - - head = """ -challenges: - - slug: twin-primes - statements: - - declaration: Challenge.TwinPrimes.infinite - informal: There are infinitely many twin primes. -""" - - claims = new_claims(head, "challenges: []\n", "challenge") - - assert claims[0].declaration == "Challenge.TwinPrimes.infinite" - assert claims[0].query == "There are infinitely many twin primes." - - def test_claim_query_falls_back_to_the_declaration_name() -> None: """A card with no informal text is still searchable by name.""" from lean_pool.prior_art import Claim @@ -66,8 +48,8 @@ def test_new_claims_survives_a_malformed_registry() -> None: """Unparseable YAML costs the search, never the review.""" from lean_pool.prior_art import new_claims - assert new_claims("projects: [oops", PROJECTS_BASE, "project") == [] - assert new_claims("", "", "project") == [] + assert new_claims("projects: [oops", PROJECTS_BASE) == [] + assert new_claims("", "") == [] def test_pool_index_lists_every_project() -> None: @@ -92,7 +74,7 @@ def test_render_surfaces_a_duplicate_as_a_candidate_not_a_verdict() -> None: """ from lean_pool.prior_art import MathlibHit, new_claims, render - claims = new_claims(PROJECTS_HEAD, PROJECTS_BASE, "project") + claims = new_claims(PROJECTS_HEAD, PROJECTS_BASE) hits = { claims[0].declaration: [ MathlibHit( @@ -118,7 +100,7 @@ def test_render_says_plainly_when_nothing_matched() -> None: """An empty result is evidence of novelty and must read as such.""" from lean_pool.prior_art import new_claims, render - claims = new_claims(PROJECTS_HEAD, PROJECTS_BASE, "project") + claims = new_claims(PROJECTS_HEAD, PROJECTS_BASE) section = render(claims, {claims[0].declaration: []}, PROJECTS_HEAD, None) @@ -136,7 +118,7 @@ def test_one_failed_query_is_not_reported_as_novelty() -> None: """ from lean_pool.prior_art import new_claims, render - claims = new_claims(PROJECTS_HEAD, PROJECTS_BASE, "project") + claims = new_claims(PROJECTS_HEAD, PROJECTS_BASE) section = render(claims, {claims[0].declaration: None}, PROJECTS_HEAD, None) @@ -176,7 +158,7 @@ def test_render_distinguishes_a_failed_search_from_a_clean_one() -> None: """Silence must never be mistaken for an absence of prior art.""" from lean_pool.prior_art import new_claims, render - claims = new_claims(PROJECTS_HEAD, PROJECTS_BASE, "project") + claims = new_claims(PROJECTS_HEAD, PROJECTS_BASE) section = render(claims, {}, PROJECTS_HEAD, "LEANEXPLORE_API_KEY is not set") diff --git a/python/tests/test_quality.py b/python/tests/test_quality.py index 9271f32d1c..95bdce124e 100644 --- a/python/tests/test_quality.py +++ b/python/tests/test_quality.py @@ -5,10 +5,13 @@ from pathlib import Path from unittest.mock import patch +import pytest + from lean_pool.quality import ( _axiom_audit_missing, _axiom_audit_resolved, _Declaration, + _parse_axiom_output, _parse_declarations, _parse_option_audit_output, _project_card, @@ -854,3 +857,59 @@ def test_quality_check_rejects_malformed_github_repo(tmp_path: Path) -> None: errors = run_checks(tmp_path, skip_lean_axioms=True) assert any("github_repo" in error.message for error in errors) + + +@pytest.mark.parametrize("proof", ["sorry", "by sorry", "by admit", "⟨sorry, trivial⟩"]) +def test_quality_check_rejects_unproved_terms(tmp_path: Path, proof: str) -> None: + """Completed projects reject proof holes in every source form.""" + _write_minimal_repo(tmp_path, f"theorem unfinished : True := {proof}\n") + errors = run_checks(tmp_path, skip_lean_axioms=True) + assert any( + error.message in {"sorry is forbidden", "admit is forbidden"} + for error in errors + ) + + +def test_axiom_audit_rejects_sorry_axiom(tmp_path: Path) -> None: + """A compiled proof hole fails even when textual checks cannot see it.""" + declaration = _Declaration( + "unfinished", tmp_path / "LeanPool/Basic.lean", 7, "theorem" + ) + errors = _parse_axiom_output( + tmp_path, + [declaration], + "'unfinished' depends on axioms: [propext, sorryAx]\n", + ) + assert len(errors) == 1 + assert "unallowlisted axioms: sorryAx" in errors[0].message + + +@pytest.mark.parametrize("name", ["unfinished", "unfinished.eq_def"]) +def test_environment_audit_rejects_proof_holes(tmp_path: Path, name: str) -> None: + """Generated companions cannot hide a compiled proof hole.""" + errors = _parse_option_audit_output( + tmp_path, + f"LEANPOOL_OPTION_AUDIT|LeanPool.Basic|{name}|references " + "forbidden axiom-injecting constants: sorryAx\n" + "LEANPOOL_OPTION_AUDIT_COMPLETE\n", + "", + ) + assert len(errors) == 1 + assert "sorryAx" in errors[0].message + + +@pytest.mark.parametrize("extra", ["", ",\n sorryAx", ",\n customAxiom"]) +def test_axiom_audit_reads_wrapped_lists(tmp_path: Path, extra: str) -> None: + """Lean's wrapped axiom output preserves both safe and forbidden findings.""" + declaration = _Declaration( + "Widget.long_theorem_name", tmp_path / "LeanPool/Widget.lean", 7, "theorem" + ) + errors = _parse_axiom_output( + tmp_path, + [declaration], + "'Widget.long_theorem_name' depends on axioms: [propext,\n" + f" Classical.choice,\n Quot.sound{extra}]\n", + ) + assert bool(errors) == bool(extra) + if extra: + assert extra.split()[-1] in errors[0].message diff --git a/python/tests/test_review.py b/python/tests/test_review.py index 60ed0ba263..66c5d76292 100644 --- a/python/tests/test_review.py +++ b/python/tests/test_review.py @@ -130,256 +130,12 @@ def test_classify_pr_project_root_module_still_counts_as_content() -> None: """A project's own root module is content even at depth two.""" from lean_pool.review import classify_pr, touches_reviewable_content - assert touches_reviewable_content([("Challenge/TwinPrimes.lean", "added")]) - assert touches_reviewable_content([("Solution/Widget.lean", "added")]) assert touches_reviewable_content([("LeanPool/Foo/A.lean", "added")]) # The generated root index alone is not somebody's contribution. assert not touches_reviewable_content([("LeanPool.lean", "modified")]) assert classify_pr([("LeanPool/NewProj/A.lean", "added")]) == "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 @@ -598,7 +354,7 @@ def test_render_comment_notes_truncation() -> None: def test_every_review_mode_asks_for_literal_unicode(monkeypatch) -> None: """The notation rule reaches the model whichever mode is reviewing. - PR #289's challenge review came back with `over ^R09` where `over ℚ` + An earlier review came back with `over ^R09` where `over ℚ` belonged, so a Lean review that cannot render its own notation is a regression worth a test. """ @@ -1003,7 +759,7 @@ def test_infra_skip_comment_is_sticky_and_explains_itself() -> None: assert body.startswith(LLM_REVIEW_MARKER) assert "**Reviewed head:** `abc123`" in body - assert "no project, challenge, or solution here to judge" in body + assert "no project here to judge" in body # No verdict, because there is no contribution to have a verdict about. assert "**Verdict:**" not in body @@ -1062,5 +818,4 @@ def test_gather_prior_art_skips_kinds_with_nothing_new_to_check(monkeypatch) -> from lean_pool import review assert review.gather_prior_art("refactor", "abc123", "o/r") is None - assert review.gather_prior_art("solution", "abc123", "o/r") is None assert review.gather_prior_art("infra", "abc123", "o/r") is None diff --git a/python/tests/test_review_portions.py b/python/tests/test_review_portions.py index 5f2f81d743..fb03a8f13a 100644 --- a/python/tests/test_review_portions.py +++ b/python/tests/test_review_portions.py @@ -329,7 +329,7 @@ def merge_base(number, repo, path): assert "omitted" not in diff -@pytest.mark.parametrize("kind", ["project", "refactor", "challenge", "solution"]) +@pytest.mark.parametrize("kind", ["project", "refactor"]) def test_unresolved_evidence_stays_visible(kind): """All comment formats retain concrete source findings and coverage details.""" payload = review_portions.enforce_resolutions( diff --git a/python/tests/test_stats.py b/python/tests/test_stats.py index 721cbf7020..555c8bed68 100644 --- a/python/tests/test_stats.py +++ b/python/tests/test_stats.py @@ -11,7 +11,6 @@ apply_stats, collect_stats, count_lean_loc, - count_open_challenges, count_projects, main, render_stats, @@ -68,28 +67,6 @@ 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/pins.env b/scripts/challenge/pins.env deleted file mode 100644 index 7e8177cca0..0000000000 --- a/scripts/challenge/pins.env +++ /dev/null @@ -1,20 +0,0 @@ -# Pinned versions of the three external tools that decide whether a challenge -# solution is real. They are part of the trusted base for every `status: -# solved` claim, so bumping one is a deliberate change, not a floating `@main`. -# -# Read by .github/workflows/challenge-verify.yml and by `make comparator`, so -# that a local verification and a CI verification run the same judge. They -# once did not, and the difference hid a real failure: comparator's `main` -# resolves its tools from COMPARATOR_* environment variables, while the pin -# below still hardcodes `lean4export` and `landrun` as PATH lookups. - -# 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 must match this repository's lean-toolchain: it reads the oleans -# our build produced. The workflow asserts that, and prints the right SHA. -# This is refs/tags/v4.35.0-rc3, matching this branch's toolchain. -LEAN4EXPORT_COMMIT=66f1fb4bc256072069767fce52d39480e4524869 - -COMPARATOR_COMMIT=71b52ec29e06d4b7d882726553b1ceb99a2499e0 diff --git a/scripts/challenge/verify-solution.sh b/scripts/challenge/verify-solution.sh deleted file mode 100755 index 38bf87f6dd..0000000000 --- a/scripts/challenge/verify-solution.sh +++ /dev/null @@ -1,151 +0,0 @@ -#!/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 - -# `mktemp -t PREFIX` means a prefix on BSD (macOS) but a *template* on GNU, -# where it must end in at least three X's — so the BSD spelling dies on the -# Linux runner with "too few X's in template". Pass the template as an -# operand, which both implementations read the same way. -config="$(mktemp "${TMPDIR:-/tmp}/lean-pool-comparator.XXXXXX")" -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..." -# Belt and braces: comparator's `main` resolves these from the environment, -# while the commit CI pins hardcodes them as PATH lookups. Provide both, so a -# local run and a CI run behave the same whichever judge is installed. -lean4export_dir="$(dirname "$lean4export_bin")" -landrun_dir="$(dirname "$landrun_bin")" -export PATH="$lean4export_dir:$landrun_dir:$PATH" -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 deleted file mode 100755 index 6e9fa352c1..0000000000 --- a/scripts/ci/build-challenges.sh +++ /dev/null @@ -1,31 +0,0 @@ -#!/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."