Create Lean projects atomically

.github/workflows/tests.yml

@@ -31,7 +31,7 @@ jobs:
   real-lean:
     name: real Lean (fixture toolchain)
     runs-on: ubuntu-latest
-    timeout-minutes: 45
+    timeout-minutes: 75
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
       - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
@@ -58,6 +58,16 @@ jobs:
           timeout --signal=TERM --kill-after=30s 10m \
             elan toolchain install "$(tr -d '\r\n' < tests/fixtures/skeleton-project/lean-toolchain)"
           command -v lake
+      - name: Build a project from the bundled creation release
+        run: |
+          set -euo pipefail
+          generated_project="$RUNNER_TEMP/autoform-created-project"
+          uv run autoform project new "$generated_project" \
+            --package GeneratedProject \
+            --release lean-v4.32.2-mathlib-v4.32.2
+          cd "$generated_project"
+          timeout --signal=TERM --kill-after=30s 20m lake exe cache get
+          timeout --signal=TERM --kill-after=30s 10m lake build
       - name: Run the skeleton suite against real Lean
         run: >-
           timeout --signal=TERM --kill-after=30s 25m uv run pytest -q

README.md

@@ -97,6 +97,8 @@ plugin development and debugging, not as a required user workflow.
 
 | Command | Purpose |
 | --- | --- |
+| `autoform project new` | Atomically create a compatible Lean and Autoform project. |
+| `autoform project inspect` | Inspect local project configuration without executing it. |
 | `autoform init` | Scaffold the blueprint and site; add CI when immutably pinned. |
 | `autoform check` | Validate Markdown structure and dependencies. |
 | `autoform audit` | Audit completeness and checked facts. |

autoform_cli/README.md

@@ -140,15 +140,41 @@ Local template capture uses retained no-follow directory descriptors, so
 `init` currently fails closed on platforms without the required POSIX APIs,
 including Windows.
 
-Inspect a Lean project and list Autoform's bundled known-good release pairs:
+Create or inspect a Lean project and list Autoform's bundled known-good release pairs:
 
 ```bash
+autoform project versions
+autoform project new ./FiniteFlat \
+  --package FiniteFlat \
+  --release lean-v4.32.2-mathlib-v4.32.2 \
+  --autoform-source https://github.com/facebookresearch/autoform-bot.git \
+  --autoform-ref <full-commit-sha>
 autoform project inspect .
 autoform project inspect path/inside/project --json
 autoform project versions --json
 autoform project provenance --json
 ```
 
+`project new` requires an absent target and an explicit release ID. It builds a
+complete Lean shell with the release's Lake-generated resolved dependency
+manifest, blueprint, and site in a private sibling directory, validates the
+staged project, then publishes the directory with an atomic no-replace rename.
+It never overwrites an existing path. Failed and concurrent creations leave no
+partial target, and exactly one concurrent creator can win.
+A private creation bundle adds generated production-module roots, so package
+names cannot shadow Mathlib libraries such as `Archive` or `Counterexamples`.
+Its release identity is cross-checked with the public catalog and its complete
+Lake manifest before any filesystem state is created.
+The command does not run Git, Lake, Lean, subprocesses, or network operations.
+Pass both provenance flags to include pinned CI workflows; without them the
+local project is complete but the workflows are omitted.
+It fails closed where POSIX descriptor traversal, advisory locking, directory
+sync, or atomic no-replace rename is unavailable, including on Windows.
+Immediately before publication and after syncing it, Autoform reopens the
+requested parent without following links and rechecks its device, inode, and
+owner. A pre-publication mismatch preserves the stage; a later mismatch reports
+where publication was observed and tells the caller not to retry blindly.
+
 `project inspect` reads the nearest enclosing project's decision files without
 running Lake, Lean, Git, or the network. `supported` means the inspected Lean
 toolchain, immutable Mathlib Git lock, and release loading layout identify a

autoform_cli/__main__.py

@@ -19,7 +19,13 @@
 from .doctor import diagnose_project
 from .graph import GraphValidationError, load_graph
 from .lean import build_linker, declaration_names
-from .project import ProjectCatalogError, inspect_project, load_release_catalog
+from .project import (
+    ProjectCatalogError,
+    ProjectCreateError,
+    create_project,
+    inspect_project,
+    load_release_catalog,
+)
 from .provenance import ProvenanceError, verify_plugin_provenance
 from .render import PublicationError, render_site
 from .scaffold import ScaffoldError, scaffold_project
@@ -73,8 +79,29 @@ def main(argv: Sequence[str] | None = None) -> int:
     doctor.add_argument("--lean-root", type=Path, help="Lean project to resolve local targets against")
     doctor.add_argument("--json", action="store_true", help="write stable machine-readable output")
 
-    project = subparsers.add_parser("project", help="inspect local project configuration and releases")
+    project = subparsers.add_parser(
+        "project", help="create or inspect local projects and supported releases"
+    )
     project_subparsers = project.add_subparsers(dest="project_command", required=True)
+    project_new = project_subparsers.add_parser(
+        "new", help="atomically create a complete Lean and Autoform project"
+    )
+    project_new.add_argument(
+        "target", nargs="?", help="new project directory; it must not exist"
+    )
+    project_new.add_argument("--package", help="UpperCamelCase Lean package name")
+    project_new.add_argument("--release", help="release id from 'project versions'")
+    project_new.add_argument(
+        "--autoform-source",
+        default="",
+        help="trusted Autoform Git source for generated workflows",
+    )
+    project_new.add_argument(
+        "--autoform-ref",
+        default="",
+        help="full 40-character Autoform commit for generated workflows",
+    )
+    project_new.add_argument("--json", action="store_true", help="write stable machine-readable output")
     project_inspect = project_subparsers.add_parser(
         "inspect", help="inspect a project without running Lake, Git, or network operations"
     )
@@ -323,6 +350,27 @@ def _doctor(args: argparse.Namespace) -> int:
 
 def _project(args: argparse.Namespace) -> int:
     try:
+        if args.project_command == "new":
+            result = create_project(
+                args.target,
+                package=args.package,
+                release_id=args.release,
+                autoform_source=args.autoform_source,
+                autoform_ref=args.autoform_ref,
+            )
+            if args.json:
+                print(result.to_json())
+            else:
+                print(
+                    _human_text(
+                        f"Created {result.package} at {result.target} ({result.release})"
+                    )
+                )
+                if not result.workflows_pinned:
+                    print(
+                        "warning: workflows were omitted because no immutable Autoform pin was available"
+                    )
+            return 0
         if args.project_command == "provenance":
             result = verify_plugin_provenance()
             if args.json:
@@ -332,6 +380,12 @@ def _project(args: argparse.Namespace) -> int:
                 print(f"Revision: {result.revision}")
             return 0
         catalog = load_release_catalog()
+    except ProjectCreateError as error:
+        if args.json:
+            print(error.to_json())
+        else:
+            print(f"error[{error.code}]: {error.message}", file=sys.stderr)
+        return 1
     except ProjectCatalogError as error:
         if args.json:
             print(json.dumps({"error": {"code": "project-catalog-invalid", "message": str(error)}, "ok": False}))
@@ -395,12 +449,9 @@ def _print_project_inspection(result) -> None:
 
 
 def _human_text(value: object) -> str:
-    """Escape nonprintable characters so project files cannot forge report lines."""
+    """Escape untrusted text into one printable ASCII report line."""
 
-    return "".join(
-        character if character.isprintable() else character.encode("unicode_escape").decode("ascii")
-        for character in str(value)
-    )
+    return ascii(str(value))[1:-1]
 
 
 def _claim(args: argparse.Namespace) -> int:

autoform_cli/project/__init__.py

@@ -1,4 +1,4 @@
-"""Offline Lean project inspection and supported release data."""
+"""Lean project creation, inspection, and supported release data."""
 
 from .catalog import (
     RELEASE_CATALOG_SCHEMA,
@@ -7,14 +7,18 @@
     load_release_catalog,
     parse_release_catalog,
 )
+from .create import ProjectCreateError, ProjectCreateResult, create_project
 from .inspect import PROJECT_INSPECTION_SCHEMA, ProjectInspection, inspect_project
 
 __all__ = [
     "PROJECT_INSPECTION_SCHEMA",
     "RELEASE_CATALOG_SCHEMA",
     "ProjectCatalogError",
+    "ProjectCreateError",
+    "ProjectCreateResult",
     "ProjectInspection",
     "ReleaseCatalog",
+    "create_project",
     "inspect_project",
     "load_release_catalog",
     "parse_release_catalog",