Repository navigation
fix(abstracts): keep explanations with declarations and reserve footer space #529
Description
Follow-up to the completed PDF pipeline work in #421 and #432. Rendering the supporting GSW security abstract in #524 exposed layout defects despite passing the current text-margin checks: explanatory paragraphs could be orphaned from their declarations, a native-efficiency explanation split awkwardly across pages, and a code-box border touched the multi-line provenance footer.
The reviewed standalone PDF was repaired using local TeX layout changes only. The repository renderer remains unchanged, so this issue tracks a reusable fix rather than treating the one-off artifact as a renderer repair.
Acceptance:
- Keep a complete explanatory paragraph with a short following declaration when it fits on a page. Preserve deliberate paragraph boundaries; avoid regexes that capture only the final line or split the code environment.
- Allow genuinely long declarations to break safely; do not solve short-block pagination by making every possible block unbreakable.
- Reserve sufficient vertical space for the full provenance/footer, including non-text code-box borders. Current text bounding boxes alone did not catch the contact.
- Use the checked GSW security abstract as a regression fixture, along with representative selected abstracts and a long-block case. Keep source text, declaration links, exact-revision provenance and source credit intact.
- Run the renderer tests and inspect every page of the representative generated PDFs. Record exact source and artifact revisions and independent visual review. Do not commit generated PDFs.
Likely scope: scripts/build_abstracts.py, scripts/abstract_to_tex.py and focused tests. No Lean theorem changes or catalogue promotion are required. AI-assisted finding from independent review by /root/refactor_plan_review. State: available; no implementation claim.
Activity
SamuelSchlesinger commentedon Oct 24, 2026
Status: active (
worker-jetski-73aa4b5a, session73aa4b5a-fa3d-4195-8024-b19f43bfa557)Claiming #529 on branch
fix/abstracts-pagination-footer-529(isolated worktreewt-529, coordinating with #716 onscripts/abstract_to_tex.pyandscripts/build_abstracts.py):build_abstracts.py.ComplexityTests/Abstracts/GSWSecurityAbstract.lean, selected abstracts, and long declarations, and inspect every page of the generated PDFs.SamuelSchlesinger commentedon Oct 24, 2026
Status: awaiting review (
worker-jetski-73aa4b5a, session73aa4b5a-fa3d-4195-8024-b19f43bfa557)Opened #749 (
fix/abstracts-pagination-footer-529, commit1334176d81b3e27326b28ed87161f25906dd69a1):\begin{minipage}[b]{\linewidth}) inside\NewEnviron{leandeclaration}so TeX counts the full height of short declarations and their explanations against\pagegoalinstead of letting half the box hang into the footer as depth.render_tex_paragraphs, keeps the complete final explanatory paragraph attached to short following declarations, prevents long declarations from orphaning or splitting their explanatory paragraph at the bottom of a page, and reserves vertical space for the multi-line provenance footer (bottom=1.1in,footskip=44pt).page_drawn_boundsinscripts/build_abstracts.pyto enforce>= 12ptclearance above the provenance footer for both body text and non-text code-box borders, along with regression tests coveringGSWSecurityAbstract.lean, multi-paragraph short declarations, long breakable definitions, and footer encroachment rejection../scripts/check.shgates and 75 unit/TeX tests pass; independent visual and code review recorded in fix(abstracts): keep explanations with declarations and reserve footer space (#529) #749.SamuelSchlesinger commentedon Oct 24, 2026
worker-jetski-73aa4b5aawaiting review(approved bycoordinator-reviewer-codex-20261023at exact head1334176d81b3e27326b28ed87161f25906dd69a1in comment 6380192641 with green CI and PDF provenance checks; ready for merge queue)fix(abstracts): keep explanations with declarations and reserve foote…