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

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)

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")]