Skip rendered sites in every Lean capture

[Deicyde]

Summary

autoform render copies every non-Markdown file under the blueprint into its
site, so a .lean file kept in the blueprint lands in the site. mkdocs build
then copies the site, publication.json included, into site/. Only render's
own Lean capture treated a folder holding a complete publication.json as
generated output; it passed that marker through an opaque_markers parameter
no other caller used. check, audit, doctor, work, search, skeleton,
runtime, impact and unused-hypotheses used the default selection (only
.git and the skeleton manifest.json), so they indexed the copies: duplicate
declarations, stale names that still resolved after the source renamed them,
and a different Lean revision from render's for the same tree. Found in the
#307 post-merge review.

This PR treats a folder holding a complete publication.json as generated
output in every Lean capture, exactly like skeleton output.

• autoform_cli/lean.py: PUBLICATION_MANIFEST, PUBLICATION_SCHEMA,
  PUBLICATION_MANIFEST_MAX_BYTES and _is_complete_publication move here
  from render.py (render already imports lean.py, not the other way round),
  and the marker joins _lean_tree_selection's default markers.
• opaque_markers is removed from snapshot_project_sources,
  _open_stable_project_sources, open_project_sources and
  _lean_tree_selection; render was its only caller (checked
  autoform_cli, servers, skills, tests).
• autoform_cli/render.py imports the names from lean.py and still exports
  them (dashboard.py and tests import them from render). It keeps
  exclude_roots=(copy_root,) and its refusal rules. The comment that claimed
  every Lean walk skipped sites is replaced by one at the capture call that is
  now true. _write_publication_manifest replaces publication.json through
  a hidden temporary file in the same folder and os.replace instead of
  rewriting it in place, so a capture never reads a truncated marker. Bytes
  and file mode are unchanged.
• autoform_cli/README.md: the stop list no longer says "for render"; every
  command skips a folder holding a complete publication.json and stops at an
  unreadable one.

Behavior changes

• Every command that indexes Lean skips a folder below the Lean root holding a
  complete publication.json (schema v1 or v2, "complete": true, at most
  8 MiB), so render and the other commands index the same files and agree on
  the Lean revision.
• Every command now stops at an unreadable publication.json below the Lean
  root, as render already did and as all commands do for manifest.json.
• An incomplete, unrelated or oversized publication.json hides nothing.
• A capture during a render skips the site being written: render
  writes a complete publication.json into its stage before it copies any
  file, and replaces it, never truncates it, when it adds the file inventory.
  Not changed here: mkdocs build empties site/ and copies files in
  name order, so site/ can hold a copied .lean file before its
  publication.json (checked with mkdocs 1.6.1); a command that indexes during
  the build can read it, and running it again afterwards gives the settled
  result. The README says so.

Tests

• tests/test_lean_sources.py::test_only_a_complete_publication_manifest_hides_its_folder:
  one tree with render-style site-src/, mkdocs-style site/, a v1 site, and
  incomplete, unrelated and oversized manifests, each over a stale .lean
  copy; asserts exactly which sources snapshot_project_sources captures.
  Fails on main (stale copies under site-src/, site/ and legacy/ are
  captured).
• tests/test_render.py::test_audit_and_render_skip_a_site_and_its_mkdocs_copy_alike:
  renders into site-src/, copies it to site/ as mkdocs does, renames the
  source declaration, renders again, then audits a lean: that names the old
  declaration. Asserts audit's Lean revision equals render's
  lean_source_revision and that audit reports lean-target-not-found. Both
  assertions fail on main.
• tests/test_render.py::test_a_capture_during_a_render_skips_the_stage_being_written:
  captures after each .lean copy during a render and asserts only the sources
  are indexed. Fails on main (the capture includes
  .autoform-publication-<hex>/Proofs.lean).
• tests/test_render.py::test_a_capture_while_render_rewrites_its_manifest_skips_the_stage:
  captures during render's final manifest write (just after an in-place write
  would truncate the file, and on both sides of the replace) and asserts only
  the sources are indexed. Fails when the manifest is rewritten with
  Path.write_bytes (the capture includes
  .autoform-publication-<hex>/Proofs.lean).
• Touched and dependent files (test_render, test_lean_sources,
  test_windows_source_boundary, test_dashboard, test_audit): 499
  passed, 5 skipped, 1 xfailed on Python 3.13 and on 3.10.
• Full non-Lean suite on 3.13 (before the manifest-replace commit): 3134 passed, 137 skipped, 1 xfailed, 48 failed.
  All 48 are in tests/test_library_generate.py with "Autoform is not
  installed": the local venv is synced with --no-install-project, and main
  fails the same 48 in that venv.
• ruff check autoform_cli servers tests is clean.

Overlap with open PRs

MAIN_REF=upstream/main ~/bin/pr_conflicts.sh on the merge of this branch
into upstream/main feec945 (the branch is based on e108ee0 and merges
cleanly into feec945). New overlaps, all with draft PRs that already
conflict with main on graph.py:

• Scale roadmap inventories and the full DAG explorer #90 (Scale roadmap inventories): lean.py 3 hunks, render.py 3,
  tests/test_render.py 1.
• Show statement review on the site #217, Label statement approvals by the repository's code-owner review policy #219, Add statement-review commands #284 (statement review stack): lean.py 2, README.md 2,
  tests/test_lean_sources.py 1.

No new overlap with any other open PR (#195, #213 to #216, #320 to #335, #337, #338).

[Deicyde]

Merge readiness: one small change requested (reviewed at f48f40a)

What holds (independent review plus CI, green on every job including Windows and the real-Lean jobs):

• check, audit, doctor, render, work and search were run on main and on this branch over trees with and without a rendered site and its mkdocs copy. Two things differ: the skipped site copies (so a stale copy no longer resolves a renamed declaration), and a new stop at an unreadable publication.json.
• The marker is strict. Only a regular file with schema v1 or v2, "complete": true and at most 8 MiB hides its folder; 26 probe trees covered the near misses. Only render writes a complete manifest, and only into an empty folder or its own site, so it cannot hide real sources.
• No caller of the removed opaque_markers parameter remains. Draft Scale roadmap inventories and the full DAG explorer #90 is the only open PR that relies on it, and the body names it.
• Windows render is unchanged. The README's mkdocs ordering was confirmed with mkdocs 1.6.1.

Change requested:

• The README says render marks the site it is writing before it copies any file, so a command indexing during a render skips it. It does write the marker first. But at the end it rewrites publication.json with Path.write_bytes, which truncates the file before writing. A capture that reads the marker in that gap indexes the stage's .lean copies; a probe reproduced it.
• Fix: write the final manifest to a temporary file in the stage and os.replace it onto publication.json, as Keep skeleton packets behind their manifest while publishing #258 does for skeleton manifests. I'll push that as a new commit.

Body nits:

• test_only_a_complete_publication_manifest_hides_its_folder fails on main at the monkeypatch.setattr, not at the captured copies.
• The body mentions a follow-up commit, an older base and an older overlap run.

It is a draft, so it needs to be marked ready before merging.

[Deicyde]

Update: change made, now ready to merge (b007a13)

• render writes publication.json to a temporary file in the stage and moves it into place with os.replace, so a capture never reads an empty marker. Both manifest writes (into the empty stage, and the final one with the file inventory) go through that one function.
• test_a_capture_while_render_rewrites_its_manifest_skips_the_stage captures at the moment the manifest is rewritten. It fails on f48f40a, where the stage's .lean copy is captured, and passes now. test_only_a_complete_publication_manifest_hides_its_folder now fails on main at its assertion, as the body says.
• Independent check:
  • Mode and bytes of publication.json are identical to before under umask 022, 077 and 002.
  • No temporary file is left when the write or the replace fails.
  • The Windows-emulated render tests pass, including a replace onto an existing manifest.
• CI is green on every job: tests 3.10/3.13, real Lean, the real-Lean skeleton suite, the real REPL, Windows and CLA. It merges cleanly with main. The body is refreshed.

Optional: the new test catches a truncating rewrite through Path.write_bytes. An in-place rewrite by another route would not trip it.

It is a draft, so it needs to be marked ready before merging.