[Deicyde]

Problem

Users install Autoform from main's moving head, so every merge ships to them. The version has been 0.5.0 since Aug 28, and the only tag is v0. Jack asked for a 0.6.0 release that users install from a tag.

Change

• Version 0.6.0 in pyproject.toml, uv.lock, the Claude and Muse manifests and the base of Codex's cachebuster version, which gets a fresh stamp, as tests/test_release.py requires.

• CHANGELOG.md. Unreleased becomes "0.6.0 (2026-10-22)", above a new, empty Unreleased heading. It now covers the 236 merges since 0.5.0:

  • the 12 merged on Oct 21 that Add autoform --version, a release-version check, and a changelog #397's text predates (Scale roadmap inventories and the full DAG explorer #90's explorer and module catalogs, Add autoform site check for what a site's build broke #401, Deploy Pages only from the commit autoform verify passed on main #399, Speed up claim list and shorten impact's stale-build error #427 and the rest);
  • a batch from Oct 17 and 18 that it skipped;
  • older user-facing changes it left out;
  • Skip the dependency explorer's parameter fragments in site check #438, Retire generated Mermaid: a Markdown dependency summary and locked-down authored diagrams #378, Verify the library probe on Lean 4.35.0 #440, Report autoform audit's findings in the generated Pages workflow #437 and Clean up the dependency explorer's design #411, which merged while this PR was open. Report autoform audit's findings in the generated Pages workflow #437's Unreleased line moves into 0.6.0, as agreed with its author.

  The schema list names autoform-runtime/v4 and autoform-publication/v3, which Scale roadmap inventories and the full DAG explorer #90 moved to.

• The README installs v0.6.0:

  • Claude Code with facebookresearch/autoform-bot@v0.6.0: the marketplace parser in Claude Code 2.1.220 accepts owner/repo@ref and owner/repo#ref;
  • Codex with --ref v0.6.0;
  • Muse Code with a #v0.6.0 suffix on its source, quoted, which Muse's marketplace parser accepts.

  It also says how to move an install that follows main onto the release, and how to keep following main.

• tests/test_release.py checks that the README's installers name the version's tag, reading only the Installation section's command blocks, so a release cannot leave them behind.

• CI pins from a Claude Code tag install. Claude Code installs a ref with git clone --depth 1 --branch v0.6.0, which leaves no refs/remotes/, so plugin_pin found nothing, and init and project new skipped CI. (Muse Code clones the same way, but plugin_pin already found no pin in Muse's snapshot layout before this release, so that gap is unchanged.) A tag now counts as evidence for the one remote whose fetch refspec writes it by exact name. A tag that several remotes claim counts for none, and so does any tag when a remote's name is not read. The pin is still HEAD's full SHA. Tests build real depth-1 tag clones in both clone shapes.

• Upgrading from 0.5.0 and corrected notes, from jackmccarthy-77's line-by-line check: links to the per-statement pages 404, the checks that now fail where 0.5.0 passed, the Pages deploy change, Treat every published page as untrusted #215's TeX lockdown, the default debrief, and the REPL's process per call.

After merge

I push a lightweight tag v0.6.0 on the merge commit right away. An annotated tag would make Codex re-clone the marketplace on every start, and the existing v0 tag is lightweight too. Then I publish a GitHub release with the 0.6.0 section as its notes. The README's commands fail until the tag exists, so the tag follows the merge within minutes.

Test

• tests/test_release.py (7 tests) and the README test pass, run directly.
• uv lock --check passes.
• CI runs the full suite.
• Main is red until Skip the dependency explorer's parameter fragments in site check #438 lands, so merge this after it.

[Deicyde]

Review: ready to merge once CI finishes (reviewed at 8ac33ad). Nothing blocks merge.

• The version is 0.6.0 in pyproject.toml, uv.lock and all three manifests, and tests/test_release.py now also checks that the README's installers name the release tag.
• Every PR the 0.6.0 section cites (144) is merged, and none of the open PRs (Add statement-review commands #284, Show statement review on the site #217, Label statement approvals by the repository's code-owner review policy #219, Retire generated Mermaid: a Markdown dependency summary and locked-down authored diagrams #378, Clean up the dependency explorer's design #411, Report autoform audit's findings in the generated Pages workflow #437) is listed. The section also takes the entries Add autoform --version, a release-version check, and a changelog #397's review asked for (dashboard, the hidden implementation notes, --version).

Notes:

• The README's three installers point at v0.6.0, which exists only after the tag is pushed, so main's README is wrong until then. Push the tag right after the merge, as the description plans.
• The owner/repo@ref form for claude plugin marketplace add and the #v0.6.0 source for Muse could not be run from here. Run each installer once against the tag, before announcing the release.
• Add read-back cards and the testimony validator #216 (merged) is not in the changelog. That is right while it has no user-facing surface; it gets its line with Add statement-review commands #284.
• Report autoform audit's findings in the generated Pages workflow #437 adds a changelog line under Unreleased; whichever of the two lands second moves it.

Posted by Claude Code (348 worker session).

[Deicyde]

CHANGELOG line check at 6d4d590: what's wrong. This is one round, and only my part, so it isn't a second verdict. Every bullet and sub-bullet was checked against its cited PRs and today's main, from 0.5.0's point of view.

The 236 count checks out at this head, and so do the lines added for #378, #440, #437, #411 and #438. The problems below are in lines that were already there.

Blocks merge

These tell someone upgrading from 0.5.0 the opposite of what happens.

1. Old dependency links (Dependency explorer). "Old /dependencies/full.html#node= links still resolve" does not apply to 0.5.0 sites, which have no #node= links: that format arrived with Scale roadmap inventories and the full DAG explorer #90.

   • What 0.5.0 sites have is a per-statement page, dependencies/nodes/<id>.html, linked from every statement card. Scale roadmap inventories and the full DAG explorer #90 deleted those pages, so those links now 404. autoform_cli/README.md (the explorer section, and Upgrading item 8) says so.
   • Suggested: "0.5.0's per-statement dependencies/nodes/<id>.html pages are gone, and links to them no longer resolve. A statement's dependency link is now <scope>.html#node=<id>, and a dependencies/full.html#node=<id> link redirects to the smallest scope holding the node." Add the removal under Removed too.

2. CI audit. "Elaboration limits" is credited to the generated verify workflow (Report unbounded and file-wide elaboration limits in the audit #264), but Report unbounded and file-wide elaboration limits in the audit #264 added those findings to autoform audit --lean-root only. The verify workflow never runs that check. Since Report autoform audit's findings in the generated Pages workflow #437, the Pages workflow's audit step lists them in its log, report-only. Move the clause there.

3. "Commands inform; they do not break a codebase." A repository that passed 0.5.0's check can fail 0.6.0's. Each of these passes at 0.5.0 and exits 1 on main:

   • a Sources link that names no file (Make check reject Sources links that name no file in the blueprint #287);
   • a dependency on a hidden page, or a Sources link to ../structure.md (Make check and audit see the blueprint render publishes #380);
   • a Sources link that steps through a hidden folder (Reject a link that steps through a hidden folder and back out #409, merged after Write down that Autoform's commands inform and never break a codebase #394's rule);
   • a name declared with a universe binder (def f.{u}) in one file and plainly in another (Scale roadmap inventories and the full DAG explorer #90).

   Say that the rule holds since Let work and search omit what they can't represent, and have check warn #325, isn't retroactive, and has these exceptions. Make Checks say these rules fail check, and so both generated workflows, instead of telling them as history.

4. Unpublished folders. published: false works only in the README.md of a folder below roadmap/. Elsewhere it is silently ignored: in blueprint/sources/README.md, which the scaffold ships, check passes and render publishes the folder. A published article's link into the folder also fails check. Say "a folder below roadmap/", and say to remove the parent's link first.

5. Pages deploys (Deploy Pages only from the commit autoform verify passed on main #399).

   • "Manual runs still build without deploying" is wrong: a manual run deployed in 0.5.0, and now it doesn't.
   • A project scaffolded by 0.5.0 keeps its old push-triggered workflow after bumping AUTOFORM_REF. It gets the verify gate only after deleting blueprint-pages.yml and rerunning autoform init. Say both.

6. "Diagnostics barriers" (Wait for Lean's diagnostics barrier instead of a quiet gap #256). Check diagnostics with one lake lean run per call #283 and Delete the language server's diagnostics path #306 deleted that mechanism, and the Removed section lists Delete the language server's diagnostics path #306's removal, so the two lines contradict each other. The change users meet goes unsaid: lean_diagnostic_messages runs one lake --no-build lean per call, so it reports unbuilt or stale imports instead of building them as 0.5.0 did (Check diagnostics with one lake lean run per call #283, Tell callers to build the file's imports, not Lake's short list #364).

7. Raw HTML (fix(render): preserve mathematical bodies and Markdown validation #362). "Bodies keep their ... raw HTML" was reversed by Treat every published page as untrusted #215: raw HTML now makes the statement, or the page, publish as typed, escaped in one block. The Security bullet states Treat every published page as untrusted #215's behaviour, so the two contradict each other. Drop "raw HTML" from the fix(render): preserve mathematical bodies and Markdown validation #362 line.

8. Contracts. Scale roadmap inventories and the full DAG explorer #90 also moved autoform-coverage from v1, the version 0.5.0 shipped, to v2: INVENTORIED is a new disposition, and counts always has its key. The coverage object is in publication.json and audit --json, so a consumer reading this paragraph misses the contract it parses. Also replace "on main", which goes stale in a tagged release.

9. Claude Code's tag install loses CI in new projects.

   • Claude Code clones a ref with git clone --depth 1 --branch v0.6.0, which leaves no refs/remotes/origin/*.
   • scaffold._remote_contains_ref accepts only refs/remotes/<remote>/ refs, so plugin_pin returns nothing.
   • autoform init and autoform project new then leave out autoform-verify.yml, blueprint-pages.yml and autoform_audit.py and print "CI was not written".

   Either accept the clone's exact local fetch destinations, such as refs/tags/v0.6.0, in _remote_contains_ref before tagging, with a test that clones a tag at depth 1, or add a README caveat beside the Claude Code command.

Notes

• Upgrading from 0.5.0's site.
  • Render refuses to replace the autoform-publication/v1 site 0.5.0 wrote ("delete it once by hand", Publish blueprint sites transactionally #165).
  • The Contracts line "render still replaces a v2 site" concerns only people who tracked main.
  • The dashboard reports any pre-v3 site as stale.
• Treat every published page as untrusted #215's TeX change. Formulas can't define notation anymore: \newcommand, \def, \DeclareMathOperator, \label, \color, \cancel and \href show in red. Render replaces an edited blueprint/javascripts/mathjax.js, with a warning, and project macros go in blueprint/tex-macros.json. Without a note, 0.5.0 blueprints publish red errors after upgrading.
• Feedback. Setup, Roadmap and Formalize now end with an orchestrator debrief, on by default; AUTOFORM_DEBRIEF=0 turns it off. Subagent debriefs are opt-in. Say both.
• REPL (Isolate and validate public REPL calls #105, Validate REPL imports with the selected Lean toolchain #106).
  • run_lean_code starts a fresh Lean process per call, so nothing carries over and every call pays for its imports.
  • The default LEAN_REPL_CMD is now lake exe @repl/repl.
  • "Isolated public REPL calls" understates this.
• Dependencies. The section omits:
  • markdown pinned to 3.10.3, and pymdown-extensions to 11.0.1, a major version up from 10.x (Fix roadmap loading, Lean index edge cases and undecodable JSON #212);
  • the Pages workflow's mkdocs-material 9.7.7 (Fix roadmap loading, Lean index edge cases and undecodable JSON #212);
  • tomli as a new runtime dependency (Harden project compatibility inspection snapshots #79).
• Removed. autoform unused-hypotheses never shipped in a release: Add autoform unused-hypotheses: report hypotheses a proof never uses #198 added it after 0.5.0, and Remove autoform unused-hypotheses in favor of Batteries' unusedArguments linter #352 removed it four days later. The user-facing change is the Batteries unusedArguments lint step in Formalize and Agent Review.
• Not said anywhere.
  • The Formalize skill itself is new since 0.5.0.
  • project new --library atlas, and Setup's ATLAS offer, are missing from Projects.
  • The citation warning that Warn about library declarations that cite the blueprint's sources #379 and Let source pages silence library citation warnings, and group module hits #400 added to check --lean-root is cited but not described.
  • The INVENTORIED disposition and the catalog CI-pin step are missing from Module catalogs.
• Small accuracy fixes.
  • autoform-search/v2 is only the --library output; plain search --json is still v1.
  • migrate article-ids --write needs its BLUEPRINT argument.
  • navigation: can be set on any container.
  • The new CI audit reaches an existing project only if it replaces its two local files together.
  • Document running several sessions on one project #420 is cited for claims guidance it doesn't add.
  • Index Batteries' wanted commands and keep them unproved #278 changes the project's own Lean index, not library search.
• Install text.
  • "Leave out the version" leaves Codex with a bare --ref.
  • owner/repo@ref needs Claude Code 2.1.71 or newer, and the README states no minimum.
  • Between the merge and the tag push, the commands fail. Claude Code reports that as an SSH error.
  • The new README test also passes when a pinned command sits outside the install blocks.

Posted by jackmccarthy-77, the changelog-line check the lead assigned.

[Deicyde]

Back to draft until jackmccarthy-77's nine blocking findings are fixed. The most serious is that a tag install through Claude Code or Muse Code would make init and project new skip CI, because a depth-1 tag clone has no remote-tracking ref for plugin_pin. That fix has to be in the tagged code. The other eight are changelog lines that tell a 0.5.0 user the opposite of what happens. Fixes are in progress, and I'll ask for a check of just those.

[Deicyde]

Fixes for jackmccarthy-77's nine blocking findings are in, at a6beec3:

• 9, tag installs lost CI: afd2a04 and 830d5fa let plugin_pin pin a depth-1 tag clone (the Claude Code and Muse Code shapes). The tests build real tag clones and guard against over-acceptance.
• 1-8, changelog lines: d600204 and a6beec3. The README's install text is in 1fc4e61.
• Also fixed, from a verification pass: the duplicate-name rule (Select the public Lean declaration among duplicates and report ambiguous names #348) and the symlink rule (graph: refuse roadmap symlinks at load time instead of hanging #197) are now listed under Checks that fail.

Notes left out, on purpose:

• Blocker 9 (the Claude Code tag clone loses CI): another agent owns it in code. I did not add a README caveat, so that agent's fix still decides whether one is needed.
• The note that the commands fail between the merge and the tag push: this is about release timing, not text a released README should carry.
• The catalog CI-pin step in Module catalogs: it doesn't fit in one accurate clause next to the rest, and the Roadmap skill and CLI README already cover it.
• Did not add the full TeX list (\bbox, \unicode, \require, ...). 'and the like' plus tex-macros.json is enough for an upgrader. I also avoided claiming check warns about every turned-off command, since the README only confirms definitions and \label.
• Did not rewrite pre-existing lines the review didn't flag, such as whether every cryptography/pyjwt bump or every Tell callers to build the file's imports, not Lake's short list #364 citation is placed in the ideal group.
• Kept the '236 merged pull requests' count, which the reviewer confirmed.

jackmccarthy-77 is checking the blocker fixes only.

[Deicyde]

Blockers-only check at a6beec3: all nine are fixed, and nothing blocks merge.

• 9 (tag install loses CI). Fixed, checked with real git against a bare repo with a tag:

  • Claude Code 2.1.220's own clone command, read from its bundle, pins the tag's commit for lightweight and annotated tags, and after its update steps. End to end, autoform init writes autoform-verify.yml, with AUTOFORM_REF set to the tag's commit, plus blueprint-pages.yml and autoform_audit.py.
  • Codex pins through refs/remotes, as before. Branch clones are unchanged.
  • Two remotes claiming the tag, an unread remote name, a glob tag refspec, a local commit on top of the tag, and HEAD behind the tag all stay safe.
  • The 30 tests selected by -k "pin or tag or remote" pass.

• 1-8 (CHANGELOG). Each corrected line was checked against 0.5.0 (00a3cbd) and main, and the four "Checks that fail" cases were run through both versions' check. The text is accurate:

  • the per-statement pages and their redirect;
  • elaboration limits now credited to the Pages audit step;
  • "Commands inform" with its exceptions;
  • published: false below roadmap/ only;
  • the Pages deploy and refresh advice;
  • the Diagnostics bullet;
  • no raw-HTML claim;
  • runtime, publication and coverage in Contracts.

  The Upgrading section matches the README's own upgrade notes.

Notes, none blocking:

• Checks that fail omits Bind Lean source snapshots to filesystem generations #95's --lean-root refusal of a .lean file that is a symbolic link. A project with one passes 0.5.0's Pages check and fails this one.

• The README release test checks the three install blocks but not the prose fallback ('facebookresearch/autoform-bot#v0.6.0' on line 34), so a 0.7.0 bump can leave older Claude Code users on 0.6.0. Also, the #ref fallback needs Claude Code 2.0.28 or newer.

• The PR description says the CI pin fix covers Muse Code. It doesn't: plugin_pin still finds no pin in Muse's marketplace layout (…/muse/plugins/marketplaces/<name>/source). That predates this PR, and the README makes no such claim. Limit the description's claim to Claude Code.

• _exact_tag_destinations hardening.

  • A second remote's undecodable or oversized fetch list returns no claims, so origin still gets credit for a tag that remote overwrote. Treating a decode failure as "no tag counts" matches 830d5fa.
  • Three guards have no test: the decode guard, the exact name match, and the refs/tags/ restriction. Four single-point mutants survive.
  • The comment and docstring read as if a locally moved tag never counts. It does, under the refspec's name.

  All of these need deliberate git work inside the marketplace clone, and the bad pin then fails loudly in CI. Pin checks based on local refs already had this exposure.

• Wording.

  • The Select the public Lean declaration among duplicates and report ambiguous names #348 line says "declared in more than one file", but the rule is "declared more than once unless exactly one declaration is public".
  • Only audit, not check --lean-root, refuses a wanted target that backs a proof.
  • "Rerun autoform init" should add "or with --autoform-ref <sha>" for an install that cannot pin.

Posted by jackmccarthy-77, the blockers-only check the lead asked for.