diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index b2968649..656aa4c7 100644 --- a/.github/workflows/tests.yml +++ b/.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 diff --git a/README.md b/README.md index e520aafe..12770a19 100644 --- a/README.md +++ b/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. | diff --git a/autoform_cli/README.md b/autoform_cli/README.md index 7923442d..50f2726b 100644 --- a/autoform_cli/README.md +++ b/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 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 diff --git a/autoform_cli/__main__.py b/autoform_cli/__main__.py index aa065d6a..6c801d2f 100644 --- a/autoform_cli/__main__.py +++ b/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: diff --git a/autoform_cli/project/__init__.py b/autoform_cli/project/__init__.py index b65259cd..fe228069 100644 --- a/autoform_cli/project/__init__.py +++ b/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", diff --git a/autoform_cli/project/create.py b/autoform_cli/project/create.py new file mode 100644 index 00000000..592217df --- /dev/null +++ b/autoform_cli/project/create.py @@ -0,0 +1,1242 @@ +"""Create a complete Autoform Lean project and publish it atomically.""" + +from __future__ import annotations + +import ctypes +import errno +import json +import os +import re +import secrets +import stat +from dataclasses import dataclass +from importlib.resources import files +from pathlib import Path, PurePosixPath +from urllib.parse import urlsplit + +from ..graph import _parse_node +from ..provenance import normalize_git_source +from ..scaffold import ( + DEFAULT_AUTOFORM_SOURCE, + ScaffoldError, + _TEMPLATES, + _ScaffoldFile, + _filesystem_template_snapshot, + _scaffold_plan, +) +from .catalog import SupportedRelease, load_release_catalog + +_PACKAGE_NAME = re.compile(r"[A-Z][A-Za-z0-9]*") +_FULL_SHA = re.compile(r"[0-9a-f]{40}") +_RESERVED_PACKAGE_NAMES = frozenset({"Prop", "Sort", "Type"}) +_CREATION_RELEASE_SCHEMA = "autoform-project-creation-release/v1" +_RELEASE_ID = re.compile(r"[A-Za-z0-9][A-Za-z0-9._-]*") +_STAGE_ATTEMPTS = 32 +_TOOLCHAIN_MODULE_ROOTS = frozenset({"Init", "Lake", "Lean", "Std"}) +_MATHLIB_PRODUCTION_ROOTS = frozenset({"Archive", "Counterexamples", "Mathlib"}) +_MANIFEST_FIELDS = frozenset( + {"version", "packagesDir", "packages", "name", "lakeDir", "fixedToolchain"} +) +_MANIFEST_PACKAGE_FIELDS = frozenset( + { + "url", + "type", + "subDir", + "scope", + "rev", + "name", + "manifestFile", + "inputRev", + "inherited", + "configFile", + } +) + + +class ProjectCreateError(ValueError): + """A new project could not be created without risking existing data.""" + + def __init__(self, code: str, message: str) -> None: + self.code = code + self.message = message + super().__init__(message) + + def as_dict(self) -> dict[str, object]: + return {"error": {"code": self.code, "message": self.message}, "ok": False} + + def to_json(self) -> str: + return json.dumps( + self.as_dict(), ensure_ascii=True, sort_keys=True, separators=(",", ":") + ) + + +@dataclass(frozen=True, slots=True) +class ProjectCreateResult: + package: str + release: str + target: str + written: tuple[str, ...] + workflows_pinned: bool + + def as_dict(self) -> dict[str, object]: + return { + "ok": True, + "package": self.package, + "release": self.release, + "target": self.target, + "workflows_pinned": self.workflows_pinned, + "written": list(self.written), + } + + def to_json(self) -> str: + return json.dumps( + self.as_dict(), ensure_ascii=True, sort_keys=True, separators=(",", ":") + ) + + +@dataclass(frozen=True, slots=True) +class _ReleaseBundle: + """Immutable release bytes and generated production-module metadata.""" + + manifest_bytes: bytes + module_roots: frozenset[str] + + +@dataclass(frozen=True, slots=True) +class _CreationReleaseDescriptor: + manifest_resource: str + module_roots: tuple[str, ...] + + +def create_project( + target: str | Path | None, + *, + package: str | None, + release_id: str | None, + autoform_source: str = "", + autoform_ref: str = "", +) -> ProjectCreateResult: + """Create and atomically publish a new project at an absent *target*.""" + + requested = _validate_target(target) + package_name = _validate_package(package, requested.parent) + release = _find_release(release_id) + release_bundle = _load_release_bundle(release) + _validate_package_for_release(package_name, release_bundle) + workflow_source, workflow_ref = _validate_workflow_pin(autoform_source, autoform_ref) + try: + plan, workflows_pinned = _build_project_plan( + package_name, + release, + release_bundle, + autoform_source=workflow_source, + autoform_ref=workflow_ref, + ) + _plan_tree(plan) + _validate_roadmap_plan(plan) + except (OSError, ScaffoldError, UnicodeError): + raise ProjectCreateError( + "project-create-validation-failed", + "The generated project did not satisfy Autoform's project contracts.", + ) from None + parent = requested.parent + parent_descriptor = _open_parent(parent) + parent_identity = _descriptor_identity(parent_descriptor) + publish_parent_descriptor: int | None = None + confirmed_parent_descriptor: int | None = None + stage_name: str | None = None + stage_descriptor: int | None = None + publication_started = False + published = False + parent_synced = False + parent_rebound = False + parent_recheck_failed = False + try: + _require_package_filename_fit(package_name, parent_descriptor) + _lock_parent(parent_descriptor) + _require_absent(parent_descriptor, requested.name) + stage_name = _create_stage(parent_descriptor) + stage_metadata = os.stat(stage_name, dir_fd=parent_descriptor, follow_symlinks=False) + if not stat.S_ISDIR(stage_metadata.st_mode): + raise OSError(errno.ENOTDIR, "staging path is not a directory") + stage_descriptor = _open_stage(parent_descriptor, stage_name) + _require_stage_identity(parent_descriptor, stage_name, stage_descriptor) + _materialize_project(stage_descriptor, plan) + _require_stage_identity(parent_descriptor, stage_name, stage_descriptor) + _validate_staged_project( + stage_descriptor, + plan, + package_name, + release, + release_bundle, + ) + _require_stage_identity(parent_descriptor, stage_name, stage_descriptor) + os.fchmod(stage_descriptor, 0o755) + os.fsync(stage_descriptor) + _verify_project_plan(stage_descriptor, plan, root_mode=0o755) + _require_stage_identity(parent_descriptor, stage_name, stage_descriptor) + # Re-resolve the canonical requested parent with O_NOFOLLOW at the last + # possible moment. Publication uses this fresh descriptor only after + # its device, inode, and owner match the directory we locked and staged + # in. A mismatch leaves the complete stage untouched. + publish_parent_descriptor = _reopen_bound_parent(parent, parent_identity) + _require_stage_identity(publish_parent_descriptor, stage_name, stage_descriptor) + publication_started = True + try: + _rename_noreplace( + parent_descriptor, + stage_name, + publish_parent_descriptor, + requested.name, + ) + except FileExistsError: + raise ProjectCreateError( + "project-target-exists", + "The target already exists; project new never overwrites it.", + ) from None + published = True + _require_stage_identity(publish_parent_descriptor, requested.name, stage_descriptor) + os.fsync(publish_parent_descriptor) + parent_synced = True + try: + confirmed_parent_descriptor = _reopen_bound_parent(parent, parent_identity) + except ProjectCreateError as error: + if error.code == "project-parent-changed": + parent_rebound = True + else: + parent_recheck_failed = True + raise + _require_stage_identity(confirmed_parent_descriptor, requested.name, stage_descriptor) + return ProjectCreateResult( + package=package_name, + release=release.id, + target=requested.name, + written=tuple(item.relative for item in plan), + workflows_pinned=workflows_pinned, + ) + except ProjectCreateError as error: + state = _publication_state( + parent_descriptor, + requested.name, + stage_name, + stage_descriptor, + ) + if published or (publication_started and state != "stage"): + raise ProjectCreateError( + "project-create-commit-uncertain", + _commit_uncertain_message( + state, + parent_synced=parent_synced, + parent_rebound=parent_rebound, + parent_recheck_failed=parent_recheck_failed, + ), + ) from None + if stage_name is not None: + raise ProjectCreateError(error.code, _with_preserved_stage(error.message)) from None + raise + except OSError: + state = _publication_state( + parent_descriptor, + requested.name, + stage_name, + stage_descriptor, + ) + if published or (publication_started and state != "stage"): + raise ProjectCreateError( + "project-create-commit-uncertain", + _commit_uncertain_message( + state, + parent_synced=parent_synced, + parent_rebound=parent_rebound, + parent_recheck_failed=parent_recheck_failed, + ), + ) from None + message = "Project creation failed; no project was created." + if stage_name is not None: + message = _with_preserved_stage(message) + raise ProjectCreateError("project-create-failed", message) from None + except BaseException: + state = _publication_state( + parent_descriptor, + requested.name, + stage_name, + stage_descriptor, + ) + if published or (publication_started and state != "stage"): + raise ProjectCreateError( + "project-create-commit-uncertain", + _commit_uncertain_message( + state, + parent_synced=parent_synced, + parent_rebound=parent_rebound, + parent_recheck_failed=parent_recheck_failed, + ), + ) from None + raise + finally: + state = _publication_state( + parent_descriptor, + requested.name, + stage_name, + stage_descriptor, + ) + publication_uncertain = not published and publication_started and state != "stage" + close_failed = False + for descriptor in ( + confirmed_parent_descriptor, + publish_parent_descriptor, + stage_descriptor, + parent_descriptor, + ): + if descriptor is None: + continue + try: + os.close(descriptor) + except OSError: + close_failed = True + if publication_uncertain: + raise ProjectCreateError( + "project-create-commit-uncertain", + _commit_uncertain_message( + state, + parent_synced=parent_synced, + parent_rebound=parent_rebound, + parent_recheck_failed=parent_recheck_failed, + ), + ) + if close_failed and published: + raise ProjectCreateError( + "project-create-commit-uncertain", + _commit_uncertain_message( + state, + parent_synced=parent_synced, + parent_rebound=parent_rebound, + parent_recheck_failed=parent_recheck_failed, + cleanup_failed=True, + ), + ) + + +def _with_preserved_stage(message: str) -> str: + return f"{message} An .autoform-new-* stage may remain; inspect it before removal." + + +def _commit_uncertain_message( + state: str, + *, + parent_synced: bool, + parent_rebound: bool, + parent_recheck_failed: bool, + cleanup_failed: bool = False, +) -> str: + if parent_rebound: + return ( + "The project was published and its original parent directory was synced, but the " + "requested parent path no longer names that directory. The requested target may not " + "name the project; locate it before retrying." + ) + if parent_recheck_failed: + return ( + "The project was published and its original parent directory was synced, but Autoform " + "could not reopen the requested parent path to confirm that it still names that " + "directory. The target was observed through the original parent descriptor; verify " + "the requested path before retrying." + ) + if state == "target": + durability = ( + "its parent directory was synced" + if parent_synced + else "the parent-directory sync was not confirmed" + ) + suffix = " and final descriptor cleanup failed" if cleanup_failed else "" + return ( + f"The target names the published project and {durability}{suffix}. " + "Do not retry project creation." + ) + return ( + "Publication started, but neither the target nor the preserved stage names the project " + "directory held open by Autoform. It may have been moved; locate it before retrying." + ) + + +def _validate_package(package: str | None, parent: Path) -> str: + if ( + not isinstance(package, str) + or _PACKAGE_NAME.fullmatch(package) is None + or package in _RESERVED_PACKAGE_NAMES + ): + raise ProjectCreateError( + "project-name-invalid", + "Project name must be an UpperCamelCase Lean identifier.", + ) + try: + name_limit = os.pathconf(parent, "PC_NAME_MAX") + except (AttributeError, OSError, ValueError): + raise ProjectCreateError( + "project-create-safety-unavailable", + "This platform cannot validate the generated Lean filename safely.", + ) from None + if len(f"{package}.lean".encode("ascii")) > name_limit: + raise ProjectCreateError( + "project-name-invalid", + "Project name is too long for a Lean module on the target filesystem.", + ) + return package + + +def _require_package_filename_fit(package: str, parent_descriptor: int) -> None: + try: + name_limit = os.fpathconf(parent_descriptor, "PC_NAME_MAX") + except (AttributeError, OSError, ValueError): + raise ProjectCreateError( + "project-create-safety-unavailable", + "This platform cannot validate the generated Lean filename safely.", + ) from None + if len(f"{package}.lean".encode("ascii")) > name_limit: + raise ProjectCreateError( + "project-name-invalid", + "Project name is too long for a Lean module on the target filesystem.", + ) + + +def _find_release(release_id: str | None) -> SupportedRelease: + catalog = load_release_catalog() + release = next((item for item in catalog.releases if item.id == release_id), None) + if release is None: + raise ProjectCreateError( + "project-release-unknown", + "The requested release is not in the bundled release catalog.", + ) + return release + + +def _validate_package_for_release(package: str, bundle: _ReleaseBundle) -> None: + if package.casefold() in {root.casefold() for root in bundle.module_roots}: + raise ProjectCreateError( + "project-name-invalid", + "Project name must not shadow a Lean module root used by the selected release.", + ) + + +def _validate_workflow_pin(source: str, ref: str) -> tuple[str, str]: + """Validate explicit provenance before creating filesystem state.""" + + if not isinstance(source, str) or not isinstance(ref, str): + raise ProjectCreateError( + "project-provenance-invalid", + "Autoform workflow provenance must include a safe Git source and full commit SHA.", + ) + if not source and not ref: + return "", "" + safe_source = normalize_git_source(source) + normalized_ref = ref.strip().lower() + if not source or not ref or safe_source is None or _FULL_SHA.fullmatch(normalized_ref) is None: + raise ProjectCreateError( + "project-provenance-invalid", + "Autoform workflow provenance must include a safe Git source and full commit SHA.", + ) + return safe_source, normalized_ref + + +def _validate_target(target: str | Path | None) -> Path: + try: + if target is None: + raise ValueError + encoded = os.fspath(target) + if not isinstance(encoded, str) or "\0" in encoded: + raise ValueError + # Reject strings that the host filesystem codec cannot round-trip and + # all surrogate spellings. Some POSIX kernels accept surrogate-escaped + # bytes for lookup but reject them in atomic rename syscalls; rejecting + # them here avoids leaving a complete stage after that late failure. + if ( + any(0xD800 <= ord(character) <= 0xDFFF for character in encoded) + or os.fsdecode(os.fsencode(encoded)) != encoded + ): + raise ValueError + selected = Path(encoded).expanduser() + if not selected.parts or selected.name in {"", ".", ".."}: + raise ValueError + raw = selected.absolute() + except (OSError, RuntimeError, TypeError, ValueError): + raise ProjectCreateError("project-target-invalid", "The project target cannot be resolved safely.") from None + if raw.name in {"", ".", ".."}: + raise ProjectCreateError("project-target-invalid", "The project target must name a new directory.") + parent = raw.parent + if not parent.exists(): + raise ProjectCreateError("project-parent-missing", "The target parent directory does not exist.") + if not parent.is_dir(): + raise ProjectCreateError("project-parent-invalid", "The target parent is not a directory.") + try: + metadata = parent.stat() + except OSError: + raise ProjectCreateError("project-parent-invalid", "The target parent is not a directory.") from None + if _unsafe_parent_metadata(metadata.st_mode, metadata.st_uid): + raise ProjectCreateError( + "project-parent-unsafe", + "The target parent has unsafe write permissions or ownership.", + ) + try: + canonical_parent = parent.resolve(strict=True) + except (OSError, RuntimeError, ValueError): + raise ProjectCreateError("project-parent-invalid", "The target parent is not a directory.") from None + return canonical_parent / raw.name + + +def _unsafe_parent_metadata(mode: int, owner: int) -> bool: + shared_writable = bool(mode & (stat.S_IWGRP | stat.S_IWOTH)) + if not shared_writable: + return False + if not mode & stat.S_ISVTX: + return True + # Sticky directories protect entries only from peers, not from their owner. + # Trust the invoking user and the system administrator, as conventional + # root-owned temporary directories require. + return not hasattr(os, "geteuid") or owner not in {0, os.geteuid()} + + +def _open_parent(parent: Path) -> int: + if ( + not hasattr(os, "O_NOFOLLOW") + or not hasattr(os, "O_DIRECTORY") + or not hasattr(os, "O_NONBLOCK") + or any(function not in os.supports_dir_fd for function in (os.mkdir, os.open, os.stat)) + or os.stat not in os.supports_follow_symlinks + or os.listdir not in os.supports_fd + or not hasattr(os, "geteuid") + ): + raise ProjectCreateError( + "project-create-safety-unavailable", + "This platform cannot create the project with the required path safety.", + ) + flags = os.O_RDONLY | os.O_DIRECTORY | os.O_NOFOLLOW | getattr(os, "O_CLOEXEC", 0) + absolute = parent.absolute() + try: + descriptor = os.open(absolute.anchor, flags) + try: + for part in absolute.parts[1:]: + child = os.open(part, flags, dir_fd=descriptor) + os.close(descriptor) + descriptor = child + metadata = os.fstat(descriptor) + if _unsafe_parent_metadata(metadata.st_mode, metadata.st_uid): + raise ProjectCreateError( + "project-parent-unsafe", + "The target parent has unsafe write permissions or ownership.", + ) + except BaseException: + os.close(descriptor) + raise + except (OSError, UnicodeError): + raise ProjectCreateError("project-path-is-symlink", "The target path contains a symbolic link.") from None + return descriptor + + +def _reopen_bound_parent(parent: Path, expected_identity: tuple[int, int, int]) -> int: + """Open *parent* afresh and require the same device, inode, and owner.""" + + try: + descriptor = _open_parent(parent) + except ProjectCreateError: + raise ProjectCreateError( + "project-parent-unverifiable", + "The requested parent path could not be reverified safely.", + ) from None + try: + if _descriptor_identity(descriptor) != expected_identity: + raise ProjectCreateError( + "project-parent-changed", + "The requested parent path changed while the project was being created.", + ) + except BaseException: + os.close(descriptor) + raise + return descriptor + + +def _require_absent(parent_descriptor: int, name: str) -> None: + try: + os.stat(name, dir_fd=parent_descriptor, follow_symlinks=False) + except FileNotFoundError: + return + except OSError: + raise ProjectCreateError("project-create-failed", "Project creation failed; no project was created.") from None + raise ProjectCreateError("project-target-exists", "The target already exists; project new never overwrites it.") + + +def _create_stage(parent_descriptor: int) -> str: + for _ in range(_STAGE_ATTEMPTS): + name = f".autoform-new-{secrets.token_hex(8)}" + try: + os.mkdir(name, mode=0o700, dir_fd=parent_descriptor) + return name + except FileExistsError: + continue + raise ProjectCreateError("project-create-failed", "Project creation failed; no project was created.") + + +def _open_stage(parent_descriptor: int, stage_name: str) -> int: + flags = os.O_RDONLY | os.O_DIRECTORY | os.O_NOFOLLOW | getattr(os, "O_CLOEXEC", 0) + return os.open(stage_name, flags, dir_fd=parent_descriptor) + + +def _open_planned_file(parent_descriptor: int, name: str) -> int: + flags = os.O_RDONLY | os.O_NOFOLLOW | os.O_NONBLOCK | getattr(os, "O_CLOEXEC", 0) + return os.open(name, flags, dir_fd=parent_descriptor) + + +def _lock_parent(parent_descriptor: int) -> None: + try: + import fcntl + + fcntl.flock(parent_descriptor, fcntl.LOCK_EX) + except (ImportError, OSError): + raise ProjectCreateError( + "project-create-safety-unavailable", + "This platform cannot serialize concurrent project creation safely.", + ) from None + + +def _list_directory(directory_descriptor: int) -> list[str]: + """List through a fresh descriptor so earlier scans cannot leave it at EOF.""" + + fresh = _open_stage(directory_descriptor, ".") + try: + return os.listdir(fresh) + finally: + os.close(fresh) + + +def _descriptor_identity(descriptor: int) -> tuple[int, int, int]: + metadata = os.fstat(descriptor) + if not stat.S_ISDIR(metadata.st_mode): + raise OSError(errno.ENOTDIR, "staging path is not a directory") + return metadata.st_dev, metadata.st_ino, metadata.st_uid + + +def _require_stage_identity(workspace_descriptor: int, stage_name: str, stage_descriptor: int) -> None: + expected = _descriptor_identity(stage_descriptor) + metadata = os.stat(stage_name, dir_fd=workspace_descriptor, follow_symlinks=False) + if ( + not stat.S_ISDIR(metadata.st_mode) + or metadata.st_uid != os.geteuid() + or (metadata.st_dev, metadata.st_ino, metadata.st_uid) != expected + ): + raise ProjectCreateError("project-create-failed", "Project creation failed; no project was created.") + + +def _entry_matches_descriptor(parent_descriptor: int, name: str, descriptor: int) -> bool: + try: + expected = _descriptor_identity(descriptor) + metadata = os.stat(name, dir_fd=parent_descriptor, follow_symlinks=False) + except (OSError, UnicodeError): + return False + return ( + stat.S_ISDIR(metadata.st_mode) + and metadata.st_uid == os.geteuid() + and (metadata.st_dev, metadata.st_ino, metadata.st_uid) == expected + ) + + +def _publication_state( + parent_descriptor: int, + target_name: str, + stage_name: str | None, + stage_descriptor: int | None, +) -> str: + if stage_name is None or stage_descriptor is None: + return "none" + target_matches = _entry_matches_descriptor(parent_descriptor, target_name, stage_descriptor) + stage_matches = _entry_matches_descriptor(parent_descriptor, stage_name, stage_descriptor) + if target_matches and not stage_matches: + return "target" + if stage_matches and not target_matches: + return "stage" + return "detached" + + +def _build_project_plan( + package: str, + release: SupportedRelease, + release_bundle: _ReleaseBundle, + *, + autoform_source: str, + autoform_ref: str, +) -> tuple[tuple[_ScaffoldFile, ...], bool]: + files = list(_core_project_plan(package, release, release_bundle)) + scaffold_files, _ = _scaffold_plan( + _filesystem_template_snapshot(_TEMPLATES), + title=package, + repository_url="", + autoform_source=autoform_source or DEFAULT_AUTOFORM_SOURCE, + autoform_ref=autoform_ref, + ) + files.extend(scaffold_files) + return tuple(sorted(files, key=lambda item: item.relative)), bool(autoform_ref) + + +def _core_project_plan( + package: str, + release: SupportedRelease, + release_bundle: _ReleaseBundle, +) -> tuple[_ScaffoldFile, ...]: + return ( + _ScaffoldFile("lean-toolchain", f"{release.lean_toolchain}\n".encode(), 0o644), + _ScaffoldFile( + "lakefile.toml", + ( + f'name = "{package}"\n' + 'version = "0.1.0"\n' + f'defaultTargets = ["{package}"]\n\n' + "[[require]]\n" + 'name = "mathlib"\n' + f'git = "{release.mathlib_git}"\n' + f'rev = "{release.mathlib_rev}"\n\n' + "[[lean_lib]]\n" + f'name = "{package}"\n' + 'srcDir = "src"\n' + ).encode(), + 0o644, + ), + _ScaffoldFile( + "lake-manifest.json", + _lake_manifest(package, release_bundle), + 0o644, + ), + _ScaffoldFile( + f"src/{package}.lean", + ( + "import Mathlib\n\n" + f"namespace {package}\n\n" + "/-- Marker declaration for the initial project build. -/\n" + "def autoformProjectInitialized : Bool := true\n\n" + f"end {package}\n" + ).encode(), + 0o644, + ), + ) + + +def _load_release_bundle(release: SupportedRelease) -> _ReleaseBundle: + try: + descriptor = _load_creation_release_descriptor(release) + manifest_bytes = ( + files("autoform_cli.project").joinpath(descriptor.manifest_resource).read_bytes() + ) + return _parse_release_bundle(manifest_bytes, release, descriptor.module_roots) + except ProjectCreateError: + raise + except (OSError, TypeError, UnicodeError, ValueError, RecursionError, MemoryError): + raise ProjectCreateError( + "project-create-validation-failed", + "The bundled release manifest is invalid.", + ) from None + + +def _load_creation_release_descriptor( + release: SupportedRelease, +) -> _CreationReleaseDescriptor: + if _RELEASE_ID.fullmatch(release.id) is None: + raise ProjectCreateError( + "project-create-validation-failed", + "The bundled project-creation release metadata is invalid.", + ) + resource = f"creation-release-{release.id}.json" + try: + payload = json.loads( + files("autoform_cli.project").joinpath(resource).read_bytes(), + object_pairs_hook=_reject_duplicate_object, + parse_constant=_reject_json_constant, + ) + except (OSError, TypeError, UnicodeError, ValueError, RecursionError, MemoryError): + raise ProjectCreateError( + "project-create-validation-failed", + "The bundled project-creation release metadata is invalid.", + ) from None + expected_release = { + "id": release.id, + "lean_toolchain": release.lean_toolchain, + "mathlib_git": release.mathlib_git, + "mathlib_rev": release.mathlib_rev, + "mathlib_commit": release.mathlib_commit, + } + roots = payload.get("production_module_roots") if type(payload) is dict else None + manifest_resource = payload.get("lake_manifest") if type(payload) is dict else None + if ( + type(payload) is not dict + or set(payload) + != {"schema", "release", "lake_manifest", "production_module_roots"} + or payload.get("schema") != _CREATION_RELEASE_SCHEMA + or payload.get("release") != expected_release + or type(manifest_resource) is not str + or not _safe_resource_name(manifest_resource) + or type(roots) is not list + or not roots + or any( + type(root) is not str or _PACKAGE_NAME.fullmatch(root) is None + for root in roots + ) + or len({root.casefold() for root in roots}) != len(roots) + ): + raise ProjectCreateError( + "project-create-validation-failed", + "The bundled project-creation release metadata is invalid.", + ) + return _CreationReleaseDescriptor(manifest_resource, tuple(roots)) + + +def _safe_resource_name(value: str) -> bool: + return ( + value.endswith(".json") + and value not in {".", ".."} + and "/" not in value + and "\\" not in value + and "\0" not in value + and all(0x20 <= ord(character) < 0xD800 for character in value) + ) + + +def _parse_release_bundle( + manifest_bytes: bytes, + release: SupportedRelease, + module_roots: tuple[str, ...], +) -> _ReleaseBundle: + try: + payload = json.loads( + manifest_bytes, + object_pairs_hook=_reject_duplicate_object, + parse_constant=_reject_json_constant, + ) + except (OSError, TypeError, UnicodeError, ValueError, RecursionError, MemoryError): + raise ProjectCreateError( + "project-create-validation-failed", + "The bundled release manifest is invalid.", + ) from None + roots = frozenset(module_roots) + packages = payload.get("packages") if type(payload) is dict else None + if ( + type(payload) is not dict + or set(payload) != _MANIFEST_FIELDS + or payload.get("version") != "1.2.0" + or payload.get("packagesDir") != ".lake/packages" + or payload.get("name") != "" + or payload.get("lakeDir") != ".lake" + or payload.get("fixedToolchain") is not False + or type(packages) is not list + or not packages + ): + raise ProjectCreateError( + "project-create-validation-failed", + "The bundled release manifest is invalid.", + ) + names: list[str] = [] + for entry in packages: + if not _valid_manifest_package(entry): + raise ProjectCreateError( + "project-create-validation-failed", + "The bundled release manifest is invalid.", + ) + names.append(entry["name"]) + direct = [entry for entry in packages if entry.get("inherited") is False] + folded_roots = {root.casefold() for root in roots} + if ( + len({name.casefold() for name in names}) != len(names) + or len(direct) != 1 + or direct[0].get("name") != "mathlib" + or direct[0].get("url") != release.mathlib_git + or direct[0].get("inputRev") != release.mathlib_rev + or direct[0].get("rev") != release.mathlib_commit + or direct[0].get("subDir") is not None # releases load Mathlib from its repository root + or direct[0].get("configFile") != "lakefile.lean" + or direct[0].get("manifestFile") != "lake-manifest.json" + or not _TOOLCHAIN_MODULE_ROOTS <= roots + or not _MATHLIB_PRODUCTION_ROOTS <= roots + or any(name.casefold() not in folded_roots for name in names) + ): + raise ProjectCreateError( + "project-create-validation-failed", + "The bundled release manifest does not match the release catalog.", + ) + return _ReleaseBundle(manifest_bytes=manifest_bytes, module_roots=roots) + + +def _valid_manifest_package(entry: object) -> bool: + if type(entry) is not dict or set(entry) != _MANIFEST_PACKAGE_FIELDS: + return False + url = entry["url"] + name = entry["name"] + scope = entry["scope"] + revision = entry["rev"] + input_revision = entry["inputRev"] + config_file = entry["configFile"] + manifest_file = entry["manifestFile"] + subdirectory = entry["subDir"] + return ( + type(url) is str + and _safe_https_git_url(url) + and entry["type"] == "git" + and type(name) is str + and re.fullmatch(r"[A-Za-z][A-Za-z0-9]*", name) is not None + and type(scope) is str + and type(revision) is str + and _FULL_SHA.fullmatch(revision) is not None + and type(input_revision) is str + and bool(input_revision) + and all(ord(character) >= 0x20 for character in input_revision) + and type(entry["inherited"]) is bool + and _safe_manifest_relative(config_file) + and _safe_manifest_relative(manifest_file) + and (subdirectory is None or _safe_manifest_relative(subdirectory)) + ) + + +def _safe_https_git_url(value: str) -> bool: + try: + parsed = urlsplit(value) + except ValueError: + return False + return ( + parsed.scheme == "https" + and bool(parsed.hostname) + and parsed.username is None + and parsed.password is None + and not parsed.query + and not parsed.fragment + and parsed.path not in {"", "/"} + ) + + +def _safe_manifest_relative(value: object) -> bool: + if ( + type(value) is not str + or value in {"", ".", ".."} + or "\\" in value + or "\0" in value + or any( + ord(character) < 0x20 or 0xD800 <= ord(character) <= 0xDFFF + for character in value + ) + ): + return False + path = PurePosixPath(value) + return ( + not path.is_absolute() + and path.as_posix() == value + and all(part not in {"", ".", ".."} for part in path.parts) + ) + + +def _reject_duplicate_object(pairs: list[tuple[str, object]]) -> dict[str, object]: + result: dict[str, object] = {} + for key, value in pairs: + if key in result: + raise ValueError("duplicate JSON key") + result[key] = value + return result + + +def _reject_json_constant(value: str) -> None: + raise ValueError(f"invalid JSON constant: {value}") + + +def _lake_manifest(package: str, bundle: _ReleaseBundle) -> bytes: + payload = json.loads(bundle.manifest_bytes) + payload["name"] = package + return (json.dumps(payload, sort_keys=True, separators=(",", ":")) + "\n").encode() + + +def _plan_tree(plan: tuple[_ScaffoldFile, ...]) -> dict[str, object]: + if type(plan) is not tuple: + raise ProjectCreateError( + "project-create-validation-failed", + "The generated project did not satisfy Autoform's project contracts.", + ) + tree: dict[str, object] = {} + for item in plan: + if ( + type(item) is not _ScaffoldFile + or type(item.relative) is not str + or type(item.content) is not bytes + or type(item.mode) is not int + or item.mode != item.mode & 0o777 + or item.mode & 0o022 + or not item.mode & 0o400 + ): + raise ProjectCreateError( + "project-create-validation-failed", + "The generated project did not satisfy Autoform's project contracts.", + ) + path = PurePosixPath(item.relative) + if ( + not item.relative + or "\\" in item.relative + or "\0" in item.relative + or any( + ord(character) < 0x20 or 0xD800 <= ord(character) <= 0xDFFF + for character in item.relative + ) + or path.is_absolute() + or path.as_posix() != item.relative + or any(part in {"", ".", ".."} for part in path.parts) + ): + raise ProjectCreateError( + "project-create-validation-failed", + "The generated project did not satisfy Autoform's project contracts.", + ) + branch = tree + for part in path.parts[:-1]: + child = branch.setdefault(part, {}) + if not isinstance(child, dict): + raise ProjectCreateError( + "project-create-validation-failed", + "The generated project did not satisfy Autoform's project contracts.", + ) + branch = child + if path.name in branch: + raise ProjectCreateError( + "project-create-validation-failed", + "The generated project did not satisfy Autoform's project contracts.", + ) + branch[path.name] = item + return tree + + +def _write_all(descriptor: int, content: bytes) -> None: + offset = 0 + while offset < len(content): + written = os.write(descriptor, content[offset:]) + if written <= 0: + raise OSError(errno.EIO, "short project file write") + offset += written + + +def _materialize_project(root_descriptor: int, plan: tuple[_ScaffoldFile, ...]) -> None: + tree = _plan_tree(plan) + + def write_directory(descriptor: int, entries: dict[str, object]) -> None: + for name, entry in sorted(entries.items()): + if isinstance(entry, dict): + os.mkdir(name, mode=0o700, dir_fd=descriptor) + metadata = os.stat(name, dir_fd=descriptor, follow_symlinks=False) + child = _open_stage(descriptor, name) + try: + if _descriptor_identity(child) != ( + metadata.st_dev, + metadata.st_ino, + metadata.st_uid, + ): + raise OSError(errno.ESTALE, "project directory changed") + write_directory(child, entry) + os.fchmod(child, 0o755) + os.fsync(child) + current = os.stat(name, dir_fd=descriptor, follow_symlinks=False) + if (current.st_dev, current.st_ino, current.st_uid) != ( + metadata.st_dev, + metadata.st_ino, + metadata.st_uid, + ): + raise OSError(errno.ESTALE, "project directory changed") + finally: + os.close(child) + continue + if not isinstance(entry, _ScaffoldFile): + raise OSError(errno.EINVAL, "invalid project plan") + flags = os.O_WRONLY | os.O_CREAT | os.O_EXCL | os.O_NOFOLLOW | getattr(os, "O_CLOEXEC", 0) + child = os.open(name, flags, 0o600, dir_fd=descriptor) + try: + _write_all(child, entry.content) + os.fchmod(child, entry.mode) + os.fsync(child) + finally: + os.close(child) + if set(_list_directory(descriptor)) != set(entries): + raise OSError(errno.ESTALE, "project directory changed") + + write_directory(root_descriptor, tree) + + +def _verify_project_plan( + root_descriptor: int, + plan: tuple[_ScaffoldFile, ...], + *, + root_mode: int = 0o700, +) -> None: + tree = _plan_tree(plan) + root = os.fstat(root_descriptor) + if ( + not stat.S_ISDIR(root.st_mode) + or root.st_uid != os.geteuid() + or stat.S_IMODE(root.st_mode) != root_mode + ): + raise OSError(errno.ESTALE, "project root changed") + + def stable_metadata(metadata: os.stat_result) -> tuple[int, ...]: + return ( + metadata.st_dev, + metadata.st_ino, + metadata.st_mode, + metadata.st_nlink, + metadata.st_uid, + metadata.st_gid, + metadata.st_size, + metadata.st_mtime_ns, + metadata.st_ctime_ns, + ) + + def verify_directory(descriptor: int, entries: dict[str, object]) -> None: + directory_before = os.fstat(descriptor) + if set(_list_directory(descriptor)) != set(entries): + raise OSError(errno.ESTALE, "project directory changed") + for name, entry in sorted(entries.items()): + metadata = os.stat(name, dir_fd=descriptor, follow_symlinks=False) + if isinstance(entry, dict): + if not stat.S_ISDIR(metadata.st_mode): + raise OSError(errno.ESTALE, "project directory changed") + child = _open_stage(descriptor, name) + try: + opened = os.fstat(child) + if ( + stable_metadata(opened) != stable_metadata(metadata) + or opened.st_uid != os.geteuid() + or stat.S_IMODE(opened.st_mode) != 0o755 + ): + raise OSError(errno.ESTALE, "project directory changed") + verify_directory(child, entry) + after = os.fstat(child) + current = os.stat(name, dir_fd=descriptor, follow_symlinks=False) + if not (stable_metadata(opened) == stable_metadata(after) == stable_metadata(current)): + raise OSError(errno.ESTALE, "project directory changed") + finally: + os.close(child) + continue + if not isinstance(entry, _ScaffoldFile) or not stat.S_ISREG(metadata.st_mode): + raise OSError(errno.ESTALE, "project file changed") + child = _open_planned_file(descriptor, name) + try: + opened = os.fstat(child) + content = bytearray() + while len(content) <= len(entry.content): + chunk = os.read( + child, + min(1024 * 1024, len(entry.content) + 1 - len(content)), + ) + if not chunk: + break + content.extend(chunk) + after = os.fstat(child) + current = os.stat(name, dir_fd=descriptor, follow_symlinks=False) + if ( + not stat.S_ISREG(opened.st_mode) + or stable_metadata(metadata) != stable_metadata(opened) + or stable_metadata(opened) != stable_metadata(after) + or stable_metadata(after) != stable_metadata(current) + or after.st_nlink != 1 + or after.st_uid != os.geteuid() + or stat.S_IMODE(after.st_mode) != entry.mode + or bytes(content) != entry.content + ): + raise OSError(errno.ESTALE, "project file changed") + finally: + os.close(child) + directory_after = os.fstat(descriptor) + if stable_metadata(directory_before) != stable_metadata(directory_after) or set( + _list_directory(descriptor) + ) != set(entries): + raise OSError(errno.ESTALE, "project directory changed") + + verify_directory(root_descriptor, tree) + + +def _validate_staged_project( + stage_descriptor: int, + plan: tuple[_ScaffoldFile, ...], + package: str, + release: SupportedRelease, + release_bundle: _ReleaseBundle, +) -> None: + _verify_project_plan(stage_descriptor, plan) + indexed = {item.relative: item for item in plan} + expected_core = _core_project_plan(package, release, release_bundle) + if any(indexed.get(expected.relative) != expected for expected in expected_core): + raise ProjectCreateError( + "project-create-validation-failed", + "The staged project did not satisfy Autoform's project contracts.", + ) + _validate_roadmap_plan(plan) + _verify_project_plan(stage_descriptor, plan) + + +def _validate_roadmap_plan(plan: tuple[_ScaffoldFile, ...]) -> None: + roadmap = [ + item for item in plan if item.relative.startswith("blueprint/roadmap/") and item.relative.endswith(".md") + ] + if len(roadmap) != 1 or roadmap[0].relative != "blueprint/roadmap/README.md": + raise ProjectCreateError( + "project-create-validation-failed", + "The staged project did not satisfy Autoform's project contracts.", + ) + try: + text = roadmap[0].content.decode("utf-8") + except UnicodeError: + raise ProjectCreateError( + "project-create-validation-failed", + "The staged project did not satisfy Autoform's project contracts.", + ) from None + parsed, issues = _parse_node("roadmap", Path("roadmap/README.md"), text) + if issues or parsed is None or parsed.statement_targets or parsed.proof_targets: + raise ProjectCreateError( + "project-create-validation-failed", + "The staged project did not satisfy Autoform's project contracts.", + ) + + +def _rename_noreplace( + source_parent_descriptor: int, + source: str, + target_parent_descriptor: int, + target: str, +) -> None: + libc = ctypes.CDLL(None, use_errno=True) + source_bytes = os.fsencode(source) + target_bytes = os.fsencode(target) + if hasattr(libc, "renameatx_np"): + function = libc.renameatx_np + function.argtypes = [ctypes.c_int, ctypes.c_char_p, ctypes.c_int, ctypes.c_char_p, ctypes.c_uint] + function.restype = ctypes.c_int + result = function( + source_parent_descriptor, + source_bytes, + target_parent_descriptor, + target_bytes, + 0x00000004, + ) + elif hasattr(libc, "renameat2"): + function = libc.renameat2 + function.argtypes = [ctypes.c_int, ctypes.c_char_p, ctypes.c_int, ctypes.c_char_p, ctypes.c_uint] + function.restype = ctypes.c_int + result = function( + source_parent_descriptor, + source_bytes, + target_parent_descriptor, + target_bytes, + 1, + ) + else: + raise ProjectCreateError( + "project-create-safety-unavailable", + "This platform cannot atomically publish a new project without replacement.", + ) + if result == 0: + return + error = ctypes.get_errno() + if error in {errno.EEXIST, errno.ENOTEMPTY}: + raise FileExistsError(error, os.strerror(error), target) + if error in {errno.EINVAL, errno.ENOSYS, errno.ENOTSUP}: + raise ProjectCreateError( + "project-create-safety-unavailable", + "This platform cannot atomically publish a new project without replacement.", + ) + raise OSError(error, os.strerror(error), target) + + +__all__ = ["ProjectCreateError", "ProjectCreateResult", "create_project"] diff --git a/autoform_cli/project/creation-release-lean-v4.32.2-mathlib-v4.32.2.json b/autoform_cli/project/creation-release-lean-v4.32.2-mathlib-v4.32.2.json new file mode 100644 index 00000000..52a2df2d --- /dev/null +++ b/autoform_cli/project/creation-release-lean-v4.32.2-mathlib-v4.32.2.json @@ -0,0 +1,30 @@ +{ + "schema": "autoform-project-creation-release/v1", + "release": { + "id": "lean-v4.32.2-mathlib-v4.32.2", + "lean_toolchain": "leanprover/lean4:v4.32.2", + "mathlib_git": "https://github.com/leanprover-community/mathlib4", + "mathlib_rev": "v4.32.2", + "mathlib_commit": "905b95818eb32af7874a58b427f50c1711a5e96c" + }, + "lake_manifest": "release-manifest-lean-v4.32.2-mathlib-v4.32.2.json", + "production_module_roots": [ + "Aesop", + "Archive", + "Batteries", + "Cache", + "Cli", + "Counterexamples", + "ImportGraph", + "Init", + "Lake", + "Lean", + "LeanSearchClient", + "Mathlib", + "MathlibTest", + "Plausible", + "ProofWidgets", + "Qq", + "Std" + ] +} diff --git a/autoform_cli/project/release-manifest-lean-v4.32.2-mathlib-v4.32.2.json b/autoform_cli/project/release-manifest-lean-v4.32.2-mathlib-v4.32.2.json new file mode 100644 index 00000000..9c0e6027 --- /dev/null +++ b/autoform_cli/project/release-manifest-lean-v4.32.2-mathlib-v4.32.2.json @@ -0,0 +1,117 @@ +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "905b95818eb32af7874a58b427f50c1711a5e96c", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.32.2", + "inherited": false, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.32.0", + "inherited": true, + "configFile": "lakefile.toml" + } + ], + "name": "", + "lakeDir": ".lake", + "fixedToolchain": false +} diff --git a/autoform_cli/scaffold.py b/autoform_cli/scaffold.py index 2a1ff37a..522a3847 100644 --- a/autoform_cli/scaffold.py +++ b/autoform_cli/scaffold.py @@ -46,6 +46,23 @@ _MAX_TEMPLATE_FILE_BYTES = 4 * 1024 * 1024 _MAX_TEMPLATE_TOTAL_BYTES = 16 * 1024 * 1024 _MAX_TEMPLATE_DEPTH = 32 +_REQUIRED_TEMPLATE_PATHS = frozenset( + { + "README.md", + "blueprint/README.md", + "blueprint/coverage/README.md", + "blueprint/gitignore", + "blueprint/javascripts/mathjax.js", + "blueprint/roadmap/README.md", + "blueprint/sources/README.md", + "github/autoform_audit.py", + "github/workflows/autoform-verify.yml", + "github/workflows/blueprint-pages.yml", + "gitignore", + "mkdocs.yml", + "theme/main.html", + } +) def _normalize_autoform_source(source: str, *, allow_github_scp: bool = False) -> str | None: @@ -179,6 +196,13 @@ def as_dict(self) -> dict[str, object]: } +@dataclass(frozen=True, slots=True) +class _ScaffoldFile: + relative: str + content: bytes + mode: int + + def _destination(relative: str) -> str: for template_prefix, real_prefix in _DOTTED.items(): if relative == template_prefix: @@ -214,6 +238,54 @@ def _render(text: str, substitutions: dict[str, str]) -> str: ) +def _scaffold_plan( + template_snapshot: _TemplateSnapshot, + *, + title: str, + repository_url: str, + autoform_source: str, + autoform_ref: str, +) -> tuple[tuple[_ScaffoldFile, ...], tuple[str, ...]]: + template_paths = [relative for relative, _content, _mode in template_snapshot] + if len(template_paths) != len(set(template_paths)) or not _REQUIRED_TEMPLATE_PATHS.issubset( + template_paths + ): + raise ScaffoldError(["the Autoform template tree is incomplete"]) + substitutions = { + "PROJECT_TITLE_YAML": _yaml_scalar(title), + "REPO_URL_YAML": _yaml_scalar(repository_url), + "PROJECT_TITLE": title, + "REPO_URL": repository_url, + "AUTOFORM_SOURCE": autoform_source, + "AUTOFORM_REF": autoform_ref, + "AUTOFORM_SOURCE_YAML": _yaml_scalar(autoform_source), + "AUTOFORM_REF_YAML": _yaml_scalar(autoform_ref), + } + files: list[_ScaffoldFile] = [] + skipped: list[str] = [] + for relative, template_content, template_mode in template_snapshot: + destination = _destination(relative) + if not autoform_ref and relative.startswith("github/"): + skipped.append(destination) + continue + if Path(relative).suffix in {".js", ".html"} or relative.endswith("gitignore"): + content = template_content + else: + try: + text = template_content.decode("utf-8") + except UnicodeError: + raise ScaffoldError(["the Autoform template tree contains invalid text"]) from None + content = _render(text, substitutions).encode("utf-8") + files.append( + _ScaffoldFile( + relative=destination, + content=content, + mode=template_mode, + ) + ) + return tuple(files), tuple(skipped) + + def _atomic_write(destination: Path, content: bytes, *, mode: int) -> None: """Replace *destination* from a same-directory temporary file. @@ -323,46 +395,35 @@ def scaffold_project( # project whose first CI step fails for a reason no file in it explains. So # the ref alone decides: without one the workflows are skipped and reported. unpinned = not ref - substitutions = { - "PROJECT_TITLE_YAML": _yaml_scalar(title.strip()), - "REPO_URL_YAML": _yaml_scalar(repository_url.strip()), - "PROJECT_TITLE": title.strip(), - "REPO_URL": repository_url.strip(), - "AUTOFORM_SOURCE": source, - "AUTOFORM_REF": ref, - "AUTOFORM_SOURCE_YAML": _yaml_scalar(source), - "AUTOFORM_REF_YAML": _yaml_scalar(ref), - } + planned, omitted = _scaffold_plan( + template_snapshot, + title=title.strip(), + repository_url=repository_url.strip(), + autoform_source=source, + autoform_ref=ref, + ) written: list[str] = [] - skipped: list[str] = [] - for relative, template_content, template_mode in template_snapshot: - if unpinned and relative.startswith("github/"): - skipped.append(_destination(relative)) - continue - destination = root / _destination(relative) + skipped = list(omitted) + for planned_file in planned: + destination = root / planned_file.relative # Confine every write, not just the root. Reject links outright before # checking whether the destination should be skipped: `exists()` is # false for a dangling symlink, but opening that path still follows the # link and can create a file outside the project. probe = root - for part in Path(_destination(relative)).parts: + for part in Path(planned_file.relative).parts: probe = probe / part if probe.is_symlink() or (probe.exists() and not _within(probe, root)): raise ScaffoldError( [f"refusing to write outside the project through a link: {probe}"] ) if destination.exists() and not force: - skipped.append(_destination(relative)) + skipped.append(planned_file.relative) continue destination.parent.mkdir(parents=True, exist_ok=True) - if Path(relative).suffix in {".js", ".html"} or relative.endswith("gitignore"): - content = template_content - else: - rendered = _render(template_content.decode("utf-8"), substitutions) - content = rendered.encode("utf-8") - _atomic_write(destination, content, mode=template_mode) - written.append(_destination(relative)) + _atomic_write(destination, planned_file.content, mode=planned_file.mode) + written.append(planned_file.relative) return ScaffoldResult(title.strip(), tuple(written), tuple(skipped), unpinned) diff --git a/skills/develop-plugin/SKILL.md b/skills/develop-plugin/SKILL.md index 249b21b6..135c70a6 100644 --- a/skills/develop-plugin/SKILL.md +++ b/skills/develop-plugin/SKILL.md @@ -10,17 +10,19 @@ description: >- Treat Autoform as an example-based plugin in an independent formalization repository. Use the Cabannes thesis as a consumer example. -Inspect the worktree, state a consumer scenario, and observe installed behavior. -Name a refactor's invariant. +Inspect the worktree, state a consumer scenario, observe installed behavior, +and name refactor invariants. -Treat user nudges during real work as product evidence. Distill reusable ones -into the owning skill as a trigger, decision rule, and action. -Ensure future agents need less steering. -Preserve the insight, not the transcript or consumer choice. -Add a focused test and acceptance assertion in `tests/test_skill_examples.py`. +Treat user nudges as product evidence. Encode reusable triggers and decisions +so future agents need less steering. Preserve insight, not the transcript, and +add a focused assertion in `tests/test_skill_examples.py`. -Implement reusable plugin behavior. Keep Cabannes-specific facts in the example -and references; demonstrate outcomes without special-casing them. +For each Lean/Mathlib release, regenerate `production_module_roots` from Lake +package configs. Update the private creation bundle, catalog identity, and +complete `lake update` manifest together; run `lake build`. +A direct-Mathlib-only manifest is invalid. + +Implement reusable plugin behavior. Keep Cabannes-specific facts in examples. Keep plugin and formalization roots distinct. Agents can infer routine details; keep skills to non-obvious constraints and fragile domain steps. @@ -37,7 +39,8 @@ make check-example ``` Run `lake build` when example Lean results change. Validate edited skills and -the manifest with skill-creator and plugin-creator. Use cachebuster and reinstall -only to test installed discovery in a new thread. +the manifest with skill-creator and plugin-creator. Reinstall only to test +installed discovery in a new thread. + Treat rewritten private declaration safety as fail-closed evidence: correlate the official user name to its lexical declaration by source coordinates. diff --git a/skills/setup/SKILL.md b/skills/setup/SKILL.md index 9f38e3d5..03086810 100644 --- a/skills/setup/SKILL.md +++ b/skills/setup/SKILL.md @@ -31,13 +31,28 @@ package, check the current matching stable Lean/Mathlib release, update branch and immutable workflow pins, and merge rather than overwrite. Its populated thesis notes illustrate later skills; Setup does not reproduce that mathematics. -For a new repository, first create a standard Lean/Lake project using the -recommended pair reported by `autoform project versions --json`. For a new or -incomplete Autoform installation inside that repository: +For a new repository, require a target directory that does not already exist. +Have the user select a release from `autoform project versions`, then create the +complete local project atomically: -- create or repair a buildable Lean project with matching `lean-toolchain` and - Mathlib revisions; and -- write the blueprint vault, site configuration, and CI with `autoform init`. +```bash +autoform project provenance --json +autoform project new --package --release \ + --autoform-source --autoform-ref +``` + +The catalog is a bundled known-good allowlist, not an automatic selection +mechanism. `project new` writes matching `lean-toolchain` and Mathlib revisions, +the Lean shell, and the Autoform vault without running Git, Lake, Lean, or +network operations; it never overwrites an existing target. It fails closed on +platforms without the required POSIX filesystem operations, including Windows. +Omit both provenance flags if verification is unavailable; the command then +omits CI workflows. Do not invent version pairs, sources, or revisions, and do +not copy the populated example as a project generator. + +For an incomplete existing repository, preserve its authored configuration and +use `autoform init` only for the Autoform vault/site overlay until the dedicated +repair command is available. `autoform init` is the whole vault: `blueprint/` with its landing page, `roadmap/README.md`, `coverage/`, and `sources/`, plus `mkdocs.yml`, the theme diff --git a/tests/test_plugin_runtime.py b/tests/test_plugin_runtime.py index e2ff4073..60d10478 100644 --- a/tests/test_plugin_runtime.py +++ b/tests/test_plugin_runtime.py @@ -102,6 +102,9 @@ def test_wheel_contains_only_the_minimal_runtime(repo_root, tmp_path): "autoform_cli/graph.py", "autoform_cli/probes/skeleton_probe.lean", "autoform_cli/visualize.py", + "autoform_cli/project/create.py", + "autoform_cli/project/creation-release-lean-v4.32.2-mathlib-v4.32.2.json", + "autoform_cli/project/release-manifest-lean-v4.32.2-mathlib-v4.32.2.json", "autoform_cli/project/releases.json", "servers/lean_client.py", "servers/lean_runtime.py", @@ -181,18 +184,8 @@ def test_wheel_contains_only_the_minimal_runtime(repo_root, tmp_path): assert installed.returncode == 0, installed.stderr command = environment / ("Scripts/autoform.exe" if sys.platform == "win32" else "bin/autoform") outside = tmp_path / "outside" + outside.mkdir() project = outside / "project" - project.mkdir(parents=True) - (project / "lakefile.toml").write_text( - 'name = "WheelProject"\n' - '[[require]]\nname = "mathlib"\n' - 'git = "https://github.com/leanprover-community/mathlib4.git"\n' - 'rev = "v4.32.2"\n', - encoding="utf-8", - ) - (project / "lean-toolchain").write_text( - "leanprover/lean4:v4.32.2\n", encoding="utf-8" - ) versions = subprocess.run( [str(command), "project", "versions", "--json"], cwd=outside, @@ -201,6 +194,24 @@ def test_wheel_contains_only_the_minimal_runtime(repo_root, tmp_path): ) assert versions.returncode == 0, versions.stderr assert json.loads(versions.stdout)["schema"] == "autoform-project-release-catalog/v1" + creation = subprocess.run( + [ + str(command), + "project", + "new", + str(project), + "--package", + "WheelProject", + "--release", + "lean-v4.32.2-mathlib-v4.32.2", + "--json", + ], + cwd=outside, + capture_output=True, + text=True, + ) + assert creation.returncode == 0, creation.stderr + assert json.loads(creation.stdout)["package"] == "WheelProject" inspection = subprocess.run( [str(command), "project", "inspect", str(project), "--json"], cwd=outside, diff --git a/tests/test_project_create.py b/tests/test_project_create.py new file mode 100644 index 00000000..3d1d6ba6 --- /dev/null +++ b/tests/test_project_create.py @@ -0,0 +1,1354 @@ +from __future__ import annotations + +import errno +import json +import os +import shutil +import socket +import stat +import subprocess +import sys +import threading +from dataclasses import replace +from pathlib import Path + +import pytest + +from autoform_cli.__main__ import main +from autoform_cli.graph import load_graph +from autoform_cli.project import ( + ProjectCreateError, + create_project, + inspect_project, + load_release_catalog, +) +from autoform_cli.project import create as create_module + +_RELEASE = "lean-v4.32.2-mathlib-v4.32.2" + + +def test_creation_never_discovers_git_provenance(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + from autoform_cli import scaffold as scaffold_module + + def forbidden(): + raise AssertionError("project new invoked Git-backed plugin discovery") + + monkeypatch.setattr(scaffold_module, "plugin_pin", forbidden) + target = tmp_path / "Project" + result = create_project(target, package="Project", release_id=_RELEASE) + + assert not result.workflows_pinned + assert not (target / ".github/workflows/autoform-verify.yml").exists() + assert not (target / ".github/workflows/blueprint-pages.yml").exists() + + +def test_creation_accepts_only_a_complete_workflow_pin(tmp_path: Path) -> None: + target = tmp_path / "Project" + source = "https://example.test/owner/autoform.git" + revision = "A" * 40 + + result = create_project( + target, + package="Project", + release_id=_RELEASE, + autoform_source=source, + autoform_ref=revision, + ) + + assert result.workflows_pinned + workflow = (target / ".github/workflows/autoform-verify.yml").read_text(encoding="utf-8") + assert f'AUTOFORM_SOURCE: "{source}"' in workflow + assert f'AUTOFORM_REF: "{revision.lower()}"' in workflow + + +@pytest.mark.parametrize( + ("source", "revision"), + [ + ("https://example.test/owner/autoform.git", ""), + ("", "1" * 40), + ("https://example.test/owner/autoform.git", "main"), + ("https://user:secret@example.test/autoform.git", "1" * 40), + ], +) +def test_creation_rejects_invalid_provenance_before_writing(source: str, revision: str, tmp_path: Path) -> None: + target = tmp_path / "Project" + + with pytest.raises(ProjectCreateError) as raised: + create_project( + target, + package="Project", + release_id=_RELEASE, + autoform_source=source, + autoform_ref=revision, + ) + + assert raised.value.code == "project-provenance-invalid" + assert not target.exists() + assert not list(tmp_path.glob(".autoform-new-*")) + + +def test_creation_with_an_explicit_pin_stays_offline(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + from autoform_cli import provenance, scaffold as scaffold_module + + def forbidden(*args, **kwargs): + raise AssertionError("project new crossed its offline boundary") + + monkeypatch.setattr(scaffold_module, "plugin_pin", forbidden) + monkeypatch.setattr(provenance, "verify_plugin_provenance", forbidden) + monkeypatch.setattr(subprocess, "Popen", forbidden) + monkeypatch.setattr(subprocess, "run", forbidden) + monkeypatch.setattr(socket, "create_connection", forbidden) + + result = create_project( + tmp_path / "Project", + package="Project", + release_id=_RELEASE, + autoform_source="https://example.test/owner/autoform.git", + autoform_ref="1" * 40, + ) + + assert result.workflows_pinned + + +def test_unsafe_local_templates_use_the_project_error_contract( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + templates = tmp_path / "templates" + templates.mkdir() + (templates / "escape").symlink_to(tmp_path / "missing") + target = tmp_path / "Project" + monkeypatch.setattr(create_module, "_TEMPLATES", templates) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-validation-failed" + assert not target.exists() + assert not list(tmp_path.glob(".autoform-new-*")) + + +def test_incomplete_local_templates_are_not_published( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + templates = tmp_path / "templates" + shutil.copytree(create_module._TEMPLATES, templates) + (templates / "theme/main.html").unlink() + target = tmp_path / "Project" + monkeypatch.setattr(create_module, "_TEMPLATES", templates) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-validation-failed" + assert not target.exists() + assert not list(tmp_path.glob(".autoform-new-*")) + + +def test_missing_release_manifest_is_not_published( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + target = tmp_path / "Project" + release = load_release_catalog().recommended + descriptor = create_module._load_creation_release_descriptor(release) + monkeypatch.setattr( + create_module, + "_load_creation_release_descriptor", + lambda _release: replace( + descriptor, manifest_resource="missing-release-manifest.json" + ), + ) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-validation-failed" + assert not target.exists() + assert not list(tmp_path.glob(".autoform-new-*")) + + +def test_creates_complete_supported_project(tmp_path: Path) -> None: + target = tmp_path / "FiniteFlat" + result = create_project(target, package="FiniteFlat", release_id=_RELEASE) + + assert result.package == "FiniteFlat" + assert result.release == _RELEASE + assert result.target == "FiniteFlat" + assert (target / "lean-toolchain").read_text(encoding="utf-8") == ("leanprover/lean4:v4.32.2\n") + assert (target / "lakefile.toml").read_text(encoding="utf-8") == ( + 'name = "FiniteFlat"\n' + 'version = "0.1.0"\n' + 'defaultTargets = ["FiniteFlat"]\n\n' + "[[require]]\n" + 'name = "mathlib"\n' + 'git = "https://github.com/leanprover-community/mathlib4"\n' + 'rev = "v4.32.2"\n\n' + "[[lean_lib]]\n" + 'name = "FiniteFlat"\n' + 'srcDir = "src"\n' + ) + manifest = json.loads((target / "lake-manifest.json").read_text(encoding="utf-8")) + assert manifest["version"] == "1.2.0" + assert manifest["name"] == "FiniteFlat" + assert {entry["name"]: entry["rev"] for entry in manifest["packages"]} == { + "Cli": "88679d088c9720c27ebdf2ba4dafe17341747f94", + "LeanSearchClient": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "Qq": "38d591e778f100aec9762bb582f9c7f55f50e9dc", + "aesop": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", + "batteries": "023ce7d62a0531e22a5331e20b587817a80d49ff", + "importGraph": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12", + "mathlib": "905b95818eb32af7874a58b427f50c1711a5e96c", + "plausible": "e12c1910fe855cbfc38803cd4e55543906d5fa62", + "proofwidgets": "6e311e2a844da9b2cc3971187df2fe0066947b93", + } + direct = [entry for entry in manifest["packages"] if not entry["inherited"]] + assert len(direct) == 1 + assert direct[0]["name"] == "mathlib" + assert direct[0]["inputRev"] == "v4.32.2" + assert (target / "src/FiniteFlat.lean").read_text(encoding="utf-8") == ( + "import Mathlib\n\n" + "namespace FiniteFlat\n\n" + "/-- Marker declaration for the initial project build. -/\n" + "def autoformProjectInitialized : Bool := true\n\n" + "end FiniteFlat\n" + ) + inspection = inspect_project(target) + assert inspection.ok + assert inspection.compatibility.status == "supported" + assert inspection.compatibility.release == _RELEASE + assert inspection.mathlib is not None + assert inspection.mathlib.rev == "905b95818eb32af7874a58b427f50c1711a5e96c" + assert set(load_graph(target / "blueprint").nodes) == {"roadmap"} + assert stat.S_IMODE(target.stat().st_mode) == 0o755 + assert not list(tmp_path.glob(".autoform-new-*")) + + +@pytest.mark.parametrize( + "package", + [ + "", + "A" * 256, + "finiteFlat", + "Finite_Flat", + "Finite.Flat", + "../FiniteFlat", + "Finite Flat", + 'Finite"Flat', + "Aesop", + "Archive", + "Batteries", + "Cache", + "Cli", + "Counterexamples", + "ImportGraph", + "Lean", + "LeanSearchClient", + "Lake", + "Plausible", + "ProofWidgets", + "Qq", + "Std", + "Type", + "Sort", + "Prop", + "Init", + "Mathlib", + "MathlibTest", + "MATHLIB", + "MathLib", + "LEAN", + "STD", + ], +) +def test_rejects_invalid_package_before_writing(tmp_path: Path, package: str) -> None: + target = tmp_path / "project" + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package=package, release_id=_RELEASE) + assert raised.value.code == "project-name-invalid" + assert not target.exists() + assert not list(tmp_path.glob(".autoform-new-*")) + + +def test_every_release_has_creation_contracts() -> None: + public_catalog = load_release_catalog() + public_json = public_catalog.to_json() + assert "production_module_roots" not in public_json + assert "project_manifest" not in public_json + for release in public_catalog.releases: + descriptor = create_module._load_creation_release_descriptor(release) + bundle = create_module._load_release_bundle(release) + assert descriptor.manifest_resource.endswith(".json") + assert bundle.module_roots == { + "Aesop", + "Archive", + "Batteries", + "Cache", + "Cli", + "Counterexamples", + "ImportGraph", + "Init", + "Lake", + "Lean", + "LeanSearchClient", + "Mathlib", + "MathlibTest", + "Plausible", + "ProofWidgets", + "Qq", + "Std", + } + + +@pytest.mark.parametrize("missing", ["Aesop", "Archive", "Counterexamples"]) +def test_release_metadata_must_cover_manifest_and_mathlib_production_roots( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch, missing: str +) -> None: + release = load_release_catalog().recommended + descriptor = create_module._load_creation_release_descriptor(release) + changed = replace( + descriptor, + module_roots=tuple(root for root in descriptor.module_roots if root != missing), + ) + monkeypatch.setattr( + create_module, "_load_creation_release_descriptor", lambda _release: changed + ) + + with pytest.raises(ProjectCreateError) as raised: + create_project(tmp_path / "Project", package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-validation-failed" + assert not list(tmp_path.iterdir()) + + +@pytest.mark.parametrize( + "corruption", + ["top-level-key", "revision", "credentials", "traversal", "inherited-type"], +) +def test_release_bundle_rejects_non_generated_manifest_shapes(corruption: str) -> None: + release = load_release_catalog().recommended + descriptor = create_module._load_creation_release_descriptor(release) + bundle = create_module._load_release_bundle(release) + payload = json.loads(bundle.manifest_bytes) + if corruption == "top-level-key": + payload["unexpected"] = True + elif corruption == "revision": + payload["packages"][1]["rev"] = "main" + elif corruption == "credentials": + payload["packages"][1]["url"] = "https://user:secret@example.test/repo" + elif corruption == "traversal": + payload["packages"][1]["manifestFile"] = "../lake-manifest.json" + else: + payload["packages"][1]["inherited"] = 1 + + with pytest.raises(ProjectCreateError) as raised: + create_module._parse_release_bundle( + json.dumps(payload).encode(), release, descriptor.module_roots + ) + + assert raised.value.code == "project-create-validation-failed" + + +def test_rejects_non_string_package_before_writing(tmp_path: Path) -> None: + target = tmp_path / "project" + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package=123, release_id=_RELEASE) # type: ignore[arg-type] + + assert raised.value.code == "project-name-invalid" + assert not target.exists() + assert not list(tmp_path.glob(".autoform-new-*")) + + +def test_open_parent_descriptor_rechecks_the_generated_module_filename_limit( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + package = "A" * 256 + monkeypatch.setattr( + create_module, "_validate_package", lambda _package, _parent: package + ) + + with pytest.raises(ProjectCreateError) as raised: + create_project(tmp_path / "project", package=package, release_id=_RELEASE) + + assert raised.value.code == "project-name-invalid" + assert not list(tmp_path.iterdir()) + + +def test_rejects_unknown_release_before_writing(tmp_path: Path) -> None: + target = tmp_path / "project" + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id="unknown") + assert raised.value.code == "project-release-unknown" + assert not target.exists() + + +def test_long_valid_target_name_does_not_expand_the_stage_name(tmp_path: Path) -> None: + name_limit = os.pathconf(tmp_path, "PC_NAME_MAX") + if name_limit < 64: + pytest.skip("filesystem name limit is too small for this boundary test") + target = tmp_path / ("p" * name_limit) + + result = create_project(target, package="Project", release_id=_RELEASE) + + assert result.target == target.name + assert inspect_project(target).ok + assert not list(tmp_path.glob(".autoform-new-*")) + + +def test_embedded_nul_target_uses_the_stable_error_contract(tmp_path: Path, capsys) -> None: + target = os.fspath(tmp_path / "bad\0name") + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + assert raised.value.code == "project-target-invalid" + + assert ( + main( + [ + "project", + "new", + target, + "--package", + "Project", + "--release", + _RELEASE, + "--json", + ] + ) + == 1 + ) + assert json.loads(capsys.readouterr().out)["error"]["code"] == "project-target-invalid" + + +@pytest.mark.parametrize("target", ["", ".", "..", "/"]) +def test_target_must_name_a_directory(target: str) -> None: + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-target-invalid" + + +@pytest.mark.parametrize("kind", ["file", "directory", "symlink", "broken-symlink"]) +def test_never_overwrites_existing_target(tmp_path: Path, kind: str) -> None: + target = tmp_path / "project" + if kind == "file": + target.write_bytes(b"authored\n") + elif kind == "directory": + target.mkdir() + (target / "authored").write_bytes(b"authored\n") + else: + real = tmp_path / "real" + if kind == "symlink": + real.mkdir() + target.symlink_to(real, target_is_directory=True) + before = sorted( + (path.relative_to(tmp_path).as_posix(), path.read_bytes()) + for path in tmp_path.rglob("*") + if path.is_file() and not path.is_symlink() + ) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-target-exists" + after = sorted( + (path.relative_to(tmp_path).as_posix(), path.read_bytes()) + for path in tmp_path.rglob("*") + if path.is_file() and not path.is_symlink() + ) + assert after == before + + +def test_normal_macos_tmp_alias_is_supported() -> None: + if not Path("/tmp").is_symlink(): + pytest.skip("platform has no /tmp alias") + parent = Path("/tmp") / f"autoform-new-test-{os.getpid()}" + parent.mkdir() + target = parent / "Project" + try: + create_project(target, package="Project", release_id=_RELEASE) + assert inspect_project(parent.resolve() / "Project").ok + finally: + shutil.rmtree(parent, ignore_errors=True) + + +def test_rejects_nonsticky_shared_parent(tmp_path: Path) -> None: + parent = tmp_path / "shared" + parent.mkdir(mode=0o777) + parent.chmod(0o777) + with pytest.raises(ProjectCreateError) as raised: + create_project(parent / "Project", package="Project", release_id=_RELEASE) + assert raised.value.code == "project-parent-unsafe" + + +def test_rechecks_parent_mode_on_the_open_descriptor( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + parent = tmp_path / "shared" + parent.mkdir(mode=0o777) + parent.chmod(0o777) + target = parent / "Project" + monkeypatch.setattr(create_module, "_validate_target", lambda _target: target) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-parent-unsafe" + assert not target.exists() + assert not list(parent.glob(".autoform-new-*")) + + +def test_sticky_shared_parent_requires_a_trusted_descriptor_owner( + monkeypatch: pytest.MonkeyPatch, +) -> None: + monkeypatch.setattr(create_module.os, "geteuid", lambda: 1000) + mode = stat.S_IFDIR | stat.S_ISVTX | 0o777 + + assert not create_module._unsafe_parent_metadata(mode, 0) + assert not create_module._unsafe_parent_metadata(mode, 1000) + assert create_module._unsafe_parent_metadata(mode, 2000) + + +def test_fresh_parent_binding_compares_owner_as_well_as_device_and_inode( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + descriptor = create_module._open_parent(tmp_path) + expected = create_module._descriptor_identity(descriptor) + monkeypatch.setattr( + create_module, + "_descriptor_identity", + lambda _descriptor: (expected[0], expected[1], expected[2] + 1), + ) + try: + with pytest.raises(ProjectCreateError) as raised: + create_module._reopen_bound_parent(tmp_path, expected) + finally: + os.close(descriptor) + + assert raised.value.code == "project-parent-changed" + + +def test_missing_directory_capability_uses_stable_error(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + target = tmp_path / "project" + monkeypatch.setattr( + create_module.os, + "supports_dir_fd", + create_module.os.supports_dir_fd - {create_module.os.mkdir}, + ) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-safety-unavailable" + assert not target.exists() + assert not list(tmp_path.glob(".autoform-new-*")) + + +def test_injected_build_failure_preserves_the_empty_stage(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + target = tmp_path / "project" + + def fail(*args, **kwargs): + raise OSError("injected") + + monkeypatch.setattr(create_module, "_materialize_project", fail) + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + assert raised.value.code == "project-create-failed" + assert ".autoform-new-* stage may remain" in raised.value.message + assert not target.exists() + stages = list(tmp_path.glob(".autoform-new-*")) + assert len(stages) == 1 + assert not list(stages[0].iterdir()) + + +def test_injected_validation_failure_preserves_stage_for_safe_recovery( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + target = tmp_path / "project" + + def fail(*args, **kwargs): + raise ProjectCreateError("project-create-validation-failed", "invalid") + + monkeypatch.setattr(create_module, "_validate_staged_project", fail) + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + assert raised.value.code == "project-create-validation-failed" + assert ".autoform-new-* stage may remain" in raised.value.message + assert not target.exists() + stages = list(tmp_path.glob(".autoform-new-*")) + assert len(stages) == 1 + assert (stages[0] / "lean-toolchain").is_file() + + +def test_invalid_planned_roadmap_is_never_published(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + target = tmp_path / "project" + original = create_module._build_project_plan + + def corrupt(*args, **kwargs): + plan, pinned = original(*args, **kwargs) + changed = tuple( + type(item)(item.relative, b"No H1 title.\n", item.mode) + if item.relative == "blueprint/roadmap/README.md" + else item + for item in plan + ) + return changed, pinned + + monkeypatch.setattr(create_module, "_build_project_plan", corrupt) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-validation-failed" + assert not target.exists() + assert not list(tmp_path.glob(".autoform-new-*")) + + +@pytest.mark.parametrize("corruption", ["container", "relative", "content", "mode"]) +def test_plan_requires_exact_types_and_safe_file_modes_before_writing( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch, corruption: str +) -> None: + original = create_module._build_project_plan + + def corrupt(*args, **kwargs): + plan, pinned = original(*args, **kwargs) + if corruption == "container": + return list(plan), pinned + first, *rest = plan + changed = { + "relative": type(first)(Path(first.relative), first.content, first.mode), + "content": type(first)(first.relative, memoryview(first.content), first.mode), + "mode": type(first)(first.relative, first.content, 0o666), + }[corruption] + return (changed, *rest), pinned + + monkeypatch.setattr(create_module, "_build_project_plan", corrupt) + + with pytest.raises(ProjectCreateError) as raised: + create_project(tmp_path / "Project", package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-validation-failed" + assert not list(tmp_path.iterdir()) + + +def test_close_failure_after_publish_reports_that_the_target_exists( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + target = tmp_path / "project" + original_rename = create_module._rename_noreplace + original_reopen = create_module._reopen_bound_parent + original_close = create_module.os.close + published = False + cleanup_ready = False + reopen_calls = 0 + failed = False + + def publish(*args): + nonlocal published + original_rename(*args) + published = True + + def reopen(*args): + nonlocal cleanup_ready, reopen_calls + descriptor = original_reopen(*args) + reopen_calls += 1 + if reopen_calls == 2: + cleanup_ready = True + return descriptor + + def close_after_publish(descriptor): + nonlocal failed + original_close(descriptor) + if published and cleanup_ready and not failed: + failed = True + raise OSError("injected close failure") + + monkeypatch.setattr(create_module, "_rename_noreplace", publish) + monkeypatch.setattr(create_module, "_reopen_bound_parent", reopen) + monkeypatch.setattr(create_module.os, "close", close_after_publish) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-commit-uncertain" + assert "target names the published project" in raised.value.message + assert "parent directory was synced" in raised.value.message + assert "final descriptor cleanup failed" in raised.value.message + assert inspect_project(target).ok + assert not list(tmp_path.glob(".autoform-new-*")) + + +def test_fsync_failure_after_publish_reports_that_the_target_exists( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + target = tmp_path / "project" + original_rename = create_module._rename_noreplace + original_fsync = create_module.os.fsync + published = False + failed = False + + def publish(*args): + nonlocal published + original_rename(*args) + published = True + + def fail_after_publish(descriptor): + nonlocal failed + if published and not failed: + failed = True + raise OSError("injected fsync failure") + original_fsync(descriptor) + + monkeypatch.setattr(create_module, "_rename_noreplace", publish) + monkeypatch.setattr(create_module.os, "fsync", fail_after_publish) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-commit-uncertain" + assert "target names the published project" in raised.value.message + assert "parent-directory sync was not confirmed" in raised.value.message + assert inspect_project(target).ok + assert not list(tmp_path.glob(".autoform-new-*")) + + +def test_interrupt_after_publish_reports_that_the_target_exists( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + target = tmp_path / "project" + original_rename = create_module._rename_noreplace + original_fsync = create_module.os.fsync + published = False + + def publish(*args): + nonlocal published + original_rename(*args) + published = True + + def interrupt_after_publish(descriptor): + if published: + raise KeyboardInterrupt + original_fsync(descriptor) + + monkeypatch.setattr(create_module, "_rename_noreplace", publish) + monkeypatch.setattr(create_module.os, "fsync", interrupt_after_publish) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-commit-uncertain" + assert inspect_project(target).ok + assert not list(tmp_path.glob(".autoform-new-*")) + + +def test_rename_exception_after_commit_reports_that_the_target_exists( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + target = tmp_path / "project" + original = create_module._rename_noreplace + + def commit_then_fail(*args): + original(*args) + raise OSError("injected post-rename failure") + + monkeypatch.setattr(create_module, "_rename_noreplace", commit_then_fail) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-commit-uncertain" + assert inspect_project(target).ok + assert not list(tmp_path.glob(".autoform-new-*")) + + +def test_detached_stage_after_publication_attempt_reports_uncertain_commit( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + target = tmp_path / "project" + moved = tmp_path / "moved" + original = create_module._rename_noreplace + + def commit_move_then_fail(*args): + original(*args) + target.rename(moved) + raise OSError("injected post-rename failure") + + monkeypatch.setattr(create_module, "_rename_noreplace", commit_move_then_fail) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-commit-uncertain" + assert "neither the target nor the preserved stage names the project" in raised.value.message + assert not target.exists() + assert inspect_project(moved).ok + + +def test_publication_capability_error_remains_actionable(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + target = tmp_path / "project" + + def unavailable(*args): + raise ProjectCreateError( + "project-create-safety-unavailable", + "Atomic no-replace rename is unavailable.", + ) + + monkeypatch.setattr(create_module, "_rename_noreplace", unavailable) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-safety-unavailable" + assert ".autoform-new-* stage may remain" in raised.value.message + assert not target.exists() + assert len(list(tmp_path.glob(".autoform-new-*"))) == 1 + + +def test_unsupported_rename_flag_uses_capability_error( + monkeypatch: pytest.MonkeyPatch, +) -> None: + class FailingRename: + argtypes = None + restype = None + + def __call__(self, *args): + return -1 + + class Libc: + renameat2 = FailingRename() + + monkeypatch.setattr(create_module.ctypes, "CDLL", lambda *args, **kwargs: Libc()) + monkeypatch.setattr(create_module.ctypes, "get_errno", lambda: errno.EINVAL) + + with pytest.raises(ProjectCreateError) as raised: + create_module._rename_noreplace(3, "stage", 3, "target") + + assert raised.value.code == "project-create-safety-unavailable" + + +def test_late_target_race_remains_distinguishable(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + target = tmp_path / "project" + + def lose_race(*args): + target.mkdir() + (target / "KEEP").write_text("keep\n", encoding="utf-8") + raise FileExistsError + + monkeypatch.setattr(create_module, "_rename_noreplace", lose_race) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-target-exists" + assert ".autoform-new-* stage may remain" in raised.value.message + assert (target / "KEEP").read_text(encoding="utf-8") == "keep\n" + assert len(list(tmp_path.glob(".autoform-new-*"))) == 1 + + +@pytest.mark.skipif( + os.name != "posix" or not hasattr(os, "O_DIRECTORY"), + reason="atomic no-replace publication is POSIX-only", +) +def test_real_noreplace_syscall_preserves_a_late_existing_target(tmp_path: Path) -> None: + source = tmp_path / "stage" + target = tmp_path / "target" + source.mkdir() + target.mkdir() + (source / "FROM_STAGE").write_text("stage\n", encoding="utf-8") + (target / "KEEP").write_text("target\n", encoding="utf-8") + descriptor = os.open(tmp_path, os.O_RDONLY | os.O_DIRECTORY) + try: + with pytest.raises(FileExistsError): + create_module._rename_noreplace(descriptor, source.name, descriptor, target.name) + finally: + os.close(descriptor) + + assert (source / "FROM_STAGE").read_text(encoding="utf-8") == "stage\n" + assert (target / "KEEP").read_text(encoding="utf-8") == "target\n" + + +def test_requested_parent_rebind_before_publish_preserves_the_stage( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + parent = tmp_path / "parent" + moved = tmp_path / "moved-parent" + parent.mkdir() + target = parent / "Project" + original = create_module._validate_staged_project + + def rebind(*args, **kwargs) -> None: + original(*args, **kwargs) + parent.rename(moved) + parent.mkdir() + + monkeypatch.setattr(create_module, "_validate_staged_project", rebind) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-parent-changed" + assert ".autoform-new-* stage may remain" in raised.value.message + assert not (parent / "Project").exists() + stages = list(moved.glob(".autoform-new-*")) + assert len(stages) == 1 + assert (stages[0] / "lean-toolchain").is_file() + + +def test_requested_parent_rebind_after_parent_sync_reports_exact_state( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + parent = tmp_path / "parent" + moved = tmp_path / "moved-parent" + parent.mkdir() + target = parent / "Project" + original = create_module._reopen_bound_parent + calls = 0 + + def rebind(path: Path, expected_identity: tuple[int, int, int]) -> int: + nonlocal calls + calls += 1 + if calls == 2: + parent.rename(moved) + parent.mkdir() + return original(path, expected_identity) + + monkeypatch.setattr(create_module, "_reopen_bound_parent", rebind) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert calls == 2 + assert raised.value.code == "project-create-commit-uncertain" + assert "was published and its original parent directory was synced" in raised.value.message + assert "requested parent path no longer names that directory" in raised.value.message + assert not (parent / "Project").exists() + assert inspect_project(moved / "Project").ok + + +def test_postpublish_parent_recheck_failure_does_not_claim_a_rebind( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + target = tmp_path / "Project" + original = create_module._reopen_bound_parent + calls = 0 + + def fail_second(path: Path, expected_identity: tuple[int, int, int]) -> int: + nonlocal calls + calls += 1 + if calls == 2: + raise ProjectCreateError( + "project-parent-unverifiable", + "The requested parent path could not be reverified safely.", + ) + return original(path, expected_identity) + + monkeypatch.setattr(create_module, "_reopen_bound_parent", fail_second) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-commit-uncertain" + assert "could not reopen the requested parent path" in raised.value.message + assert "no longer names" not in raised.value.message + assert inspect_project(target).ok + + +def test_workspace_substitution_fails_before_publication(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + target = tmp_path / "project" + original = create_module._validate_staged_project + + def substitute(*args, **kwargs) -> None: + original(*args, **kwargs) + stage = next(tmp_path.glob(".autoform-new-*")) + moved = stage.with_name(f"{stage.name}-owned") + stage.rename(moved) + stage.mkdir(mode=0o700) + (stage / "FOREIGN").write_text("foreign\n", encoding="utf-8") + + monkeypatch.setattr(create_module, "_validate_staged_project", substitute) + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + assert raised.value.code == "project-create-failed" + assert not target.exists() + assert any(path.name == "FOREIGN" for path in tmp_path.rglob("FOREIGN")) + + +def test_corrupt_core_plan_is_rejected_without_path_based_inspection( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + target = tmp_path / "project" + original = create_module._build_project_plan + + def corrupt(*args, **kwargs): + plan, pinned = original(*args, **kwargs) + changed = tuple( + type(item)(item.relative, b"leanprover/lean4:v0.0.0\n", item.mode) + if item.relative == "lean-toolchain" + else item + for item in plan + ) + return changed, pinned + + monkeypatch.setattr(create_module, "_build_project_plan", corrupt) + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + assert raised.value.code == "project-create-validation-failed" + assert not target.exists() + + +def test_stage_path_substitution_never_writes_to_symlink_target( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + target = tmp_path / "project" + victim = tmp_path / "victim" + victim.mkdir() + (victim / "KEEP").write_text("keep\n", encoding="utf-8") + original = create_module._materialize_project + + def substitute(stage_descriptor, plan) -> None: + stage = next(tmp_path.glob(".autoform-new-*")) + stage.rename(stage.with_name(f"{stage.name}-owned")) + stage.symlink_to(victim, target_is_directory=True) + original(stage_descriptor, plan) + + monkeypatch.setattr(create_module, "_materialize_project", substitute) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-failed" + assert not target.exists() + assert (victim / "KEEP").read_text(encoding="utf-8") == "keep\n" + assert sorted(path.name for path in victim.iterdir()) == ["KEEP"] + + +def test_stage_open_failure_preserves_the_owned_empty_stage(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + target = tmp_path / "project" + original = create_module._open_stage + + def fail_first_open(parent_descriptor: int, stage_name: str) -> int: + if stage_name.startswith(".autoform-new-"): + raise OSError("injected stage open failure") + return original(parent_descriptor, stage_name) + + monkeypatch.setattr(create_module, "_open_stage", fail_first_open) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-failed" + assert not target.exists() + stages = list(tmp_path.glob(".autoform-new-*")) + assert len(stages) == 1 + assert not list(stages[0].iterdir()) + + +def test_failure_path_never_attempts_recursive_deletion(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + target = tmp_path / "project" + + def fail(*args, **kwargs): + raise OSError("injected") + + def forbidden(*args, **kwargs): + raise AssertionError("project creation attempted destructive cleanup") + + monkeypatch.setattr(create_module, "_validate_staged_project", fail) + monkeypatch.setattr(create_module.os, "unlink", forbidden) + monkeypatch.setattr(create_module.os, "rmdir", forbidden) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-failed" + assert not target.exists() + + +def test_failure_cleanup_never_recurses_into_a_foreign_directory( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + target = tmp_path / "project" + victim = tmp_path / "victim" + victim.mkdir() + (victim / "KEEP").write_text("keep\n", encoding="utf-8") + original = create_module._validate_staged_project + + def substitute(*args, **kwargs): + original(*args, **kwargs) + stage = next(tmp_path.glob(".autoform-new-*")) + (stage / "blueprint").rename(stage / "owned-blueprint") + victim.rename(stage / "blueprint") + raise OSError("injected") + + monkeypatch.setattr(create_module, "_validate_staged_project", substitute) + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-failed" + assert not target.exists() + stages = list(tmp_path.glob(".autoform-new-*")) + assert len(stages) == 1 + assert (stages[0] / "blueprint/KEEP").read_text(encoding="utf-8") == "keep\n" + + +def test_hard_linked_planned_file_is_not_published(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + target = tmp_path / "project" + alias = tmp_path / "alias" + original = create_module._materialize_project + + def add_alias(*args, **kwargs): + original(*args, **kwargs) + stage = next(tmp_path.glob(".autoform-new-*")) + os.link(stage / "lean-toolchain", alias) + + monkeypatch.setattr(create_module, "_materialize_project", add_alias) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-failed" + assert not target.exists() + assert alias.stat().st_nlink == 2 + + +def test_noncanonical_generated_directory_mode_is_not_published( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + target = tmp_path / "project" + original = create_module._materialize_project + + def make_world_writable(*args, **kwargs): + original(*args, **kwargs) + stage = next(tmp_path.glob(".autoform-new-*")) + (stage / "blueprint").chmod(0o777) + + monkeypatch.setattr(create_module, "_materialize_project", make_world_writable) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-failed" + assert not target.exists() + stage = next(tmp_path.glob(".autoform-new-*")) + assert stat.S_IMODE((stage / "blueprint").stat().st_mode) == 0o777 + + +def test_mutation_after_validation_is_not_published(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + target = tmp_path / "project" + original = create_module._validate_staged_project + + def mutate(*args, **kwargs): + original(*args, **kwargs) + stage = next(tmp_path.glob(".autoform-new-*")) + (stage / "lean-toolchain").write_text("mutated\n", encoding="utf-8") + + monkeypatch.setattr(create_module, "_validate_staged_project", mutate) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-create-failed" + assert not target.exists() + + +def test_verifier_opens_regular_files_nonblocking(monkeypatch: pytest.MonkeyPatch) -> None: + captured: dict[str, object] = {} + + def capture(name, flags, *, dir_fd): + captured.update(name=name, flags=flags, dir_fd=dir_fd) + return 17 + + monkeypatch.setattr(create_module.os, "open", capture) + + assert create_module._open_planned_file(9, "lean-toolchain") == 17 + assert captured == { + "name": "lean-toolchain", + "flags": os.O_RDONLY | os.O_NOFOLLOW | os.O_NONBLOCK | getattr(os, "O_CLOEXEC", 0), + "dir_fd": 9, + } + + +def test_concurrent_creation_has_exactly_one_winner(tmp_path: Path) -> None: + target = tmp_path / "project" + barrier = threading.Barrier(2) + results: list[str] = [] + + def run() -> None: + barrier.wait(timeout=10) + try: + create_project(target, package="Project", release_id=_RELEASE) + results.append("created") + except ProjectCreateError as error: + results.append(error.code) + + threads = [threading.Thread(target=run) for _ in range(2)] + for thread in threads: + thread.start() + for thread in threads: + thread.join(timeout=30) + assert all(not thread.is_alive() for thread in threads) + assert sorted(results) == ["created", "project-target-exists"] + assert inspect_project(target).ok + assert not list(tmp_path.glob(".autoform-new-*")) + + +@pytest.mark.parametrize( + "arguments, code", + [ + (["project", "new", "--json"], "project-target-invalid"), + (["project", "new", "project", "--release", _RELEASE, "--json"], "project-name-invalid"), + (["project", "new", "project", "--package", "Project", "--json"], "project-release-unknown"), + ], +) +def test_cli_missing_creation_options_are_json(arguments: list[str], code: str, capsys) -> None: + assert main(arguments) == 1 + captured = capsys.readouterr() + assert json.loads(captured.out)["error"]["code"] == code + assert captured.err == "" + + +def test_cli_json_is_stable_and_path_free(tmp_path: Path, capsys) -> None: + target = tmp_path / "project" + assert ( + main( + [ + "project", + "new", + str(target), + "--package", + "Project", + "--release", + _RELEASE, + "--json", + ] + ) + == 0 + ) + captured = capsys.readouterr() + payload = json.loads(captured.out) + assert payload["ok"] is True + assert payload["target"] == "project" + assert str(tmp_path) not in captured.out + assert captured.err == "" + + duplicate = tmp_path / "project" + assert ( + main( + [ + "project", + "new", + str(duplicate), + "--package", + "Project", + "--release", + _RELEASE, + "--json", + ] + ) + == 1 + ) + failed = capsys.readouterr() + assert json.loads(failed.out)["error"]["code"] == "project-target-exists" + assert failed.err == "" + + +@pytest.mark.skipif(os.name != "posix", reason="project creation is POSIX-only") +def test_cli_postcommit_output_is_ascii_and_backslash_safe(tmp_path: Path) -> None: + target = tmp_path / "cr\N{LATIN SMALL LETTER E WITH ACUTE}ation\\line\nbreak" + environment = { + **os.environ, + "PYTHONIOENCODING": "ascii:strict", + "PYTHONDONTWRITEBYTECODE": "1", + } + completed = subprocess.run( + [ + sys.executable, + "-m", + "autoform_cli", + "project", + "new", + os.fspath(target), + "--package", + "Project", + "--release", + _RELEASE, + ], + cwd=Path(__file__).parents[1], + env=environment, + capture_output=True, + text=True, + encoding="ascii", + check=False, + ) + + assert completed.returncode == 0, completed.stderr + assert "\\xe9" in completed.stdout + assert "\\\\line\\nbreak" in completed.stdout + assert target.is_dir() + + json_target = tmp_path / "d\N{LATIN SMALL LETTER O WITH CIRCUMFLEX}nn\N{LATIN SMALL LETTER E WITH ACUTE}es" + machine = subprocess.run( + [ + sys.executable, + "-m", + "autoform_cli", + "project", + "new", + os.fspath(json_target), + "--package", + "Project", + "--release", + _RELEASE, + "--json", + ], + cwd=Path(__file__).parents[1], + env=environment, + capture_output=True, + text=True, + encoding="ascii", + check=False, + ) + assert machine.returncode == 0, machine.stderr + assert all(ord(character) < 128 for character in machine.stdout) + assert json.loads(machine.stdout)["target"] == json_target.name + + +@pytest.mark.parametrize("name", [os.fsdecode(b"project-\xff"), "project-\ud800"]) +def test_surrogate_target_is_rejected_before_writing(tmp_path: Path, name: str) -> None: + target = os.fspath(tmp_path / name) + + with pytest.raises(ProjectCreateError) as raised: + create_project(target, package="Project", release_id=_RELEASE) + + assert raised.value.code == "project-target-invalid" + assert not list(tmp_path.iterdir()) + + +def test_cli_threads_the_explicit_workflow_pin(tmp_path: Path, capsys) -> None: + target = tmp_path / "Pinned" + source = "https://example.test/owner/autoform.git" + revision = "5" * 40 + + assert ( + main( + [ + "project", + "new", + os.fspath(target), + "--package", + "Pinned", + "--release", + _RELEASE, + "--autoform-source", + source, + "--autoform-ref", + revision, + "--json", + ] + ) + == 0 + ) + + payload = json.loads(capsys.readouterr().out) + assert payload["workflows_pinned"] is True + workflow = (target / ".github/workflows/autoform-verify.yml").read_text(encoding="utf-8") + assert f'AUTOFORM_SOURCE: "{source}"' in workflow + assert f'AUTOFORM_REF: "{revision}"' in workflow diff --git a/tests/test_scaffold.py b/tests/test_scaffold.py index 1c825406..30c29bd2 100644 --- a/tests/test_scaffold.py +++ b/tests/test_scaffold.py @@ -98,6 +98,38 @@ def test_scaffold_writes_the_whole_vault(tmp_path: Path) -> None: assert (tmp_path / relative).is_file(), relative +def test_scaffold_rejects_an_incomplete_template_tree( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + templates = tmp_path / "templates" + shutil.copytree(scaffold_module._TEMPLATES, templates) + (templates / "theme/main.html").unlink() + monkeypatch.setattr(scaffold_module, "_TEMPLATES", templates) + + with pytest.raises(ScaffoldError, match="template tree is incomplete"): + scaffold_project(tmp_path / "project", title="Incomplete") + + +def test_scaffold_rejects_non_utf8_template_text( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + templates = tmp_path / "templates" + shutil.copytree(scaffold_module._TEMPLATES, templates) + (templates / "README.md").write_bytes(b"\xff") + monkeypatch.setattr(scaffold_module, "_TEMPLATES", templates) + + with pytest.raises(ScaffoldError, match="template tree contains invalid text"): + scaffold_project(tmp_path / "project", title="Invalid") + + +def test_init_does_not_create_a_lean_project_shell(tmp_path: Path) -> None: + scaffold_project(tmp_path, title="Finite Flat") + + assert not (tmp_path / "lakefile.toml").exists() + assert not (tmp_path / "lean-toolchain").exists() + assert not (tmp_path / "src/FiniteFlat.lean").exists() + + def test_scaffolded_vault_validates_immediately(tmp_path: Path) -> None: """A fresh project must pass `autoform check` before any mathematics.""" @@ -534,7 +566,12 @@ def test_verified_scaffolding_does_not_read_the_live_template_tree( ) -> None: source = "https://example.test/autoform.git" ref = "1" * 40 - snapshot = (("README.md", b"verified\n", 0o644),) + snapshot = tuple( + (relative, b"verified\n" if relative == "README.md" else content, mode) + for relative, content, mode in scaffold_module._filesystem_template_snapshot( + scaffold_module._TEMPLATES + ) + ) monkeypatch.setattr( scaffold_module, "_verified_template_snapshot", diff --git a/tests/test_skill_examples.py b/tests/test_skill_examples.py index 3b818550..c8306a15 100644 --- a/tests/test_skill_examples.py +++ b/tests/test_skill_examples.py @@ -62,6 +62,11 @@ def test_development_guidance_requires_fail_closed_local_safety(repo_root: Path) assert "private declaration safety as fail-closed evidence" in normalized assert "official user name" in normalized assert "by source coordinates" in normalized + assert "regenerate `production_module_roots`" in normalized + assert "from Lake package configs" in normalized + assert "private creation bundle, catalog identity" in normalized + assert "complete `lake update` manifest" in normalized + assert "direct-Mathlib-only manifest is invalid" in normalized def test_agent_review_treats_skeleton_hashes_as_advisory(repo_root: Path) -> None: @@ -85,6 +90,16 @@ def test_quick_start_keeps_the_cli_agent_facing(repo_root: Path) -> None: assert "uv run autoform" not in quick_start +def test_setup_guidance_uses_the_offline_atomic_project_creator(repo_root: Path) -> None: + setup = (repo_root / "skills" / "setup" / "SKILL.md").read_text(encoding="utf-8") + normalized = " ".join(setup.split()) + + assert "autoform project new " in normalized + assert "never overwrites an existing target" in normalized + assert "without running Git, Lake, Lean, or network operations" in normalized + assert "fails closed" in normalized and "including Windows" in normalized + + def test_setup_asset_is_a_repo_shaped_thesis_vault(repo_root: Path) -> None: example = repo_root / _EXAMPLE blueprint = example / "blueprint"