Repository navigation
Create Lean projects atomically with catalog-backed defaults - #96
Conversation
Add `autoform project new`, which stages a complete Lean project (toolchain, lakefile, the release's bundled lake-manifest.json, a root module, and the `autoform init` scaffold) in a private sibling directory, verifies it, and publishes it with a no-replace rename. It never overwrites an existing target and runs no Lake or network operations. This carries #86's creation fixes over to main without the plugin-provenance dependency. Template modes are normalized, so installs under umask 002 work.
project new now defaults --release to the catalog recommended release. --lean-toolchain, with an optional --mathlib-rev that defaults to the tag of the same name, creates a project for a pair the catalog does not list: it writes no lake-manifest.json and warns that lake update must resolve and lock Mathlib. A pair that matches a catalog release, by tag or commit, still gets the bundled lock. Toolchains below Lean v4.27.0 also warn, since the skeleton probe and the generated CI audit need it. Package names may no longer shadow the Mathlib roots docs, LongestPole, or Wanted, which no creation descriptor lists. Human output prints warnings on stderr; JSON adds a warnings array, and release is null for an unlisted pair.
The docstring said Lake reads manifest versions up to 2.0.0, but Lake and the inspector both reject 2.0.0 and later; they read any 1.x. Test that 2.0.0-rc1 is refused and that 1.3.0, which Lake v4.35 writes, and later 1.x versions are read.
Parent problems now have their own codes. A missing parent or ancestor is project-parent-missing, one that cannot be read or searched is project-parent-inaccessible, and the project-parent-unsafe message names the chmod that fixes a group- or world-writable parent. macOS reports a symbolic link opened with O_NOFOLLOW as ENOTDIR, which is now classified as a link. Waiting for another creator's lock gives up after 30 seconds with project-parent-busy instead of blocking indefinitely. Toolchain version components are limited to nine digits, so an oversized tag is project-version-invalid rather than a slow int() conversion. The unlisted warning says that a catalog pair is recognized by its tag or full commit. On the CLI, missing target and --package errors say what is required, an interrupt exits 130 with project-create-interrupted and mentions the hidden stage it may leave, and the omitted-workflows warning gives the init command that adds them. Only project new escapes its report to ASCII; inspect keeps printable Unicode, as on main.
A parent that can be read but not searched now fails its first lookup as project-parent-inaccessible, and a parent that cannot be written fails stage creation with the same code and a message naming the missing write permission; both were project-create-failed. A regular file swapped into the parent path after validation is reported as project-parent-invalid instead of project-path-is-symlink. macOS reports links and other non-directories alike as ENOTDIR, so the component is examined before it is called a link. An interrupt during create_project's final cleanup can follow a successful publication. When the target did not exist beforehand and does now, the CLI says it may be this run's complete project instead of saying that nothing was published. The omitted-workflows hint keeps an explicit --autoform-source, which init would otherwise replace with this checkout's origin. New tests pin project-parent-missing, the not-a-directory parent, the _open_parent errno routing, and the reworded unsafe-parent and unlisted messages. The missing-option CLI test no longer depends on the mode of the working directory.
meta-cla
Bot
added
the
CLA Signed
…0261005 # Conflicts: # autoform_cli/README.md # autoform_cli/project/inspect.py # tests/test_project_inspect.py
…0261005 # Conflicts: # tests/test_scaffold.py
Deicyde
changed the title
|
Exact-head adversarial review is complete at |
…0261005 # Conflicts: # README.md
|
Exact-head review is refreshed at Across the exact-head runs, Python 3.10, Python 3.13, Windows, real Lean project creation/build, and CLA each have a successful check. The duplicate jobs shown as cancelled were runner shutdowns before steps; the dedicated real-Lean rerun completed successfully. No known code blocker remains, and #137 becomes redundant when this lands. |
|
Merge conflicts are resolved and published at exact head Focused skill tests pass (23), Ruff and diff checks are clean, and the executable example passes. The broad local integration run passed 601 tests; its two failures were host-load timeouts (a real-Lake build and the 15-second daemon startup check). The wheel/daemon check passes with a longer diagnostic startup budget, and the committed 15-second contract is unchanged. GitHub's isolated exact-head Python, Windows, and real-Lean runs are now in progress; the PR is mergeable with no unresolved files. |
|
Final exact-head gate at |
Conflicts: - README.md: keep main's Lean v4.27.0 floor and this branch's Intel Mac sentence. - skills/setup/SKILL.md: keep this branch's MathJax paragraph and main's longer paragraph on how init pins CI. - autoform_cli/__main__.py, audit.py, render.py and their tests: take the union of the imports. render_site turns a source-index OSError into a PublicationError, as main does. - autoform_cli/lean.py and tests/test_lean_sources.py: main's snapshot model (#95) plus this branch's `#exit` handling, review-packet output schema, output-stage exclusion and `elsewhere` declarations, with their tests. - autoform_cli/skeleton.py: main's labelled run_probe (#136), which the impact probe shares, plus this branch's compiled helper module. The helper is built only when the probe imports it, so the impact probe skips it, and the label reaches the lake-manifest and shadowed-module messages. extract_skeletons reports an unreadable source tree with index_failure_message, as main's other commands do. Semantic: - tests/test_impact.py: the impact probe now names declarations with fully qualified `Lean.Name.str` terms, through this branch's `_lean_name`. - autoform_cli/scaffold.py: the required template paths drop blueprint/javascripts/mathjax.js, which this branch deleted, and add the review marker and the review-gate workflow. - tests/test_skeleton.py: drop the test that a tagged-process scan skips a process it cannot read, which main's #118 process scan contradicts. - tests/test_scaffold.py: this branch's workflow tests pass an explicit autoform_ref, as main's do. Since #96, plugin_pin finds no pin for a commit that no remote-tracking ref contains, and on such a commit init omits the workflows these tests read.
1 participant
Supersedes #86 and the closed #26.
Summary
autoform project new <TARGET> --package <Name>for a complete Lean + Autoform repository: Lean shell, exact catalog lock, blueprint vault, site configuration, ignore rules, and optionally pinned CIlake updateand are reported explicitlyautoform-project-creation/v1JSON and make Setup use the copied plugin throughuv run --project, with no secondinitafterproject newinitsafely append missing Autoform ignore rules to an existing single-link regular.gitignoreSafety and reproducibility
/tmp(use/private/tmp).gitignorerules through the retained descriptor so a concurrent replacement is never overwritten; hard links are refused and partial appends are reported for inspectionValidation
make check-examplepass