Publish blueprint sites transactionally

autoform_cli/README.md

@@ -763,6 +763,34 @@ its local context. Point `mkdocs.yml` at `docs_dir: site-src` and enable
 `md_in_html` plus a `pymdownx.superfences` mermaid fence; see the [repository
 example](../skills/setup/assets/cabannes-thesis-project/mkdocs.yml).
 
+Publication is staged, synced, validated, and atomically exchanged with the
+previous generated site. This fail-closed transaction requires macOS
+`renameatx_np` or Linux `renameat2`, plus descriptor-relative traversal,
+advisory locking, and directory sync. Autoform exercises no-replace and
+cross-directory exchange inside its private workspace before it inspects the
+live output, so a network or local filesystem that does not implement those
+flags fails without changing the published site. Other platforms, including
+Windows, can still use the remaining supported CLI commands but cannot run
+`autoform render`; Autoform never falls back to a two-rename replacement with a
+missing-site crash window. A legacy
+`autoform-publication/v1` output is never deleted automatically. Remove it
+explicitly or choose an empty output directory once, then subsequent v2 renders
+can replace only the exact checksummed generation they inspected.
+The renderer hashes both the blueprint snapshot and the exact Lean-file
+generation used for declaration links, then rechecks both under the publication
+lock immediately before the atomic rename. That check is the publication
+linearization point; later source edits belong to the next render. Generated
+v1/v2 publication trees and private staging directories are never indexed as
+Lean source.
+Repository links are emitted only when those captured blueprint and Lean bytes
+match one locally available Git commit. Mutable ref names are recorded as that
+commit's full object ID. For dirty, untracked, or otherwise unverifiable inputs,
+the render remains local, keeps source notes in the site, records no Git ref,
+and reports a warning instead of producing a stale or missing link.
+An older v2 publication without the Lean-source hash is not eligible for
+automatic replacement; remove it explicitly or choose an empty output
+directory.
+
 ## Validation
 
 `autoform check` rejects cycles, missing targets, escaping paths,
@@ -1128,6 +1156,18 @@ credentials, logs, provider state, and agent/task state inside the blueprint
 cause the render to fail rather than silently leak them. Source and output
 directories must be disjoint.
 
-Every render writes `publication.json` with the source-content hash, Git ref,
-article and dependency counts, and available views. It contains no timestamp or
-absolute path, so identical inputs produce identical output files.
+Every render writes `publication.json` with blueprint and Lean-source hashes,
+Git ref, article and dependency counts, complete file inventory, and available
+views. It contains no timestamp or absolute path, so identical inputs produce
+identical output files. Autoform validates and syncs the staged tree before one
+atomic filesystem commit, then verifies ownership and syncs both parent
+directories. Once the commit begins, Autoform never tries to exchange a recovery
+path back into the live destination. If it cannot verify the final state or
+durability, it preserves the private workspace instead of deleting a potentially
+unique generation. It reports an exact recovery path only while the bound output
+parent is still addressable. Losing that parent path after commit is an uncertain
+publication error; the parent is checked again after workspace cleanup before
+success is returned. Other post-verification cleanup refusals leave the
+published site in place and return the retained workspace as a warning. A process
+exit immediately after exchange likewise leaves the complete previous generation
+under that workspace while the complete replacement occupies the output path.

autoform_cli/__main__.py

@@ -25,7 +25,7 @@
 from .lean import build_linker, declaration_names, index_failure_message
 from .project import ProjectCatalogError, ProjectCreateError, create_project, inspect_project, load_release_catalog
 from .render import PublicationError, render_site
-from .runtime import RuntimeProjectionError, load_runtime_graph, resolve_runtime_paths
+from .runtime import RuntimeProjectionError, resolve_runtime_paths
 from .scaffold import ScaffoldError, scaffold_project
 from .skeleton import (
     DEFAULT_PROBE_TIMEOUT,
@@ -453,7 +453,6 @@ def _dashboard(args: argparse.Namespace) -> int:
         def run(scratch: Path) -> None:
             claims = ClaimBoard(repo, "dashboard-readonly", scratch)
             state = publication_bound_live_state(
-                lambda: load_runtime_graph(paths.project_root),
                 claims,
                 blueprint_dir=paths.blueprint_dir,
                 site_dir=site,
@@ -985,6 +984,8 @@ def _render(args: argparse.Namespace) -> int:
     print(f"{report.output_dir}: {report.pages} pages, {report.nodes} nodes, {report.linked} code links")
     for issue in report.unresolved:
         print(f"warning: declaration not found in the Lean sources: {issue}")
+    for issue in report.warnings:
+        print(f"warning: {issue}")
     if report.unresolved and args.require_declarations:
         return 1
     return 0

autoform_cli/coverage.py

@@ -10,19 +10,23 @@
 
 import hashlib
 import json
+import os
 import re
 from collections import Counter
+from collections.abc import Mapping
 from dataclasses import asdict, dataclass
-from pathlib import Path
+from pathlib import Path, PurePosixPath
 from urllib.parse import unquote, urlsplit
 
 from .markdown import (
+    EXTERNAL_SCHEMES,
     INLINE_CODE,
     Content,
     PublishedTable,
     content,
     link_targets,
     local_target_issue,
+    markdown_text_anchors,
     published_tables,
     rendered_visible_text,
 )
@@ -144,6 +148,57 @@ def load_coverage(blueprint_dir: str | Path) -> tuple[CoverageSummary | None, tu
     )
 
 
+def load_coverage_snapshot(
+    blueprint_dir: str | Path,
+    files: Mapping[str, bytes],
+) -> tuple[CoverageSummary | None, tuple[CoverageIssue, ...]]:
+    """Validate coverage from one immutable captured blueprint generation."""
+
+    blueprint = Path(blueprint_dir).expanduser()
+    if not blueprint.is_absolute():
+        blueprint = Path.cwd() / blueprint
+    normalized: dict[Path, bytes] = {}
+    for raw_relative, data in files.items():
+        relative = PurePosixPath(raw_relative)
+        if (
+            not raw_relative
+            or relative.is_absolute()
+            or relative.as_posix() != raw_relative
+            or ".." in relative.parts
+        ):
+            return None, (CoverageIssue(0, "coverage snapshot has an invalid path"),)
+        normalized[_lexical_path(blueprint.joinpath(*relative.parts))] = data
+    path = _lexical_path(blueprint / "coverage" / "README.md")
+    content_bytes = normalized.get(path)
+    if content_bytes is None:
+        return None, (CoverageIssue(0, "coverage contract is missing"),)
+    try:
+        text = content_bytes.decode("utf-8")
+    except UnicodeError:
+        return None, (CoverageIssue(0, "coverage contract cannot be read as UTF-8"),)
+
+    rows, issues = _parse_table(text)
+    issues.extend(
+        _validate_evidence(
+            rows,
+            blueprint=blueprint,
+            coverage_path=path,
+            captured_files=normalized,
+        )
+    )
+    if issues:
+        return None, tuple(issues)
+    return (
+        CoverageSummary(
+            schema=COVERAGE_SCHEMA,
+            source_path="coverage/README.md",
+            source_sha256=hashlib.sha256(content_bytes).hexdigest(),
+            entries=tuple(rows),
+        ),
+        (),
+    )
+
+
 def _parse_table(text: str) -> tuple[list[CoverageEntry], list[CoverageIssue]]:
     # Only published Markdown can carry the contract. Commented-out and
     # code-block tables are masked to blank lines first, which keeps every
@@ -467,9 +522,14 @@ def _validate_evidence(
     *,
     blueprint: Path,
     coverage_path: Path,
+    captured_files: Mapping[Path, bytes] | None = None,
 ) -> list[CoverageIssue]:
     issues: list[CoverageIssue] = []
-    roadmap = (blueprint / "roadmap").resolve()
+    roadmap = (
+        (blueprint / "roadmap").resolve()
+        if captured_files is None
+        else _lexical_path(blueprint / "roadmap")
+    )
     for entry in entries:
         visible_evidence = _visible_markdown(entry.evidence)
         if not _has_substance(visible_evidence):
@@ -495,13 +555,31 @@ def _validate_evidence(
         # One good link beside a broken one is a broken claim.
         broken: list[str] = []
         for target in targets:
-            problem = local_target_issue(coverage_path, target, blueprint, label="coverage")
+            problem = (
+                local_target_issue(coverage_path, target, blueprint, label="coverage")
+                if captured_files is None
+                else _captured_local_target_issue(
+                    coverage_path,
+                    target,
+                    blueprint,
+                    captured_files,
+                    label="coverage",
+                )
+            )
             if problem is not None:
                 broken.append(problem[1])
         if broken:
             issues.extend(CoverageIssue(entry.line, reason) for reason in broken)
             continue
-        if not any(_is_roadmap_article(target, coverage_path=coverage_path, roadmap=roadmap) for target in targets):
+        if not any(
+            _is_roadmap_article(
+                target,
+                coverage_path=coverage_path,
+                roadmap=roadmap,
+                captured_files=captured_files,
+            )
+            for target in targets
+        ):
             issues.append(
                 CoverageIssue(
                     entry.line,
@@ -561,21 +639,83 @@ def _is_placeholder(visible: str) -> bool:
     return _MARKER_PUNCTUATION.match(remainder) is not None
 
 
-def _is_roadmap_article(target: str, *, coverage_path: Path, roadmap: Path) -> bool:
+def _is_roadmap_article(
+    target: str,
+    *,
+    coverage_path: Path,
+    roadmap: Path,
+    captured_files: Mapping[Path, bytes] | None = None,
+) -> bool:
     parsed = urlsplit(target)
     if parsed.scheme or parsed.netloc:
         return False
     try:
         raw_path = unquote(parsed.path)
         if not raw_path or "\x00" in raw_path:
             return False
-        candidate = (coverage_path.parent / raw_path).resolve()
+        candidate = (
+            (coverage_path.parent / raw_path).resolve()
+            if captured_files is None
+            else _lexical_path(coverage_path.parent / raw_path)
+        )
         candidate.relative_to(roadmap)
-        return candidate.is_file() and candidate.suffix.casefold() == ".md"
+        return (
+            candidate.is_file() if captured_files is None else candidate in captured_files
+        ) and candidate.suffix.casefold() == ".md"
     except (OSError, RuntimeError, ValueError):
         return False
 
 
+def _captured_local_target_issue(
+    source_path: Path,
+    target: str,
+    boundary: Path,
+    files: Mapping[Path, bytes],
+    *,
+    label: str,
+) -> tuple[str, str] | None:
+    split = urlsplit(target)
+    scheme = split.scheme.casefold()
+    if scheme in EXTERNAL_SCHEMES:
+        return None
+    if scheme:
+        return f"unsupported-{label}-link", f"{label} link uses unsupported scheme: {target!r}"
+    if split.netloc:
+        return f"unsupported-{label}-link", f"{label} link uses a network location: {target!r}"
+    raw_path = unquote(split.path)
+    if "\x00" in raw_path:
+        return f"malformed-{label}-link", f"{label} link contains an invalid path: {target!r}"
+    if not raw_path:
+        candidate = _lexical_path(source_path)
+    else:
+        relative = Path(raw_path)
+        if relative.is_absolute():
+            return f"{label}-escapes-blueprint", f"{label} link escapes the blueprint: {target!r}"
+        candidate = _lexical_path(source_path.parent / relative)
+    boundary = _lexical_path(boundary)
+    try:
+        candidate.relative_to(boundary)
+    except ValueError:
+        return f"{label}-escapes-blueprint", f"{label} link escapes the blueprint: {target!r}"
+    data = files.get(candidate)
+    if data is None:
+        return f"{label}-not-found", f"{label} link does not resolve to a file: {target!r}"
+    if split.fragment and candidate.suffix.casefold() == ".md":
+        try:
+            text = data.decode("utf-8")
+        except UnicodeError:
+            anchors: set[str] = set()
+        else:
+            anchors = markdown_text_anchors(text)
+        if unquote(split.fragment) not in anchors:
+            return f"{label}-anchor-not-found", f"{label} link fragment does not resolve: {target!r}"
+    return None
+
+
+def _lexical_path(path: Path) -> Path:
+    return Path(os.path.normpath(os.fspath(path)))
+
+
 def _cells(line: str) -> tuple[str, ...]:
     stripped = line.strip()
     if not stripped.startswith("|") or not stripped.endswith("|"):
@@ -613,4 +753,5 @@ def _inline_code(value: str) -> str:
     "CoverageIssue",
     "CoverageSummary",
     "load_coverage",
+    "load_coverage_snapshot",
 ]