diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index a99abfda09..6bf0cced94 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -983,7 +983,10 @@ def _parse_axiom_output( {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) + # Past 120 columns Lean wraps the list after each comma, so the list may span + # lines: `[^\]]*` crosses newlines, and the split below strips the indents. + # `$` still demands that the closing bracket ends its line. + pattern = re.compile(r"^'(.+?)' depends on axioms: \[([^\]]*)\]$", re.MULTILINE) seen: set[str] = set() for match in pattern.finditer(output): name = match.group(1) diff --git a/python/tests/test_challenge.py b/python/tests/test_challenge.py index 95ed389ed8..53d5bb4b32 100644 --- a/python/tests/test_challenge.py +++ b/python/tests/test_challenge.py @@ -353,6 +353,44 @@ def test_axiom_audit_allows_sorry_only_for_registered_declarations() -> None: assert "Challenge.Widget.helper depends on `sorryAx`" in errors[0].message +def test_axiom_audit_reads_a_list_lean_wrapped_over_several_lines() -> None: + """Past 120 columns Lean breaks the axiom list after each comma. + + Each wrapped list must end at its own bracket: an unregistered neighbour + whose wrapped list carries `sorryAx` is still rejected. + """ + declarations = [ + _declaration("Challenge.TestingByBetting.ville_testing_by_betting"), + _declaration("Challenge.TestingByBetting.helper_with_a_long_enough_name"), + ] + # The first result is verbatim `#print axioms` output from `lake env lean` + # (Lean 4.35.0-rc3); the second is wrapped the same way. + output = ( + "'Challenge.TestingByBetting.ville_testing_by_betting' " + "depends on axioms: [propext,\n" + " sorryAx,\n" + " Classical.choice,\n" + " Quot.sound]\n" + "'Challenge.TestingByBetting.helper_with_a_long_enough_name' " + "depends on axioms: [propext,\n" + " sorryAx,\n" + " Classical.choice]\n" + ) + + errors = _parse_axiom_output( + Path("/repo"), + declarations, + output, + {"Challenge.TestingByBetting.ville_testing_by_betting"}, + ) + + assert len(errors) == 1 + assert ( + "Challenge.TestingByBetting.helper_with_a_long_enough_name 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")]