quality: read an axiom list that Lean wrapped over several lines

[deadczarvc]

_parse_axiom_output expects the whole #print axioms result on one line. Past 120 columns Lean breaks the list after each comma, and a challenge statement with a long name reaches that easily, because the open declaration's list carries sorryAx as well. Verbatim output for the statement in #557 (Lean 4.35.0-rc3, lake env lean):

'Challenge.TestingByBetting.ville_testing_by_betting' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]

The pattern \[(.*)\]$ finds no closing bracket on the first line, so the declaration is never marked as seen. _axiom_audit_resolved still counts it as resolved, since it only needs the prefix, and the audit then reports a false error: the open statement "does not depend on sorryAx". The same miss would let a wrapped list with an unallowlisted axiom through unchecked.

The fix lets the list span lines (\[([^\]]*)\], still re.MULTILINE for the anchor); the existing split on commas already strips the line breaks and indents. A regression test feeds the verbatim output above and expects no errors (it fails on main).

Checks: ruff check and ruff format --check clean on both files; pytest tests/test_challenge.py tests/test_quality.py: 75 passed. The full tests/ run on Windows has the same 28 environment failures on main with and without this change (aggregator cloner, codex worker, exposition and similar), 533 passed vs 532 on main.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium risk] Adjusts axiom parsing to handle Lean's line wrapping.

The PR appears safe to merge based on the reviewed changes.

Summary

The PR updates the axiom-output parser to read Lean’s multiline lists and adds a regression test that rejects sorryAx in an unregistered declaration. A subsequent metadata refresh updates NOTICE and README.

_{Reviews (12) · Last reviewed commit: "Merge branch 'main' into fix/axiom-audit..."}

[Vilin97]

The multiline capture fixes the reported wrapped sorryAx output, and the new test correctly fails on the old parser. One small change is needed before this gate update merges:

1. Retain the existing end-of-line $ after the closing \]. The new [^\]]* already spans continuation lines, and $ under re.MULTILINE still matches the closing bracket on its final line. Without $, the parser accepts a line such as 'Challenge.Widget.widget_exists' depends on axioms: [sorryAx] unexpected text and silently ignores the trailing content. The gate should continue requiring the complete #print axioms list line.
2. Extend the regression with a neighboring declaration after the wrapped registered statement: an unregistered helper whose list contains sorryAx must still produce the existing rejection. This checks that the multiline match ends at its own bracket and the next result is audited independently.

I checked both regexes against the wrapped sample and the trailing-text case in memory: retaining $ passes the valid wrapped sample and rejects the trailing-text case. With the exact PR parser, a wrapped registered statement followed by an unregistered helper still raises the helper error, while the trailing-text input is accepted without error. In an isolated exact-head checkout, focused test_challenge.py and test_quality.py passed (75 tests), and Ruff check/format checks passed on the two changed files. Hosted Python CI is still queued, so these are local results only.

[Vilin97]

Reviewed exact head 36db76fabc7809e1747c3704934062f7cc8c2ee5. The follow-up restores the parser's terminal $ while [^\]]* reads Lean's wrapped axiom list across lines. The regression now places a wrapped registered sorryAx statement immediately before a wrapped unregistered helper and requires the helper to be rejected. This resolves both findings in my prior changes-requested review.

In an isolated exact-head checkout, focused axiom-audit pytest passed (4 tests), the new regression passed individually, and Ruff check and format checks passed for the two changed files. The checkout diff is limited to python/lean_pool/quality.py and python/tests/test_challenge.py.

Approved as a gate-code review. Merge still awaits explicit user authorization and protected CI at this head.

[greptile-apps]

Want your agent to iterate on Greptile's feedback? Try greploops.

[Vilin97]

Needs maintainer: explicitly authorize this protected axiom-audit repair.

Re-reviewed exact head 442e3c5b7af2e69aae663539c7e4f0677cb5bc90 against main 16ac1e76587e01548c71d8ed96e298e87ecfd4ed. The diff contains only python/lean_pool/quality.py and python/tests/test_challenge.py. In an isolated checkout, 75 focused tests passed, and Python Ruff lint/format checks passed. The regression fails against the current main parser. Actual output from pinned Lean 4.35.0-rc3 confirms that the repair accepts a registered wrapped statement and rejects the following unregistered wrapped sorryAx helper; separate probes reject wrapped unallowlisted axioms and trailing text. No further code repair is justified.

Both inline review threads are now resolved. The existing code approval nevertheless explicitly reserves authorization. Live CONTRIBUTING.md says “Never change the checks or gates” and allows changes only “unless explicitly asked.” I found no recorded explicit grant for changing protected quality.py. The exact outstanding decision is to grant or decline that policy exception. needs-maintainer remains for this decision; pending CI and disabled auto-merge are separate operational conditions.

Continuation: once explicitly authorized, re-read the head and current main, revalidate any integration changes, and use normal protected merging after required checks pass. This is an external fork, so this cycle made no branch push. Updated this existing comment to avoid a duplicate discussion entry.

Final cycle reconciliation: GitHub records this PR as closed by the Vilin97 account at 2026-10-02 17:26:38 UTC, after the review above. This cycle preserves that external closure. No grant of permission or rejection of the parser mathematics is inferred from an unexplained closure. The label was removed because there is no longer an open PR awaiting disposition.