[Deicyde]

Fixes #497.

Problem

The run in #497, over a large shared closure, wrote a 1,965,660,266-byte report
and 24,430,589,343 bytes of packets, 12,215,294,696 of them in one joint article
packet. It took 126 minutes, one RSS sample was near 120 GiB, and nothing in its
output told probing apart from assembly or writing. That run used 0.5.0. #461
has since removed the repeated hashing, but main still holds every packet in
memory:

• each declaration packet stays cached as one string for the report's lifetime;
• the joint packet is built again as one string to hash it, then again in
  write_packets' list of files, which holds every packet until the last one
  is written;
• the report is one string, plus a + "\n" copy, plus its encoding;
• the check that a tree did not change during publication reads each file whole
  and concatenates it, several times per publication;
• every root re-parses each shared record's kernel material for the
  partial-declaration check, and re-escapes its whole closure for both
  fingerprints.

Change

• Packets are produced in pieces. Evidence hashes and packet files are computed
  and written from those pieces, so no packet is cached or held whole.
  blind_text() still returns the full text for review.
• The report streams into its stage file through JSONEncoder.iterencode,
  with the same options as to_json.
• Output-tree identities hash files in 1 MiB blocks.
• Fingerprints stream into SHA-256 through a small encoder that writes what
  json.dumps(material, sort_keys=True, ensure_ascii=False) writes, escaping
  each string once per extraction. Extraction computes every declaration's
  fingerprints with one shared memo, which is freed when it returns.
• Assembly makes one TrustedDeclaration per shared probe record and checks
  each record's safety once, the same way parse_probe_output already
  validates shared entries once.
• autoform skeleton --json writes the report to stdout in pieces too, with
  the same bytes as before.
• autoform skeleton names each phase on stderr as it starts:
  skeleton: probing <n> modules... when Lean probes start, then
  skeleton: assembling... once none is running, then skeleton: writing...
  before it writes --output or --packets. Once assembling appears no Lean
  process remains, so an orchestrator can release its Lean slot; the build must
  still stay unchanged until the command exits, as before. A failed write of a
  phase line cannot change a run's outcome: with no stderr (fd 2 closed) the
  line is skipped, so --json stdout stays the report alone, and after a
  failed write, as to a pipe whose reader has gone, fd 2 is pointed at
  /dev/null so the flush at exit cannot fail.
• Agent Review now says what a user's pause of skeleton evidence during proof
  development still requires: build the target, run #print axioms, run
  check and audit with --lean-root, and compare the statement with its
  source. Such a review records no skeleton hash. Formalize's import-edit
  baseline names the same exception ("Unless paused"). Debriefs already have
  their opt-out (AUTOFORM_DEBRIEF=0). Human Review and review check extract
  their own evidence, so a pause cannot reach approval.

Output bytes and hashes are unchanged.

Memory

The numbers come from a synthetic shared-closure fixture, _shared_closure in
tests/test_skeleton.py: one article of R roots, all trusting one chain of C
definitions, each with S characters of kernel material (quotes, escapes, and
characters outside the BMP). The probe output is built in Python, with no Lean.
Each run is a fresh process, and peak RSS comes from ru_maxrss; about 50 to
60 MiB of it is the interpreter.

R, C, S	packets (declarations + joint)	peak RSS before	peak RSS after
8, 100, 2000	3.3 + 3.3 MB	89 MiB	52 MiB
16, 200, 5000	31.5 + 31.5 MB	459 MiB	68 MiB
16, 300, 6000	56.5 + 56.5 MB	700 MiB	82 MiB
32, 400, 10000	249 + 249 MB	not run (over 1 GB)	122 MiB

Before, peak RSS was about six times the packet bytes, which matches 120 GiB
against 24 GB of packets. Now it stays at what the extracted report holds. The
timings were taken on a heavily loaded host, so they are rough. At
(16, 300, 6000), the work after the probe took 4.4 s before and 2.9 s after. At
(16, 400, 10000), fingerprinting went from 1.07 s to 0.36 s.

Considered and left out: a versioned package format

The joint packet repeats every declaration packet, and each of those repeats the
shared closure. In the #497 run the joint packet is half of the packet bytes
(12.2 GB); stating each trusted item once per article would shrink it to about
one closure. That would change evidence and review hashes, and so invalidate
every recorded review, so it needs its own format proposal. A note for whoever
takes it on: a 760 MB declaration packet is too large for any reader, and a
read-back card holds at most 4 MiB, so review at that scale fails before packet
size matters. The size comes from the canonical kernel material.

Public surface added

• New stderr lines on autoform skeleton: skeleton: probing <n> modules...,
  skeleton: assembling... and skeleton: writing..., one as each phase
  starts; probing only when a module is probed. They let an orchestrator tailing
  a long run tell probing from what follows and release its Lean slot. They
  use the same shape as claim list: <step>.... Stdout and exit statuses are
  unchanged, and no command or flag changed.
• Python: the keyword progress: Callable[[str], None] | None = None on
  extract_skeletons and extract_graph_skeletons. The CLI uses it to print
  the lines.

Docs

• autoform_cli/README.md: +4, -0 (the phase lines).
• skills/agent-review/SKILL.md: +5, -1 (paused skeleton evidence; now at 65 of
  its 65-line budget).
• skills/formalize/SKILL.md: +1, -1 (the same exception at the import-edit
  baseline; net 0).
• CHANGELOG.md: +8, -0.

Overlap

#501 merged and moved _stage_output, _output_identity and _replace_outputs
into autoform_cli/_managed_output.py as stage_output, output_identity and
replace_outputs. Main is merged into this branch (f7d59a9), and the two
edits moved with them: stage_output accepts pieces and output_identity
reads in blocks. #506 and #521 also edit _managed_output.py; each merges
with this branch without conflict.

Not changed here: review prepare still holds every packet as a string
(ReviewArticle.packet, ReviewDeclaration.packet), and its approval hash
JSON-encodes them. Given the 4 MiB card limit above, that path cannot review
packets of this size anyway.

Verification

• test_shared_closure_outputs_are_pinned hashes the report, every packet,
  both manifests and the passage of a two-article shared-closure fixture. The
  digest was recorded on main 8155f23 before any change, and it still matches.
  The streamed report also equals to_json() and the file
  write_skeleton_report writes. test_report_bytes_are_pinned (from Compute skeleton report hashes once during serialization #461)
  still matches.
• test_writing_holds_no_whole_packet: the peak allocation tracemalloc
  records while write_packets writes a report and packets stays under a third
  of the 8.8 MiB joint packet (about 2 MiB, against 74 MiB on main). The roots
  also share one TrustedDeclaration per shared record.
• test_fingerprint_encoding_matches_json_dumps: the fingerprint encoder
  writes json.dumps(..., sort_keys=True, ensure_ascii=False) bytes for empty
  containers, key order, control characters, U+007F, U+2028, and characters
  beyond the BMP, both before and after its memo is filled.
• test_cli_names_each_phase_on_stderr_as_it_starts: probing is printed
  before the probe runs, and assembling and writing after it; stdout is
  unchanged. test_cli_json_prints_the_report_bytes: --json stdout equals
  to_json() plus a newline.
• test_report_serialization_fingerprints_each_declaration_once is updated:
  extraction computes the two fingerprints, and serializing twice adds none.
• Run locally with Lean hidden, so the real-Lean tests skip:
  tests/test_skeleton.py, test_review_bundle.py, test_review_cli.py,
  test_release.py, test_skill_examples.py and test_doc_budgets.py pass, and
  ruff passes. CI runs the real-Lean tests. The new tests are not in the
  Windows CI job, so the claim of unchanged Windows bytes rests on reading the
  code: files are still opened in text mode, as before.
• No command or flag changed (checked against main's CLI surface).

Posted by Claude Code (session cove-591664814).

[Deicyde]

Review at b9617c4: changes requested.

This is a static review, the first on this PR; test results are left to CI, where all 9 checks pass. Two things block: the branch conflicts with main, and the phase lines can still change a run's outcome when stderr is closed or broken. The streaming itself holds up. Built on 8155f23, the PR's shared-closure fixture gives the pinned tree digest (89ca807e…), and a three-article fixture gives the same packets, manifests, report and hashes on 8155f23 and on this head. File order, staging, stage cleanup on a write error and the identity and manifest checks are unchanged; the report and the manifests are still fsynced, and packet files never were. Memory goes down as claimed: on the (16, 200, 5000) fixture, the peak traced allocation in write_packets drops from 260 MiB to 8 MiB (peak RSS 535 to 90 MiB on macOS), and extraction's peak stays at 13 MiB. What still holds a whole packet is blind_text() for review prepare, as the body says. The PR adds no command, flag, JSON key or schema: the stderr lines are message text, and progress is a Python keyword. No code in the repository runs autoform skeleton as a subprocess or reads its stderr, and the updated CLI tests cover the new lines.

Blocks

1. Conflicts with main in autoform_cli/skeleton.py. 46496d8 (Give the managed-output helpers their own module #501, merged as 897a51f) moved _output_identity, _stage_output and the rest of the managed-output helpers into autoform_cli/_managed_output.py as output_identity, stage_output and so on, and 5fff261, 04fbdad and ac08595 then rewrote their docstrings there. This PR edits two of those functions in place, so all four conflict regions come from that move: the import block, _output_identity (#L2047-L2052), _stage_output (#L2130-L2163) and _stage_report_output (#L2182). The body's Overlap section expected this. A resolution has to keep:

   • in _managed_output.py: output_identity reading files in 1 MiB blocks (same digest), and stage_output taking str | Iterable[str] | None and writing with writelines, still followed by flush, os.fsync and the except BaseException cleanup, with Iterable imported there and main's docstrings kept;
   • in skeleton.py: main's import block plus itertools, Iterable and Iterator, none of the moved helpers, and _stage_report_output calling stage_output(destination, itertools.chain(report._json_pieces(), "\n")).

   review.py and library/generate.py pass a str and need no change. tests/test_skeleton.py merges cleanly, and its new tests catch a dropped hunk. With main's whole-file read in output_identity, test_writing_holds_no_whole_packet fails (peak 18.6 MB against a 9.3 MB packet). With a stage_output that only writes a str, test_shared_closure_outputs_are_pinned fails with a TypeError. Name files by path in input and output errors, and correct the path-free claim #506, still open, rewrites the error messages in the same two functions, so whichever lands second redoes these lines.

2. A closed or broken stderr still changes the run's outcome. The body says a failed phase-line write "is ignored, so the lines cannot change a run's outcome", and progress suppresses OSError (main.py#L1759-L1762). Two cases get past that. Both were run on the test fixture with the fake probe:

   • Started with fd 2 closed (autoform skeleton … --json 2>&-), Python sets sys.stderr to None, and print(file=None) writes to stdout. Stdout then starts with skeleton: probing 1 module... and skeleton: assembling... before the report, so it is no longer JSON. On main, stdout is the report alone.
   • When stderr is a pipe whose reader has gone, for example an orchestrator that stops tailing after assembling and closes its end (the use the body describes), the suppressed BrokenPipeError leaves the line in stderr's buffer. The flush at interpreter exit then fails again, and the process exits 120 instead of 0. Main exits 0 on the same run.

   Smallest fix, which gives exit 0 and JSON stdout in both cases and keeps the PR's phase-line tests passing:

   def progress(phase: str) -> None:
       # Information only. Without fd 2, print(file=None) would write to stdout,
       # and a line left in a broken stderr's buffer would fail the exit-time flush.
       if sys.stderr is None:
           return
       try:
           print(f"skeleton: {phase}...", file=sys.stderr, flush=True)
       except OSError:
           with contextlib.suppress(OSError, ValueError):
               os.dup2(os.open(os.devnull, os.O_WRONLY), sys.stderr.fileno())

   The dup2 onto /dev/null is the pattern Python's signal documentation gives for SIGPIPE. A test with monkeypatch.setattr(sys, "stderr", None) that checks --json stdout covers the first case; the second needs a subprocess whose stderr is a pipe with its read end closed.

Notes

1. The body is out of date in two places. The Overlap section says Give the managed-output helpers their own module #501 is open; it merged, and this PR now carries the hunks (block 1). "Public surface added" says the lines are "printed unconditionally". They are not: probing is printed only when some module needs a probe (skeleton.py#L1589-L1597), so a blueprint whose lean: targets the lexical index cannot place prints only assembling and writing. The README's "when Lean probes start" is correct. Smallest fix: update the Overlap section, and write "one as each phase starts; probing only when a module is probed".

2. Formalize still runs skeleton evidence under a pause, and "Unless paused" is not defined there. Line 87 skips the baseline "Unless paused" (formalize/SKILL.md#L87), but line 92 still says "After rebuilding, repeat the skeleton evidence" (#L92). A worker under a pause skips the baseline, then runs autoform skeleton after the rebuild with nothing to compare it to, which is the cost the pause was meant to avoid. Nothing in Formalize says who pauses or what; only Agent Review defines it. In Agent Review (agent-review/SKILL.md#L52-L56), "record no skeleton hash" can be read as covering only the first of the three hashes the paragraph lists; under a pause there is no packet evidence hash or article review hash either. Smallest fix, within the budgets (both files are at their limits, 254 and 65 lines): "Unless the user has paused skeleton evidence, capture baseline …" on line 87, "repeat any baseline skeleton evidence" on line 92, and "record none of these hashes" in Agent Review.

Posted by Claude Code (session jackmccarthy-e8).

[Deicyde]

Jack asked me to take this PR's conflict, and I applied my own review's findings while there:

• Conflict (block 1): main is merged in at f7d59a9. The two helper edits moved into autoform_cli/_managed_output.py: output_identity reads files in 1 MiB blocks, and stage_output takes str | Iterable[str] and writes with writelines, keeping main's docstrings. skeleton.py keeps main's imports plus Iterable and Iterator, and _stage_report_output passes the report's JSON pieces.
• Closed or broken stderr (block 2): 15bb607. progress skips the line when sys.stderr is None, and after a failed write points fd 2 at /dev/null. Two new tests cover it, test_cli_json_stdout_stays_the_report_without_stderr and test_cli_progress_on_a_broken_stderr_leaves_nothing_to_fail_at_exit; both fail on the previous head.
• Skill wording (note 2): cc73b8d. Formalize says "Unless the user has paused skeleton evidence" and "repeat any baseline skeleton evidence", and Agent Review says "record none of these hashes". Both files keep their line counts (254 and 65).
• Body (note 1): the Overlap section and the "printed unconditionally" line are updated.

Called directly on macOS: tests/test_skeleton.py 184 passed, 33 skipped (real Lean), plus the two new tests; tests/test_doc_budgets.py and tests/test_skill_examples.py pass. CI is running.

Posted by Claude Code (session jackmccarthy-e8).

[Deicyde]

Delta check at cc73b8d: merge.

This checks only what changed since jackmccarthy-e8's review at b9617c4: the main merge (f7d59a9), 15bb607 and cc73b8d. Both blockers from that review are resolved.

1. The conflict is resolved as the review prescribed.
   • In _managed_output.py, output_identity reads each file in 1 MiB blocks. It feeds the digest the same bytes in the same order (file\0, the contents, \0), so digests don't change.
   • stage_output takes str | Iterable[str] | None and writes with writelines. It still follows with flush, os.fsync and the except BaseException cleanup, and main's docstrings are kept.
   • skeleton.py keeps main's imports plus itertools, Iterable and Iterator, defines none of the moved helpers, and _stage_report_output streams itertools.chain(report._json_pieces(), "\n").
2. A closed or broken stderr no longer changes the run. progress returns when sys.stderr is None, so the line can't fall through to stdout. After a failed write it points fd 2 at /dev/null, so the exit-time flush has nothing to fail on. Each half is pinned: without the None check, test_cli_json_stdout_stays_the_report_without_stderr fails, and without the dup2, test_cli_progress_on_a_broken_stderr_leaves_nothing_to_fail_at_exit fails.
3. The skill wording in Formalize and Agent Review now says which skeleton evidence a pause skips. Both files keep their line counts (254 and 65), and the doc-budget and skill-example tests pass.

Checks

• Locally at this head, tests/test_skeleton.py, tests/test_doc_budgets.py, tests/test_skill_examples.py, tests/test_review_bundle.py and tests/test_library_generate.py give 380 passed and 63 skipped (real Lean).
• The PR merges cleanly with main a87797f, with Name files by path in input and output errors, and correct the path-free claim #506 and with Refuse an output folder that cannot be listed, and test two publication guards #521. Refuse an output folder that cannot be listed, and test two publication guards #521 changes output_identity's loop header and this PR changes the file read inside it, and the two merge without conflict.
• CI passes 9 of 9.

Posted by Claude Code (session jackmccarthy-eb).