--- name: setup description: >- Set up, inspect, or repair repository infrastructure for an Autoform Lean project, including the Lean/Mathlib shell, an in-repository Obsidian-compatible blueprint vault, ignore rules, MkDocs, GitHub Pages, and verification CI, with optional Zulip community synchronization. Use for new repositories, environment repair, publication setup, infrastructure checks, or an explicitly requested Zulip project sync; do not choose mathematical scope or build the roadmap and theorem DAG. --- # Set up an Autoform repository Setup prepares the Lean toolchain, an empty blueprint vault, ignore rules, MkDocs, CI, and optionally publication. It does not scope sources, choose theorems, write roadmap nodes, or prove results; Roadmap owns that work. Inspect before writing and preserve existing Lean, Markdown, workflow, and ignore files. Resolve `AUTOFORM_PLUGIN_ROOT` from the loaded plugin and inspect an existing project through the supported read-only entrypoint: ```bash AUTOFORM_PLUGIN_ROOT="" PROJECT="" uv run --project "$AUTOFORM_PLUGIN_ROOT" autoform project inspect "$PROJECT" --json ``` Infer safe local defaults from the request and repository. If a material choice is missing, ask once for the run type (new, repair, or inspect), UpperCamelCase package name, target directory, and whether publication is wanted. Without explicit publication approval, make no remote changes. Setup prepares the shell and stops before mathematical planning. Read the repo-shaped [Cabannes thesis project](assets/cabannes-thesis-project/README.md) as a concrete setup example. Reuse its structure selectively: rename the Lean package, keep the recommended release from `autoform project versions` unless the user needs another Lean version, 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, require a target directory that does not already exist, then create the complete local project atomically: ```bash AUTOFORM_PLUGIN_ROOT="" TARGET="" PACKAGE="" uv run --project "$AUTOFORM_PLUGIN_ROOT" autoform project new "$TARGET" --package "$PACKAGE" ``` Without version flags `project new` uses the recommended release from `autoform project versions`: a tested Lean/Mathlib pair whose resolved `lake-manifest.json` is bundled. Pass `--release ` for another listed pair. If the user needs a different Lean version, pass `--lean-toolchain `; `--mathlib-rev ` overrides the default Mathlib tag of the same name, and the toolchain must match the `lean-toolchain` of that Mathlib revision. Such a project is created without `lake-manifest.json` and with a warning: run `lake update` in it, which needs network access and downloads the Mathlib build cache, then commit the manifest it writes. Autoform needs Lean v4.27.0 or newer, and `project new` also warns below that. Every component of the target parent must be a real directory, not a symlink; on macOS use `/private/tmp`, not the `/tmp` alias. The parent must not be group- or world-writable unless it is a sticky directory owned by the user or root. If `project new` reports `project-parent-unsafe`, choose another parent or, with the user's agreement, remove that write access with `chmod g-w,o-w`. `project new` writes the requested `lean-toolchain` and Mathlib revision (by default the recommended, locked catalog pair), the Lean shell, and the complete Autoform vault, site, ignore rules, and pinnable CI without running Lake, Lean, or network operations; no later `init` is needed. It never overwrites an existing target and fails closed on platforms without the required POSIX filesystem operations, including Windows. It pins generated workflows exactly as `init` does, described below, and omits them when there is no commit to pin; invoke `init` later through the same plugin-root launcher, passing the target and `--autoform-ref <40-char-sha>`. Do not invent workflow sources or revisions, and do not copy the populated example as a project generator. For an incomplete existing repository, preserve its authored configuration and run `autoform init` through the same `uv run --project "$AUTOFORM_PLUGIN_ROOT"` prefix only for the Autoform vault/site repair overlay. `autoform init` is the whole vault: `blueprint/` with its landing page, `roadmap/README.md`, `coverage/`, and `sources/`, plus `mkdocs.yml`, the theme override, both workflows, and ignore rules. Do not hand-build any of it and do not copy the bundled example: the layout is fixed, and a chapter written as a sibling file instead of `/README.md` still validates while publishing a book with no chapters. `init` preserves existing files, appending only missing Autoform rules through a retained bounded regular root `.gitignore` file, so it is also the repair path; it reports what it left alone. See the [CLI reference](../../autoform_cli/README.md#commands) for its flags. `init` pins the generated workflows to the Autoform commit that ran it, using a safe remote only when a cached remote-tracking ref contains that commit. It prefers Autoform's canonical repository, then `origin`, then `upstream`, then a unique remaining source from the Autoform checkout it runs from or the marketplace checkout an installed plugin was copied from. It infers that pin only when tracked files are clean and the retained bounded, regular, link-free required template snapshot and scaffold renderer match the pinned commit in path, bytes, and executable-bit classification; an installed copy must also match its marketplace checkout. All identity and tree reads ignore local Git replacement objects. On any mismatch or when no remote has that local containment evidence, `init` writes no CI rather than guess a source or ref: guessing produced projects whose first push failed with nothing in the workflow to explain why. When it reports that, find the commit the plugin was installed from and pass `--autoform-ref <40-char-sha>`, or say plainly that CI was not configured. Never invent a ref. It must be a full 40-character commit sha: `init` refuses a branch, a tag, or an abbreviated sha, because CI would silently reinstall a different Autoform later and break a project that was passing. The two workflows it writes are `autoform-verify.yml`, which validates the Markdown DAG, builds Lean, rejects unfinished or unsafe proofs, and audits theorem axioms on pull requests, and `blueprint-pages.yml`, which validates the DAG and its `lean:` declarations, renders the blueprint, builds MkDocs, and deploys GitHub Pages. Pass `--autoform-ref` to pin them at an immutable commit. It also writes `.github/CODEOWNERS.autoform.example`. GitHub does not read it, so it cannot mask active owners. Do not guess owners or activate it silently. With names the user gives, merge its rules into the first CODEOWNERS file GitHub reads, then require code-owner review, dismiss stale approvals, and audit bypasses. Report that new rules cannot protect their own activation unless equivalent coverage already exists on the pull request's base branch. After it runs, fill in what only a human or a source can supply: the project description in `blueprint/README.md`, the coverage contract, and a verified `repo_url`. That URL is the *formalization project's own* repository, never AutoformBot's: Material renders it as the repository link in the site header, and pointing it at the plugin sends every reader to the wrong project. Pass `--repository-url` to `autoform init`, or leave the key out until the remote exists rather than guessing it. When a deployed site exists, feature its verified canonical URL in the root `README.md`, never an inferred or pending one. Adding workflow files is a local repository edit. Creating a remote, pushing, or enabling Pages are separate outward-facing actions; perform them only when the user requests them. Pin third-party Actions and the Autoform CLI source to immutable commits. Validate the prepared repository before reporting it ready. Build Lean first, then run the publication sequence: ```bash lake update # only when the project has no lake-manifest.json lake exe cache get # skip only when the project has no Mathlib dependency lake build ``` Then validate, visualize, render, and strict-build the site, keeping `--require-declarations` so a named Lean declaration that does not exist fails here rather than in CI. The exact invocations, including how to resolve ``, are in the [CLI reference](../../autoform_cli/README.md#commands); do not restate them here. `render` writes a derived tree; the vault stays the source of truth. Ignore `site-src/`, `site/`, and `blueprint/dependencies.md`. Publication is opt-in because files under `blueprint/` become public site content, together with derived progress, graph pages, and a path-free publication manifest. Show that boundary, confirm the exact repository and visibility, default to private, and warn that private Pages may require a paid GitHub plan. Rendering rejects symlinks and operational or sensitive files. When approved, prepare the commit, remote, Pages source, and push; otherwise leave the workflow inert. If credentials, hosting, or repository settings block publication, report the minimal owner action required. Zulip synchronization is a separate opt-in outward-facing action. When the user asks to discover community context or announce and coordinate the project, read and follow [the shared Zulip workflow](references/zulip.md). Do not infer consent to post from repository setup, roadmap work, or permission to search. Report the Lean toolchain, vault path, CI and Pages files, validation results, the publication decision, and any one-time GitHub setting the user must still apply. State explicitly that no sources were scoped, roadmap nodes created, or proofs started, then hand the repository to Roadmap.