[Autoform] Harden collaborative textbook workflows

[Deicyde]

Summary

This PR adds the project, workspace, coverage, collaboration, Lean-runtime, and publication tooling needed to formalize textbook-scale sources and publish a readable companion.

New commands

Ready work

• autoform ready <project-or-blueprint> [--project <id>] [--lean-root <path>] [--json] lists ready statement/proof phases and structured blockers.

Project lifecycle

• autoform project new atomically creates a Lean + Autoform project.
• autoform project repair conservatively adds unambiguous missing files and supports dry runs.
• autoform project inspect reports local project configuration without running Lake, Git, or network operations.
• autoform project versions lists bundled Lean/Mathlib release pairs.
• autoform project provenance verifies the installed plugin against an immutable source revision.

Multi-blueprint workspaces

• autoform workspace init creates the root .autoform.toml registry.
• autoform workspace inspect reports registered locations and projects.
• autoform workspace check validates every registered blueprint.
• autoform blueprint new creates and registers a blueprint vault.
• autoform blueprint register registers an existing vault.
• autoform blueprint list lists registered blueprints.

Other additions

• Coverage v2 provides hashed source-unit accounting and durable article_id bindings. Ready-work discovery requires complete v2 coverage.
• Git-ref claims add session fencing, exact-CAS receipts, compatibility guards, and shared-resource claims for concurrent contributors.
• The Orchestrate skill guides the host agent through preflight checks, ready, claim, Lean work, independent review, final validation, and integration.
• Graph, audit, runtime, and visualization traversal scale to large dependency DAGs.
• Rendering uses verified snapshots and atomic directory publication, links resolved Lean declarations, and excludes raw source artifacts from the companion site.
• The shared Lean LSP/REPL runtime adds project-aware imports, cached import contexts, bounded resources, and stronger lifecycle handling.
• Generated CI and Pages workflows are provenance-pinned. CI covers Python 3.10 and 3.13, installed wheels, daemon behavior, and pinned Lean 4.32.2.
• The README now documents Claude Code and Codex installation, setup, validation, publication, workspaces, and concurrent formalization.

Compatibility

• Existing single-vault blueprint/ projects and autoform init remain supported; workspaces are opt-in.
• Coverage v1 remains available to audit and render while projects migrate to coverage v2 for ready-work discovery.
• Plugin CLI commands run through the installed plugin project, as documented in the README.

Status

• Head: 1cf2ca825fec5e6d3303e24374e218bf3e8ab5c1
• Base: facebookresearch/main at 13be889dee8477cba7271d3b805c5a87460124a3
• GitHub reports CLEAN and MERGEABLE.
• All eight checks pass: deterministic, daemon, and installed-wheel jobs on Python 3.10 and 3.13; pinned Lean 4.32.2; and Meta CLA.

[Deicyde]

Initial synchronized head 4d1e0fc: all eight upstream checks passed (Meta CLA; deterministic on Python 3.10 and 3.13; daemon on 3.10 and 3.13; installed wheel on 3.10 and 3.13; pinned real Lean). The four new hardening tracks remain off this branch until their exact commits clear independent adversarial review.

[Deicyde]

Reviewed update pushed at 0dfae0517308bc9b6c6f0dabf2b999421ff9caeb.

This tranche adds textbook-scale graph/runtime traversal and transactional companion-site publication. An independent exact-head review returned MERGE. Local validation passed 1,034 deterministic tests, 6 daemon tests, 1 installed-wheel test, 5 real-Lean tests, 84 render tests, Ruff, diff checks, and the strict bundled example build.

The local head, VivienCabannes branch, and this PR head match. The new GitHub checks are queued. Claims, verification, durable execution, source coverage v2, README, and live end-to-end changes remain excluded until separately reviewed.

[Deicyde]

CI follow-up pushed at 9b6ff9caf640c337113bb4111e6211fd6ca6712f.

The preceding run exposed a Python 3.10-only compatibility bug: that interpreter replaces a class-defined pickle restoration hook on frozen slotted dataclasses, so saved parent-format Graph objects restored their node map as an untracked dictionary. The repair installs the hook after dataclass decoration and adds an explicit restoration assertion.

Independent review returned MERGE. Local validation passes the saved parent fixture and pickle protocols 0 through 5 on Python 3.10 and 3.13, plus the complete deterministic suites on both versions. Local HEAD, VivienCabannes, and this PR head match. All eight GitHub checks now pass.

[Deicyde]

Pushed reviewed claim-safety hardening at da6869476d651258915e00ac1079a29dd97d1e4c.

This adds session-fenced leases, mixed-v1/v2 migration guards, exact CAS receipts, scrubbed Git transport configuration, and descriptor-pinned local repository access. Independent review returned MERGE.

Local combined-head gates:

• Python 3.10 deterministic: 1,117 passed
• Python 3.13 deterministic repeat: 1,116 passed, 1 expected platform skip
• daemon: 6 passed
• installed wheel: 1 passed
• real Lean: 5 passed
• strict example render/build and Ruff: passed

One first-pass Python 3.13 run returned a fail-closed holds() result after acquisition. It did not reproduce in the complete repeat, the natural test prefix, 20 isolated processes, or 180 independent stress checks including concurrency and low-FD conditions. No retry was added to hide the signal. If it recurs, the remote OID, receipt OID, lease clock values, and pinned descriptor identities will be captured.

The Vivien branch and upstream PR head both resolve to the exact SHA above. GitHub checks are in progress.