Skip to content

ci: check statement files for the headline results and reject opaque constants #20

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Nelson Spence (Fieldnote-Echo) wants to merge 10 commits into
base: main
Choose a base branch
from
Open

ci: check statement files for the headline results and reject opaque constants #20

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
dfaf642
ci: check statement files for the headline results and reject opaque …
Fieldnote-Echo Oct 9, 2026
c811982
ci: fail the statement-file check when the headline list is empty
Fieldnote-Echo Oct 9, 2026
a8fc302
ci: excuse only the statement file's own sorry warnings and treat gre…
Fieldnote-Echo Oct 9, 2026
82db543
ci: read the statement file's messages as JSON instead of filtering L…
Fieldnote-Echo Oct 9, 2026
bba2730
ci: fail the statement-file check on any message other than its sorry…
Fieldnote-Echo Oct 9, 2026
874eedf
ci: stop the statement-file step if spec/ cannot be listed
Fieldnote-Echo Oct 9, 2026
d09412c
ci: close two false passes in the statement-file step
Fieldnote-Echo Oct 9, 2026
3b02c6d
ci: require each statement's proof to be sorry itself and fail on Lea…
Fieldnote-Echo Oct 9, 2026
492c101
docs: state the statement-file rules as CI now checks them
Fieldnote-Echo Oct 9, 2026
c490d7c
ci: reject an applied sorry in the statement files
Fieldnote-Echo Oct 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
157 changes: 133 additions & 24 deletions .github/workflows/lean_action_ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,17 @@ concurrency:

env:
ELAN_HOME: /home/runner/.elan
# The headline results. Kept in the workflow, not in Verify.lean or spec/, so that dropping one
# from the axiom dashboard or from the statement files fails CI.
HEADLINE_RESULTS: >-
SemioticBVP.exists_isWeakCoherentConfiguration
SemioticBVP.exists_pos_isWeakCoherentConfiguration
SemioticGraph.exists_pos_graph
SemioticGraph.exists_pos_graph_of_unweighted
spectral_characterization_1d
linfty_bound_algebraic
monotone_fixed_point_between
scaling_uniqueness

jobs:
# CONTRACT: org ruleset requires this exact check name 'build'
Expand Down Expand Up @@ -86,15 +97,15 @@ jobs:
run: lake lint

# Verify.lean lists the selected declarations, which must include the headline results named
# below. Each needs exactly one record, and every record may use only propext,
# in HEADLINE_RESULTS. Each needs exactly one record, and every record may use only propext,
# Classical.choice and Quot.sound.
- name: Check axioms
if: ${{ !cancelled() && steps.build.outcome == 'success' }}
run: |
set -o pipefail
lake env lean -DwarningAsError=true CdFormal/Verify.lean 2>&1 | tee "$RUNNER_TEMP/axioms.txt"
python3 - "$RUNNER_TEMP/axioms.txt" <<'EOF'
import collections, pathlib, re, sys
import collections, os, pathlib, re, sys
source = pathlib.Path("CdFormal/Verify.lean").read_text(encoding="utf-8")
expected = re.findall(r"^#print axioms (\S+)\s*$", source, re.M)
lines = []
Expand All @@ -116,13 +127,9 @@ jobs:
errors.append(f"{m[1]} uses {sorted(used - allowed)}")
if not expected:
errors.append("Verify.lean selects no declarations")
# Kept here, not in Verify.lean, so that deselecting a headline result fails the check.
headline = ["SemioticBVP.exists_isWeakCoherentConfiguration",
"SemioticBVP.exists_pos_isWeakCoherentConfiguration",
"SemioticGraph.exists_pos_graph",
"SemioticGraph.exists_pos_graph_of_unweighted",
"spectral_characterization_1d", "linfty_bound_algebraic",
"monotone_fixed_point_between", "scaling_uniqueness"]
headline = os.environ["HEADLINE_RESULTS"].split()
if not headline:
errors.append("HEADLINE_RESULTS is empty")
for name in headline:
if name not in expected:
errors.append(f"headline result {name} is not selected in Verify.lean")
Expand All @@ -142,6 +149,100 @@ jobs:
"results, one record each, using only propext, Classical.choice and Quot.sound.")
EOF

# spec/Spec.lean restates each headline result with `sorry` as its proof: the statement is
# the specification. spec/Check.lean compares every statement there with the library
# declaration of the same name (type up to binder names, a theorem with a proof term,
# axioms within the allowlist) and rejects a statement file that proves instead of states.
- name: Check statement files
if: ${{ !cancelled() && steps.build.outcome == 'success' }}
run: |
set -o pipefail
# Split on any whitespace, so a list of only newlines or tabs counts as empty.
read -r -d '' -a headline <<< "$HEADLINE_RESULTS" || true
if [ "${#headline[@]}" -eq 0 ]; then
echo "::error::HEADLINE_RESULTS is empty"
exit 1
fi
# spec/ holds the statement file and its checker, nothing else.
specfiles=$(git ls-files 'spec/*')
status=0
others=$(printf '%s\n' "$specfiles" | grep -v -x -F -e spec/Spec.lean -e spec/Check.lean) ||
status=$?
if [ "$status" -gt 1 ]; then
echo "::error::could not list spec/ (grep exit $status)"
exit 1
fi
if [ -n "$others" ]; then
echo "::error::unexpected files in spec/: $others"
exit 1
fi
lake build Spec 2>&1 | tee "$RUNNER_TEMP/spec-build.txt"
# The statement file's own messages, read as JSON from Lean with the package's options
# (linters included), not by filtering Lake's text output. Allowed: its sorry warnings.
# Any other message (information included: the file must not print), or any output that
# is not JSON, fails the step. Warnings in the
# library are the build step's concern: it runs with warnings as errors.
lake --quiet lean spec/Spec.lean -- --json > "$RUNNER_TEMP/spec-messages.jsonl" \
2> "$RUNNER_TEMP/spec-stderr.txt"
if [ -s "$RUNNER_TEMP/spec-stderr.txt" ]; then
echo "::error::Lean wrote to stderr while elaborating the statement file"
cat "$RUNNER_TEMP/spec-stderr.txt"
exit 1
fi
python3 - "$RUNNER_TEMP/spec-messages.jsonl" "$RUNNER_TEMP/spec-sorries.txt" <<'EOF'
import json, os, sys
spec = os.path.realpath("spec/Spec.lean")
sorries, other = 0, []
for line in open(sys.argv[1], encoding="utf-8"):
if not line.strip():
continue
try:
m = json.loads(line)
except json.JSONDecodeError:
print(f"::error::output from Lean that is not JSON: {line.strip()}")
sys.exit(1)
if (m["severity"] == "warning" and m.get("kind") == "hasSorry"
and os.path.realpath(m["fileName"]) == spec):
sorries += 1
continue
other.append(f'{m["fileName"]}:{m["pos"]["line"]}: {m["severity"]}: {m["data"]}')
if other:
print("::error::the statement file has a message other than its sorry warnings")
print("\n".join(other))
sys.exit(1)
if sorries == 0:
print("::error::the statement file reports no sorry warning")
sys.exit(1)
open(sys.argv[2], "w").write(f"{sorries}\n")
print(f"{sorries} sorry warnings and no other message in spec/Spec.lean")
EOF
lake env lean -DwarningAsError=true spec/Check.lean 2>&1 | tee "$RUNNER_TEMP/spec.txt"
# A Lean panic prints, substitutes a default value and continues with exit code 0.
status=0
grep -q -F 'PANIC' "$RUNNER_TEMP/spec.txt" || status=$?
if [ "$status" -ne 1 ]; then
echo "::error::Lean panicked while checking the statement files (grep exit $status)"
exit 1
fi
# One sorry warning per statement: a sorry anywhere else (an example, say) is not a
# statement the comparator checked.
statements=$(sed -n 's/^\([0-9][0-9]*\) statements match the library$/\1/p' "$RUNNER_TEMP/spec.txt")
sorries=$(cat "$RUNNER_TEMP/spec-sorries.txt")
# String comparison of two single numbers: a malformed count must not fall through.
if ! [[ "$statements" =~ ^[0-9]+$ && "$sorries" =~ ^[0-9]+$ ]] ||
[ "$statements" != "$sorries" ]; then
echo "::error::$sorries sorry warnings for ${statements:-no} checked statements"
exit 1
fi
missing=""
for name in "${headline[@]}"; do
grep -qxF "SPEC OK $name" "$RUNNER_TEMP/spec.txt" || missing="$missing $name"
done
if [ -n "$missing" ]; then
echo "::error::headline results without a matching statement:$missing"
exit 1
fi

# Every Lean name written in inline code in the README and the docs, and every declaration
# shown in a Lean code block there, must resolve.
- name: Check documented names
Expand Down Expand Up @@ -177,39 +278,45 @@ jobs:
fi
echo "$(grep -c '^#check' "$RUNNER_TEMP/DocNames.lean") documented names resolve."

# No axiom may be declared in any CdFormal module, even one that no selected declaration
# uses. The check reads the compiled environment, so it cannot be fooled by layout. It first
# proves it can fail: a module declaring a two-line axiom must be reported.
- name: Check that no axiom is declared
# No axiom and no opaque constant may be declared in any CdFormal module, even one that no
# selected declaration uses: the kernel cannot see an opaque constant's value, and neither
# #print axioms nor a text search reports one. The check reads the compiled environment, so
# it cannot be fooled by layout. It first proves it can fail: a module declaring a two-line
# axiom and an opaque constant must have both reported.
- name: Check that no axiom or opaque constant is declared
if: ${{ !cancelled() && steps.build.outcome == 'success' }}
run: |
cat > "$RUNNER_TEMP/axiom_check.lean" <<'EOF'
open Lean in
#eval show CoreM Unit from do
let env ← getEnv
let mut found := #[]
let mut axioms := #[]
let mut opaques := #[]
let mut modules := 0
for mod in env.header.moduleNames, data in env.header.moduleData do
if mod.getRoot == `CdFormal then
modules := modules + 1
for c in data.constants do
if c matches .axiomInfo _ then found := found.push c.name
unless found.isEmpty do throwError "axioms declared in CdFormal: {found}"
IO.println s!"no axiom declared in any of {modules} CdFormal modules"
if c matches .axiomInfo _ then axioms := axioms.push c.name
if c matches .opaqueInfo _ then opaques := opaques.push c.name
unless axioms.isEmpty && opaques.isEmpty do
throwError "axioms declared in CdFormal: {axioms}; opaque constants: {opaques}"
IO.println s!"no axiom or opaque constant declared in {modules} CdFormal modules"
EOF
fixture=CdFormal/CiAxiomFixture.lean
trap 'rm -f "$fixture" .lake/build/lib/lean/CdFormal/CiAxiomFixture.*' EXIT
printf 'import CdFormal.Basic\n\naxiom\n ciAxiomFixture : False\n' > "$fixture"
printf '%s\n' 'import CdFormal.Basic' '' 'axiom' ' ciAxiomFixture : False' '' \
'opaque ciOpaqueFixture : Nat' > "$fixture"
lake build CdFormal.CiAxiomFixture
{ echo 'import CdFormal.CiAxiomFixture'; cat "$RUNNER_TEMP/axiom_check.lean"; } \
> "$RUNNER_TEMP/SelfTest.lean"
# Detection must be the reason for failure: require a nonzero exit and the exact report.
status=0
lake env lean "$RUNNER_TEMP/SelfTest.lean" > "$RUNNER_TEMP/selftest.txt" 2>&1 || status=$?
cat "$RUNNER_TEMP/selftest.txt"
if [ "$status" -eq 0 ] ||
! grep -qF 'axioms declared in CdFormal: [ciAxiomFixture]' "$RUNNER_TEMP/selftest.txt"; then
echo "::error::the axiom self-test did not report ciAxiomFixture"
expected='axioms declared in CdFormal: [ciAxiomFixture]; opaque constants: [ciOpaqueFixture]'
if [ "$status" -eq 0 ] || ! grep -qF "$expected" "$RUNNER_TEMP/selftest.txt"; then
echo "::error::the self-test did not report ciAxiomFixture and ciOpaqueFixture"
exit 1
fi
rm -f "$fixture" .lake/build/lib/lean/CdFormal/CiAxiomFixture.*
Expand All @@ -223,7 +330,8 @@ jobs:
shell: python
run: |
import pathlib, re, subprocess, sys
files = subprocess.run(["git", "ls-files", "CdFormal.lean", "CdFormal/*.lean"],
files = subprocess.run(["git", "ls-files", "CdFormal.lean", "CdFormal/*.lean",
"spec/*.lean"],
capture_output=True, text=True, check=True).stdout.split()
header = re.compile(r"/-\nCopyright \(c\) 20\d\d [^\n]+\. All rights reserved\.\n"
r"Released under Apache 2\.0 license as described in the file LICENSE\.\n"
Expand All @@ -243,8 +351,9 @@ jobs:
sys.exit("header check failed:\n " + "\n ".join(bad or ["no files"]))
print(f"{len(files)} files have a copyright header and a module docstring after the imports.")

# 'sorry' and 'sorryAx' may not appear anywhere in the Lean sources, comments included, and
# no axiom may be declared.
# 'sorry' and 'sorryAx' may not appear anywhere in the library sources, comments included.
# The statement files under spec/ are outside this audit: their proofs are sorry by design,
# and the statement-file check requires it.
- name: Audit placeholders
if: ${{ !cancelled() }}
run: |
Expand Down
53 changes: 43 additions & 10 deletions AGENTS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,9 @@ A formalization of the existence theory for the Creative Determinant problem

## Invariants

- **No `sorry` on the default branch.** Every declaration is fully proved before merge.
- **No `sorry` in the library on the default branch.** Every declaration under `CdFormal/` is
fully proved before merge. The statement files under `spec/` are the one exception: each
restates a headline result with `sorry` as its proof, and CI requires that.
- **No `axiom` declarations.** Classical results that are not proved are assumed through a
typeclass or structure field (see *Assumed results*, which needs approval), never
through `axiom`.
Expand Down Expand Up @@ -59,13 +61,24 @@ lake exe cache get # Mathlib oleans; never bui
lake build --wfail # warnings are errors (includes sorry)
lake lint # Mathlib environment linters
lake env lean -DwarningAsError=true <Pkg>/Verify.lean # axiom dashboard
lake build Spec && lake env lean spec/Check.lean # statement files against the library
```

- `CdFormal/Verify.lean` holds exactly one `#print axioms` record per selected declaration:
every headline result and the supporting declarations the docs cite. The headline results
are listed in the CI workflow, not in `Verify.lean`, so dropping one from the dashboard
fails CI; add a new headline result to both. Every record may use only `propext`,
`Classical.choice` and `Quot.sound`.
are listed once, in the CI workflow (`HEADLINE_RESULTS`), not in `Verify.lean` or `spec/`,
so dropping one from the dashboard or from the statement files fails CI. Add a new headline
result to all three: the workflow list, a `#print axioms` record, and a statement in
`spec/Spec.lean` copied from the source with its proof replaced by `sorry`. Every record may
use only `propext`, `Classical.choice` and `Quot.sound`.
- `spec/` holds `Spec.lean` and `Check.lean` only; CI rejects any other file there. The only
messages `spec/Spec.lean` may produce are its own `sorry` warnings, one per statement, read by
CI as Lean's JSON messages with the package's linters on. Each statement's proof is `sorry`
itself, not a proof that uses `sorry` somewhere.
- A statement file states; it does not prove. `spec/Check.lean` rejects a statement whose proof
is not `sorry`, a statement whose type differs from the library declaration of the same name
(binder names and annotations aside), a library declaration that is not a theorem, and a
library proof whose axioms leave the allowlist.
- If the sandbox cannot install Lean or fetch the Mathlib cache, push to a draft PR and
let CI build and verify. Report which checks ran where; never claim a local build that
did not happen.
Expand All @@ -76,9 +89,12 @@ lake env lean -DwarningAsError=true <Pkg>/Verify.lean # axiom dashboard
- Test the checkers themselves. An axiom or `sorry` gate that silently passes is worse than
none (a pipe without `pipefail` once hid Lean failures here). When you add or change a
gate, also add a small negative fixture that must fail it and a snapshot of expected
axiom output that its parser must accept. This repo's CI has neither yet: after changing
the axiom check or the audit, test it by hand against a file that uses `sorry` or declares
an `axiom`.
axiom output that its parser must accept. In this repo's CI only the environment check
carries a fixture (an `axiom` and an `opaque` constant it must report). After changing the
axiom dashboard parser, the statement-file comparator or the audit, test them by hand: a
file that uses `sorry`, a statement with a changed hypothesis, a statement proved instead
of stated, and a library proof that uses native evaluation (which declares an auxiliary
axiom under Lean v4.34.1).
- Change `lake-manifest.json` only in an intentional dependency bump. No CI guard enforces
this here; check the diff yourself.
- If a repo has a docs site, `uv run zensical build` must succeed; CI also checks the
Expand All @@ -88,14 +104,18 @@ lake env lean -DwarningAsError=true <Pkg>/Verify.lean # axiom dashboard
- `lake build --wfail` of the root and every module, then `lake lint`;
- the axiom check: the selection includes every headline result, one record each, all
within the allowlist;
- the statement-file check: every headline result has a statement in `spec/Spec.lean`, and
every statement there matches its library declaration as described above;
- the documented-names check: every inline-code token in the README and docs that looks
like a Lean name containing an uppercase letter, `_` or `.`, and every declaration shown
in a Lean code block there, must resolve (all-lowercase names are not checked);
- the header check: every file has the copyright header and a module docstring after the
imports (Lean itself rejects an `import` after any command, so imports come first);
- the placeholder audit: no `sorry` or `sorryAx` anywhere, and no line that starts an
`axiom` declaration (a text search; `#print axioms` still catches any axiom a selected
result uses);
- the placeholder audit: no `sorry` or `sorryAx` anywhere in the library sources, comments
included (a text search; `spec/` is outside it by design);
- the environment check: no module of the library declares an `axiom` or an `opaque`
constant, read from the compiled environment, after a self-test with a fixture that
declares both;
- the docs build, and a link check that also verifies fragments.
Everything else in this file is a convention to follow, not an automated gate.
- If a repo has a `Makefile`, use its targets (`build`, `verify`, `audit`, `lint`) as
Expand Down Expand Up @@ -407,5 +427,18 @@ Aristotle grinds leaf lemmas and detects dependencies. It is not the theorem arc
`pp.all`; none of them belongs in a leaf proof.
- Rebuild with `lake build --wfail`: Aristotle doesn't run the project's style linters.
- Before trusting output, check Aristotle's Lean version against `lean-toolchain`.
- Elaborating a file runs code (`#eval`, `initialize`, tactics, macros), so elaborate a
returned file in a sandbox before it touches the repository: no network, home directory
hidden, the project read-only. With bubblewrap, from the project root:

```bash
bwrap --ro-bind /usr /usr --symlink usr/lib /lib --symlink usr/lib /lib64 \
--symlink usr/bin /bin --ro-bind /etc /etc --tmpfs "$HOME" \
Comment on lines +435 to +436

@qodo-code-review qodo-code-review Bot Oct 9, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Informational

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

Dismiss ↗ | View ↗

--ro-bind "$HOME/.elan" "$HOME/.elan" --ro-bind "$PWD" "$PWD" \
--ro-bind <returned-dir> /untrusted --proc /proc --dev /dev --tmpfs /tmp \
--unshare-all --die-with-parent --chdir "$PWD" lake env lean /untrusted/<File>.lean
```

Adjust the binds to where elan and the toolchain live on your machine.
- Keep raw prover artifacts and run logs out of the public repository. Commit only the
rewritten proofs, and credit Aristotle in the README.
Loading
Loading