From 7940b42d7ea2bd7bf2d3eb1ccaad062c706648dd Mon Sep 17 00:00:00 2001
From: David Loeffler <d.loeffler.01@cantab.net>
Date: Fri, 23 Oct 2026 18:20:58 +0200
Subject: [PATCH] wrap long lines in `Main declarations: ` in project card

---
 python/lean_pool/quality.py  |  9 +++++++-
 python/tests/test_quality.py | 43 ++++++++++++++++++++++++++++++++++++
 2 files changed, 51 insertions(+), 1 deletion(-)

diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py
index 7adf1cfdd9..e5414f7719 100644
--- a/python/lean_pool/quality.py
+++ b/python/lean_pool/quality.py
@@ -7,6 +7,7 @@
 import subprocess
 import sys
 import tempfile
+import textwrap
 from dataclasses import dataclass
 from pathlib import Path
 from typing import Any
@@ -1373,7 +1374,13 @@ def _project_card(project: dict[str, Any]) -> str:
         f"Source: {_format_source(project['source'])}",
         f"Authors: {authors}",
         f"Status: {project['status']}",
-        f"Main declarations: {declarations}",
+        textwrap.fill(
+            f"Main declarations: {declarations}",
+            width=100,
+            subsequent_indent="  ",
+            break_long_words=False,
+            break_on_hyphens=False,
+        ),
         f"Tags: {tags}",
     ]
     if project.get("msc"):
diff --git a/python/tests/test_quality.py b/python/tests/test_quality.py
index 494b696542..a638f72e5e 100644
--- a/python/tests/test_quality.py
+++ b/python/tests/test_quality.py
@@ -10,6 +10,7 @@
 from lean_pool.quality import (
     _axiom_audit_missing,
     _axiom_audit_resolved,
+    _card_is_current,
     _Declaration,
     _parse_axiom_output,
     _parse_declarations,
@@ -586,6 +587,48 @@ def test_quality_check_does_not_honor_size_marker(tmp_path: Path) -> None:
 }
 
 
+def test_project_card_keeps_short_declarations_on_one_line() -> None:
+    """Short headline lists retain their existing generated representation."""
+    assert "\nMain declarations: `hello`\n" in _project_card(_PROJECT_FIXTURE)
+
+
+def test_project_card_wraps_main_declarations(tmp_path: Path) -> None:
+    """Long headline lists wrap intact identifiers and remain current on rewrite."""
+    declarations = [f"Example.result_{index}_" + "x" * 60 for index in range(3)]
+    project = {**_PROJECT_FIXTURE, "main_declarations": declarations}
+    card = _project_card(project)
+    lines = card.splitlines()
+    start = next(
+        i for i, line in enumerate(lines) if line.startswith("Main declarations:")
+    )
+    end = next(i for i, line in enumerate(lines) if line.startswith("Tags:"))
+    headlines = lines[start:end]
+    assert len(headlines) > 1
+    assert all(len(line) <= 100 for line in headlines)
+    assert all(line.startswith("  ") for line in headlines[1:])
+    assert " ".join(line.strip() for line in headlines) == (
+        "Main declarations: " + ", ".join(f"`{name}`" for name in declarations)
+    )
+
+    entry = tmp_path / "MyProj.lean"
+    attribution = "/-!\n## Attribution\nRetain this separate docstring.\n-/\n"
+    entry.write_text(f"{HEADER}\nimport LeanPool.Basic\n\n{attribution}")
+    _write_project_card(entry, card)
+    generated = entry.read_text()
+    assert _card_is_current(generated, card)
+    assert attribution in generated
+    assert not _card_is_current(generated.replace(declarations[0], "different"), card)
+    _write_project_card(entry, card)
+    assert entry.read_text() == generated
+
+
+def test_project_card_does_not_split_overlong_identifiers() -> None:
+    """An unsplittable identifier is preserved rather than producing a broken link."""
+    declaration = "Example." + "x" * 110
+    card = _project_card({**_PROJECT_FIXTURE, "main_declarations": [declaration]})
+    assert f"`{declaration}`" in card
+
+
 def test_write_project_card_inserts_card_after_imports(tmp_path: Path) -> None:
     """The card writer must place the card after imports, not before them.