Repository navigation
ci: check statement files for the headline results and reject opaque constants - #20
Open
Nelson Spence (Fieldnote-Echo) wants to merge 10 commits into
Open
Nelson Spence (Fieldnote-Echo) wants to merge 10 commits into
Nelson Spence (Fieldnote-Echo) wants to merge 10 commits into
Conversation
…constants spec/Spec.lean restates each headline result with sorry as its proof. spec/Check.lean compares every statement there with the library declaration of the same name: equal types up to binder names, a theorem with a proof term, axioms within propext, Classical.choice and Quot.sound, and a statement that is sorry rather than proved. CI runs it and requires a statement for every headline result. The headline list moves to one workflow-level variable read by both checks. The environment check now also rejects opaque constants, which neither #print axioms nor a text search reports, and its self-test fixture declares both an axiom and an opaque constant. The obligation behind the two continuum theorems gets a citable name, gap:pde-infra, in their docstrings and the docs. AGENTS.md describes the checks as they now run and adds a sandbox for elaborating prover output.
Nelson Spence (Fieldnote-Echo)
requested a review
from Navi Bot (project-navi-bot)
as a code owner
October 9, 2026 05:16
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
PR Summary by QodoCI: verify headline statements and reject opaque constants
AI Description
Diagram
High-Level Assessment
Files changed (10)
|
Code Review by Qodo
1.
|
![qodo-code-review[bot]](https://avatars.githubusercontent.com/in/484649?s=60&v=4){kind=small}
| lake env lean spec/Check.lean 2>&1 | tee "$RUNNER_TEMP/spec.txt" | ||
| missing="" | ||
| for name in $HEADLINE_RESULTS; do | ||
| grep -qx "SPEC OK $name" "$RUNNER_TEMP/spec.txt" || missing="$missing $name" |
There was a problem hiding this comment.
1. Statement checks fail despite matching results 🐞 Bug ≡ Correctness
spec/Check.lean emits each success marker with logInfo, but the workflow requires a line containing only SPEC OK and the name. When Lean includes the source location and information prefix in that diagnostic, every headline is marked missing even though the comparator accepted it.
Agent Prompt
## Issue description
The workflow expects bare success lines, while the comparator emits Lean information diagnostics through `logInfo`.
## Fix Focus Areas
- .github/workflows/lean_action_ci.yml[168-175]
- spec/Check.lean[69-72]
## Recommended Fix
Emit unambiguous plain-text success markers, or parse Lean's diagnostic format when checking headline results. Test the check against the actual output of `lake env lean spec/Check.lean`.
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
| - runs the Mathlib environment linters (`lake lint`); | ||
| - runs `CdFormal/Verify.lean` with warnings as errors and requires exactly one `#print axioms` record for each listed declaration, each using only `propext`, `Classical.choice` and `Quot.sound`; | ||
| - fails if a headline result is missing from that list: the two continuum existence theorems, `SemioticGraph.exists_pos_graph` and its unweighted corollary, and the supporting lemmas the README names; | ||
| - checks the statement files: `spec/Spec.lean` restates every headline result with `sorry` as its proof, and `spec/Check.lean` requires each statement there to match the library declaration of the same name (the same type up to binder names and annotations, a theorem with a proof term, axioms within the allowlist), each statement's proof to be `sorry`, and every headline result to have a statement; |
There was a problem hiding this comment.
5. Audit page still claims no sorry anywhere 🐞 Bug ⚙ Maintainability
The PR adds spec/Spec.lean, whose proofs are sorry on purpose, and drops spec/ from the placeholder audit. The unchanged bullet in docs/reference/verification-audit.md still says CI fails if sorry appears anywhere in the Lean sources, so the page now contradicts both the new statement-file bullet above it and the README, and readers will believe the repository is free of sorry.
Agent Prompt
## Issue description
The verification audit page still says CI fails if `sorry` appears anywhere in the Lean sources. The new `spec/Spec.lean` uses `sorry` on purpose and is excluded from the audit.
## Fix Focus Areas
- docs/reference/verification-audit.md[35-38]
## Recommended Fix
Change the bullet to read: fails if `sorry` or `sorryAx` appears anywhere in the library sources (`CdFormal/`), comments included. Then add that the statement files under `spec/` are excluded because their proofs are `sorry` by design.
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
Comment on lines
+431
to
+432
| bwrap --ro-bind /usr /usr --symlink usr/lib /lib --symlink usr/lib /lib64 \ | ||
| --symlink usr/bin /bin --ro-bind /etc /etc --tmpfs "$HOME" \ |
There was a problem hiding this comment.
6. Sandbox recipe breaks on debian and ubuntu 🐞 Bug ☼ Reliability
The bubblewrap command in AGENTS.md links /lib64 to usr/lib. On Debian and Ubuntu the x86-64 dynamic loader /lib64/ld-linux-x86-64.so.2 is under /usr/lib64, not /usr/lib, so dynamically linked programs inside the sandbox (including lake and lean) fail to start, and anyone pasting the recipe as written cannot elaborate prover output in the sandbox.
Agent Prompt
## Issue description
The bwrap recipe maps `/lib64` to `usr/lib`. On Debian and Ubuntu the ELF interpreter `/lib64/ld-linux-x86-64.so.2` is then missing, so lake and lean cannot run in the sandbox.
## Fix Focus Areas
- AGENTS.md[431-432]
## Recommended Fix
Replace `--symlink usr/lib /lib64` with `--symlink usr/lib64 /lib64`. Optionally, note that on merged-/usr distributions where `/usr/lib64` is missing, the mapping should match the host layout.
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
|
|
||
| variable {V : Type*} [Fintype V] (G : SemioticGraph V) | ||
|
|
||
| /-- Statement of `SemioticGraph.exists_pos_graph` (paper Theorem 3.23): connected interior, |
There was a problem hiding this comment.
4. Graph theorem cites wrong paper result 🔗 Cross-repo conflict ≡ Correctness
The new Spec.SemioticGraph.exists_pos_graph docstring calls the result paper Theorem 3.23, while navi-creative-determinant identifies that same Lean theorem as Theorem 3.26. Readers using the statement file to audit the parent repository’s paper are directed to the wrong result.
Agent Prompt
## Issue description
The new graph statement cites paper Theorem 3.23, but the parent repository maps this Lean theorem to Theorem 3.26.
## Fix Focus Areas
- spec/Spec.lean[130-130]
## Recommended Fix
Change the docstring to cite paper Theorem 3.26; no parent-repository change is needed.
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
The loop over HEADLINE_RESULTS passed vacuously on an empty list. The axiom check already rejects one; this step now does too, without relying on it.
…p errors as failures The warning filter excused a sorry warning from any file and swallowed a grep error with || true. It now allows only spec/Spec.lean's sorry warnings and fails on a grep exit above 1. Headline names are matched as fixed strings, so a dot in a name cannot match any character.
…ake's text The text filter examined only lines starting with warning or error, so a warning in another format would pass. The step now elaborates spec/Spec.lean with lake lean --json, which applies the package's linters (lake env lean does not), and accepts only its hasSorry warnings, matched by resolved path; any other message or any non-JSON output fails. spec/ may hold Spec.lean and Check.lean only, and Check.lean runs with warnings as errors. Warnings in library modules remain the build step's, which runs with warnings as errors.
… warnings Information messages were skipped, so an #eval in the statement file could run and print unchecked. Now every message other than its own sorry warnings fails the step, as AGENTS.md states, and output that is not JSON fails with the offending line.
A failing git ls-files fed an empty list to the filter, and || true then let the extra-file check pass. The listing now runs on its own under -e, and a grep exit above 1 fails the step.
A tracked file such as spec/SpecXlean passed the spec/ listing, because grep -x read the allowed names as regular expressions; they are now fixed strings. An example with sorry in the statement file passed, because any number of sorry warnings was accepted; the count must now equal the number of statements the comparator checked. The headline list is split on all whitespace, so a list of only newlines or tabs counts as empty.
…n panics A statement proved around a sorry (have : True := sorry, then the library theorem) depended on sorryAx and passed; the comparator now requires the proof, under the statement's binders, to be an application of sorryAx. It reads the proof from the theorem record: ConstantInfo.value! panics on theorems in v4.34.1, and a panic substitutes a default value and continues with exit code 0, so the step now fails on any PANIC line and on stderr output from the JSON elaboration. The statement count is compared as a single number, so a malformed count cannot fall through.
The check accepted any term headed by sorryAx, so (sorry : A → T) a passed, including a sorry applied to the library proof itself. A statement's proof must now be exactly Lean's sorry under its binders: sorryAx with its type, the synthetic flag false, and a closed label made of Lean.Name constructors and Nat literals, applied to nothing else. The kernel already fixes the sorry's type to the conclusion, so the types are not compared again (a let in a statement is stored as a non-dependent let there and a dependent one in the sorry's type).
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
#print axiomsreports the axioms of a proof, not whether its hypotheses can be met, and a text search cannot tell a comment from a declaration. This adds checks that read the compiled environment and Lean's own messages instead.spec/Spec.leanrestates each headline result withsorryas its proof.spec/Check.leancompares every statement with the library declaration of the same name: equal types up to binder names, a theorem with a proof term, axioms within the allowlist, and a proof that issorryitself, not a proof that merely uses it. CI requires a statement for every headline result. The statement file may produce no message except its ownsorrywarnings, read as Lean's JSON messages with the package's linters on, andspec/may hold only these two files.opaquedeclarations as well as axioms. Its self-test fixture declares both and must see both reported.gap:pde-infrain their docstrings and the docs, so it can be cited beside them.native_decideneeds no new rule. Under v4.34.1 it declares an auxiliary axiom per use (foo._native.native_decide.ax_1_1), so the environment check, the axiom walk and Mathlib's linter all reject it.Controls, each required to fail with its specific report rather than any failure, files restored after each:
sorry, an appliedsorry(also to the library proof), or asorryunder aletby sorrysorryitselfnative_decide#evaloutput, or stderr output in the statement filesorrywarningsexamplewithsorryin the statement filesorrycount differs from the statements checkedspec/Library warnings stay with the build step, which already runs with warnings as errors. The Lake package cache key changes with
lakefile.toml, so the first run refetches packages.