Keep implementation notes separate from mathematical articles

[Deicyde]

Summary

• keep mathematical articles to frontmatter and informal mathematics
• store versioned implementation handoffs in one hidden file per article: blueprint/.implementation-notes/<article_id>.md
• key notes by durable article_id, so article moves preserve them and independent article claims never share a note file
• make autoform check reject noncanonical, malformed, empty, symlinked, unreadable, or orphaned notes
• make autoform audit report a note left after its article is proved, or after every formalizable descendant of a container is proved
• leave ordinary agents.md and standard AGENTS.md untouched as normal content/instructions
• teach Roadmap and Formalize to use the per-article note and keep transcripts, secrets, and machine-local paths out; Formalize deletes every note the audit reports as stale, including a container's note its proof completes

Why this design

Implementation details should not clutter the mathematical wiki, but a shared agents.md created a reserved-name collision, cross-worker merge hotspot, filename-based stale state, and a hard migration for older pinned projects.

The hidden per-article directory avoids those problems. Existing and older graph loaders scan only blueprint/roadmap/, while existing renderers and structure views already omit hidden path components. No renderer exception or pin migration is required.

Contract

• filenames are existing durable article IDs plus .md
• one regular, nonempty UTF-8 Markdown file belongs to one article claim
• roadmap path moves do not rename the note
• the file is deleted after leaf proof or completion of a container's formalizable subtree (a container with no formalizable descendant keeps its note); audit reports stale notes
• hidden implementation notes are neither mathematics nor dependency-graph state and never enter publication hashes

Validation

At exact implementation head before the final clean merge from current main:

• full suite: 1,842 passed, 6 skipped, 1 expected failure
• focused graph/audit/render/visualization/skill suites: 229 passed
• container cleanup roll-up regression: 1,200 containment levels without recursion
• make lint and make check-example: passed
• Formalize and Roadmap skill validation: passed
• independent code and architecture re-reviews: approved

After merging current main, the focused tests, lint, diff check, and
example build pass. GitHub CI at b032c03f was green, including both Windows
and real-Lean jobs.

At 3e95335, which has Formalize delete stale notes, states the container rule exactly in the README and Roadmap skill, and passes a statement string to _ArticleShape in the deep-containment test to match main: make lint passes locally, and GitHub CI is green for both the push and the merge with main, including the Python 3.10 and 3.13 test jobs (lint, full suite, example build), Windows, and real-Lean jobs.

[Deicyde]

Superseded by the review of f13757c after the per-article notes redesign: #172 (comment)

Review of #172 at 8e372ad. The graph, render, and hash changes are sound, but coverage still accepts the notes file as article evidence, and the old-pin caveat is wrong for notes files with an H1.

Should fix

• autoform_cli/coverage.py:574 _is_roadmap_article still accepts any existing .md under roadmap/. A DECOMPOSED row whose only evidence is [Notes](../roadmap/agents.md) therefore passes load_coverage (no issues) and autoform check (rc 0). On base the same project fails with agents: missing H1 title. After render_site, the coverage page links to ../roadmap/agents.md, which is never written. Fix: import is_agent_notes from .graph and append and not is_agent_notes(candidate). Add a test_coverage case that expects "DECOMPOSED coverage evidence has no link to an existing roadmap article". With both changes, test_coverage gives 54 passed and ruff is clean.
• autoform_cli/README.md:85 (same wording at skills/formalize/SKILL.md:125 and skills/roadmap/SKILL.md:71): the claim that an older AUTOFORM_REF "reads it as an article and fails" holds only when the file has no H1. On base, agents.md = # top.md\n\nMathlib gap.\n passes check ("OK: 4 articles"), becomes node agents, and render publishes roadmap/agents.md. That is the leak this PR exists to stop, on exactly the pinned projects the caveat targets. Fix: state the format ("one ## <file>.md section per article, no H1") in README:81 and both skills, or reword the caveat to say an old pin either fails or publishes the notes.

Golf

• tests/test_skill_examples.py:72 the "agents.md" entry duplicates the stricter assertions in the new test (line 110). Delete the line without replacing it. test_skill_examples still gives 26 passed.

Nits

• autoform_cli/render.py:333 render skips agents.md, but _rewrite_links still rewrites links to it, so an article that links its notes gets a dead link on the site (roadmap/README.md -> agents.md exists: False). check does not flag it. Drop the link and keep its label when the target is_agent_notes, or say "never linked from an article" in the skills.
• autoform_cli/README.md:1040 says to record revision outcomes "in the agents.md beside each touched article", while skills/formalize/SKILL.md:124 says to delete the section once the article is proved. Repaired in-place dependents and proof-impacted articles stay proved, so their record is lost, including the note that they still rest on deprecated X. Exempt revision records until the migration lands, or put them in the commit or report.
• autoform_cli/README.md:13 the match is name.casefold() == "agents.md", so an article named Agents.md drops out with no error. Write "except agents.md (in any letter case)".
• skills/formalize/SKILL.md:64 the line is 49 columns between 74-column neighbors. Reflow lines 62-66.

Checked, no change needed

• Merged tree: test_graph 58, test_render 78, test_visualization 24, test_skill_examples 26, test_coverage 53, all passed. ruff on the seven changed Python files passes.
• Graph discovery, the orphaned-chapter check, render_site, _published_source_files, and both structure pages all skip agents.md. Editing the notes leaves the publication revision unchanged.
• Parallel workers appending to one agents.md conflict textually. The PR body accepts this tradeoff, and the skill says to keep both sections.
• No Execution notes references remain outside the test that forbids them.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Review of #172 at f13757c (replaces the review of 8e372ad). The per-article hidden-notes design is sound and nothing blocks the merge, but audit reports note errors at wrong paths and the revision contract conflicts with the new audit rule.

The earlier coverage, old-pin, dead-agents.md-link and casefold findings are moot because notes no longer live under roadmap/. The revision-record finding is still present and worse (see Should fix). The duplicate skill assertion and the ragged lines are still present.

Should fix

• autoform_cli/audit.py:549 _validation_article_path treats the .implementation-notes/... prefix as a node ID, so every note error is reported at a nonexistent file. An orphaned note is reported at roadmap/.implementation-notes/af_111111111111111111111111.md.md. A file in place of the directory gives roadmap/.implementation-notes.md, and an alias gives roadmap/.Implementation-Notes.md. This breaks README:808 ("structured findings at blueprint-relative paths"). Fix: after the return "." guard add if node_id.split("/", 1)[0].casefold() == IMPLEMENTATION_NOTES_DIR: return node_id, then add an orphan-note audit test. That test fails on the head and passes with the fix (test_audit 27 passed, ruff clean).
• autoform_cli/README.md:1092 the revision contract says to record the outcome in each touched article's note. Repaired in-place dependents and expand-route proof-impacted articles stay proved, though, and audit.py:176 then reports stale-implementation-note. A proved article with a revision note passes check and fails audit. Workers either fail audit or delete the record that the article still rests on deprecated X. On main that record lived in ## Execution notes and was never forced out. Fix: "Record what happened in the revision commit and report; use an article's implementation note only while that article remains unproved."
• skills/roadmap/SKILL.md:71 Roadmap is told to put prior art in the note but never told to delete it. A note on an article marked mathlib: true fails audit, because status counts that as proved. Deleting or merging an article leaves an orphan, which stops every graph command: on the bundled example with one leftover note, check rc=1, render rc=1 and work list rc=2. README:83 says only that autoform check rejects bad notes. Fix: add "Delete the note when the article is proved or marked mathlib: true, and in the same commit that deletes or merges the article; an orphaned note fails every command that loads the graph." Reword README:83 to "Every command that loads the graph, including autoform check, rejects".
• autoform_cli/audit.py:176 no test covers a note on an unproved article. With and derived[node_id].proved removed, test_audit still gives 25 passed, so audit could reject every in-progress note unnoticed. Fix: add an unproved-theorem-with-note case next to test_audit_rejects_implementation_notes_left_after_proof that asserts no stale-implementation-note.

Golf

These edits, applied together with the audit fix and two new tests, keep the suites passing: test_graph 61 (the drop is the 2 agents.md cases), test_audit 27, test_render 78, test_skill_examples 26, ruff clean.

• autoform_cli/graph.py:407 replace node_id = article_ids.get(path.stem) / if node_id is None: with if path.stem not in article_ids:, and put the four wrapped issues.append calls on one line each (limit is 120). Keep the separate symlink and not-a-directory messages.
• tests/test_graph.py:526 delete test_agents_filenames_remain_ordinary_articles; it guards the abandoned design, and main has no agents.md handling. Fold test_implementation_notes_directory_has_canonical_spelling (593) into the fail-closed parametrize as a directory column. In tests/test_render.py delete 1048-1050 and 1058, and assert == before at 1062.
• tests/test_skill_examples.py:72 duplicates line 107. Line 110 pins rationale prose, and line 120 guards agents.md, which main never had. Delete all three, and drop the rationale sentence at skills/formalize/SKILL.md:124-125, which repeats README:80-83.

Nits

• autoform_cli/graph.py:410 a parse error in the note's own article (for example a missing H1) also reports its valid note as "names no roadmap article", which invites deleting a good handoff. Skip the orphan check when parse issues exist.
• autoform_cli/graph.py:397 the dotfile skip runs before the symlink and naming checks. A misnamed .af_<id>.md and a .secret symlink to $HOME both pass check. Nothing leaks, but the body says symlinks are rejected. Separately, at line 418 a BOM-only or zero-width-only note passes the nonempty check. Reject symlinks before the skip, and strip \ufeff and \u200b before the nonempty check.
• skills/formalize/SKILL.md:119 an article link to ../.implementation-notes/<id>.md passes check and renders as a dead link. Add "and never links its note".
• autoform_cli/graph.py:377 the note tests cover only the misnamed, orphan, empty and alias cases. Add rows for a symlinked note, a symlinked directory, <id>.txt, non-UTF-8 content and a .DS_Store positive case.
• autoform_cli/templates/github/workflows/autoform-verify.yml:39 generated CI runs check and render, never audit, so the body's "audit enforces cleanup" overstates it. README:87 ("reports") is accurate. Fix the body.
• autoform_cli/README.md:13 lines 13-16 reflow unchanged text; revert them. Reflow the ragged new lines: README:85 (49 cols), README:1091 and 1093 (39), formalize SKILL.md:62 (30) and 65 (36), roadmap SKILL.md:94 (85).

Checked, no change needed

• Notes live outside roadmap/, so coverage cannot cite them. Render, the structure pages and publication_source_revision omit the directory. Base 4c80749 check and render ignore it, so no AUTOFORM_REF migration is needed.
• Moves keep notes valid because notes are keyed by article_id. Uppercase IDs, .MD, nested directories, symlinked notes or directories (except hidden ones, see Nits), invalid UTF-8 and whitespace-only content are rejected.
• Failing closed in load_graph matches how other graph errors behave. Only the deletion guidance and the README wording need to change.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Re-checked at c2528c7. All four should-fix items from the review of f13757c5 are fixed, and each fix has a test that fails without it. Nothing blocks the merge.

• Note errors are now reported at the note's own blueprint path (audit.py:560). test_audit_reports_invalid_note_at_its_blueprint_path fails 3 of 3 when that branch is removed.
• The revision contract keeps the record in the revision commit and report, and uses a note only while its article is unproved.
• Roadmap deletes the note on proof, on mathlib: true, and in the commit that deletes or merges the article. The README now says every command that loads the graph rejects bad notes.
• test_audit_allows_implementation_notes_while_work_is_unproved fails when the proved guard at audit.py:186 is dropped.

The nits are closed too:

• an article parse error no longer reports its note as orphaned;
• symlinks are rejected before the dotfile skip;
• BOM-only and zero-width-only notes count as empty;
• both skills say never to link the note;
• the five missing fail-closed cases have tests;
• the body says audit "reports";
• the README reflow at line 13 is reverted, and the ragged lines are reflowed.

Optional golf, still open

• tests/test_graph.py:527, tests/test_render.py:1048-1050 and 1058 (then assert == before at 1062), and tests/test_skill_examples.py:125 guard the abandoned agents.md design; main has no agents.md handling.
• Five note tests in tests/test_graph.py (577, 596, 613, 630 and 652) build the same one-article blueprint in 8 lines each. One _note_blueprint(tmp_path) helper would remove about 25 lines.
• tests/test_skill_examples.py:72 is implied by line 107. Line 110 pins the rationale sentence at skills/formalize/SKILL.md:124-125, which repeats README:80-83.
• autoform_cli/graph.py lines 379, 386, 407, 412 and 422 still wrap issues.append calls that fit on one line.

Validation at c2528c7: test_audit 29, test_graph 69 and test_skill_examples 26 pass locally. Both mutations above were run against those tests. The CI test jobs are green; real Lean was still running at the time of writing.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Supersedes the “not ready” review of f13757c5: #172 (comment)

Final exact-head review at c2528c7a: ready for human review. The follow-up fixes:

• preserve complete blueprint-relative diagnostic paths for malformed note filenames, including spaces and colons;
• keep revision outcomes in the revision commit/report when touched articles remain proved, using implementation notes only for unproved work;
• require Roadmap to delete notes on proof/mathlib: true and atomically with article deletion or merge;
• verify that unproved work may retain a note and that proved work may not;
• avoid false orphan findings while an article itself is malformed;
• reject symlinked directories/files, malformed extensions, invalid UTF-8, BOM/zero-width-only notes, and orphan notes while allowing .DS_Store;
• forbid links from mathematical articles to hidden notes.

Validation at this exact head:

• focused graph/audit/render/visualization/skill suites: 226 passed;
• Ruff, git diff --check, and make check-example: pass;
• Formalize and Roadmap skill validation: pass;
• all exact-head GitHub checks pass, including Windows and both real-Lean jobs;
• independent code and architecture re-reviews: approved with no remaining blockers.

[Deicyde]

Gap in the stale-note audit: stale-implementation-note fires only when status.derive(graph)[node].proved, and proved is per-node (status.py:111: formalized proof, Mathlib, or a stated definition). A chapter or other container article is never proved, so a note keyed to its article_id is never flagged and can stay forever.

In hartshorne and hatcher-at, the 9 Lean-side notes left after cleaning proved articles are all on chapter READMEs, and some are already stale.

Possible fix: flag a container's note once every article it contains is proved.

[Deicyde]

Supersedes the container stale-note gap reported here: #172 (comment)

Fixed at exact head b032c03f. Container notes are now stale when the container has at least one formalizable descendant and every such descendant is derived proved; a container with any unfinished formalizable descendant may retain its note.

The roll-up is computed once, bottom-up and iteratively. A 1,200-level containment regression verifies that the audit does not recurse or rescan each subtree.

Validation at this exact head:

• focused graph/audit/render/visualization/skill suites: 229 passed;
• dedicated audit/skill suite: 58 passed;
• Ruff, git diff --check, and make check-example: pass;
• all exact-head GitHub checks pass, including Windows and both real-Lean jobs;
• independent code and architecture reviews: approved with no remaining blockers.

#172 is ready for human review.

[Deicyde]

Correction to my earlier comment: its suggested fix ("every article it contains is proved") misses 5 of the 9 book notes, because sub-container READMEs and other non-formalizable pages don't derive proved. The subtree rule in b032c03f is the right one: with the 9 chapter- and section-level notes in hartshorne and hatcher-at converted to .implementation-notes/ files, b032c03f flags all 9; c2528c7a flagged none.

Two gaps remain at b032c03f:

1. Nothing tells Formalize to delete a container's note. The PR that proves a container's last formalizable descendant creates stale-implementation-note on the container, but the skill keeps the worker to the claimed article (formalize/SKILL.md:64-65, :118-126) and its findings (:133-137); only Roadmap has the container rule (roadmap/SKILL.md:76-77). autoform doctor fails on the finding, so in a book whose CI runs doctor (hartshorne's does), that PR fails unless the worker leaves the skill's scope. If two PRs finish a container in parallel, the finding first appears on main, where Formalize only reports it. Suggest: Formalize deletes any container note the audit reports as stale.
2. README.md:1093-1094 still limits a note to "while that article remains unproved", which never ends for a container, and :85-86 drops the code's "at least one formalizable descendant" condition.

[Deicyde]

Fixed the two gaps from the comment above:

1. f6a9bb7 has Formalize delete every note the audit reports as stale-implementation-note, including a container's note its proof completed or an earlier commit left behind (formalize/SKILL.md:137-141), and re-run the audit after integrating, so a container finished by two parallel PRs doesn't land with a stale note (:144-146). Line 66 now lists this as an exception next to revisions.
2. The README note rule and the Roadmap skill now say "every formalizable descendant is proved and there is at least one" (README.md:85-87, roadmap/SKILL.md:76-77), and the revision contract links to that rule instead of "while that article remains unproved" (README.md:1094-1096). A new audit test pins the at-least-one case.

Separately, 3e95335 fixes a clash with main: #171 changed _ArticleShape to take the statement text, so the deep-containment test failed once merged with main (AttributeError: 'bool' object has no attribute 'splitlines'). It now passes a string, which works with and without the merge.