diff --git a/README.md b/README.md index 09e586b6..3f36a27a 100644 --- a/README.md +++ b/README.md @@ -1,141 +1,71 @@ # AutoformBot -AutoformBot is a coding-agent plugin and Python CLI for Lean 4 formalization -projects. It builds source-grounded Markdown roadmaps, validates dependencies, -publishes progress views, and prepares human or agent review. The plugin and -CLI use the identifier `autoform`; the canonical repository is -[`facebookresearch/autoform-bot`](https://github.com/facebookresearch/autoform-bot). +A plugin for Claude Code and Codex that helps turn mathematical papers and +notes into Lean 4 formalizations: plan the work, write proofs, and review +progress from your coding assistant. -The `main` branch provides repository setup, roadmap planning, Markdown-native -formalization of ready roadmap leaves, publication, human and agent review, and -shared Lean LSP/REPL tools. The historical -`execution` branch and its custom worker/prover stack are deprecated and are -not an installation target. +Install from `main`. The historical +`execution` branch and its custom worker/prover stack are deprecated. -## Prerequisites +## Installation -- Python 3.10 or newer and [`uv`](https://docs.astral.sh/uv/) -- Git -- Lean and Lake for Lean tooling and verification -- Claude Code or Codex for the installation flows below +Requires Python 3.10+, [`uv`](https://docs.astral.sh/uv/), Git, and Lean 4 +with Lake. -## Install - -Claude Code: +**Claude Code** ```bash claude plugin marketplace add facebookresearch/autoform-bot claude plugin install autoform@autoform ``` -Codex: +**Codex** ```bash codex plugin marketplace add facebookresearch/autoform-bot --ref main codex plugin add autoform@autoform ``` -Start a new agent session so the skills and MCP servers reload. A native Muse -manifest is included, but Muse installation is not covered here. +After installing, start a new session in the repository you want to inspect or +set up. ## Quick start -Work from an existing Lean repository and use the host skills from its agent -window. The skills invoke Autoform's CLI themselves; users do not need to learn -or run its commands. +Use these skills from your agent window; users do not need to learn or run its +commands: | Task | Claude Code | Codex | | --- | --- | --- | -| Set up the blueprint and publication files | `/autoform:setup` | `$setup` | -| Build a source-grounded roadmap | `/autoform:roadmap` | `$roadmap` | -| Formalize ready roadmap leaves | `/autoform:formalize` | `$formalize` | -| Prepare a person-led review | `/autoform:human-review` | `$human-review` | -| Run an independent agent review | `/autoform:agent-review` | `$agent-review` | - -For example: “Build a complete roadmap for Sections 2–4 of `paper.pdf`.” Keep -the source in the repository or provide an accessible path. Roadmap treats -coarse planning as an internal checkpoint unless staged review was requested; -when possible, the skill uses a compatible model-callable Goal itself. Human -and agent review remain available before execution. - -## Blueprint model - -```text -blueprint/ -├── README.md -├── coverage/README.md -├── roadmap/ -│ ├── README.md -│ └── convexity/ -│ ├── README.md -│ ├── convex.md -│ └── separating-hyperplane.md -└── sources/paper.md -``` - -Every Markdown file below `blueprint/roadmap/` is an article. A nested -`README.md` represents its directory and contains the articles below it. -Optional `declaration: theorem`, `declaration: def`, and similar frontmatter -marks a formalizable article. Inline relative links under `## Depends on` and -`## Proof depends on` define dependency edges; reference-style links do not. +| Set up the project | `/autoform:setup` | `$autoform:setup` | +| Plan from a paper or notes | `/autoform:roadmap` | `$autoform:roadmap` | +| Write Lean definitions and proofs | `/autoform:formalize` | `$autoform:formalize` | +| Review the roadmap and progress | `/autoform:human-review` | `$autoform:human-review` | +| Request an independent AI review | `/autoform:agent-review` | `$autoform:agent-review` | -Markdown is the source of truth; Mermaid graphs and MkDocs pages are derived -views. See the [blueprint format and CLI reference](autoform_cli/README.md) for -complete frontmatter, hierarchy, status, and validation rules. +Start with `setup`, then use `roadmap` to plan your formalization and +`formalize` to work through it. Use either review command to inspect the plan +or the resulting formalization. -## Agent-facing CLI and publication +For example, invoke `roadmap` and ask: -Skills use these commands to make and verify changes. They are documented for -plugin development and debugging, not as a required user workflow. +> Build a complete roadmap for Sections 2–4 of `paper.pdf`. -| Command | Purpose | -| --- | --- | -| `autoform init` | Scaffold the blueprint and site; add CI when immutably pinned. | -| `autoform check` | Validate Markdown structure and dependencies. | -| `autoform audit` | Audit completeness and checked facts. | -| `autoform doctor` | Diagnose the local blueprint contract. | -| `autoform skeleton` | Extract what a reader must trust for each formalized statement. | -| `autoform work` | Inspect the Markdown-derived formalization frontier and node context. | -| `autoform claim` | Coordinate temporary ownership through Git refs. | -| `autoform dashboard` | Serve the built publication locally with live claim badges. | -| `autoform render` | Generate publishable MkDocs source. | -| `autoform-visualize` | Generate the Mermaid dependency graph. | +Keep the source file in your project or provide an accessible path. -Inside an Autoform checkout, use `uv run`: +Setup changes local files by default. Creating or pushing a remote repository, +enabling GitHub Pages, and publishing blueprint content require an explicit +request; content published through Pages is public. -```bash -uv run autoform check /path/to/project/blueprint --lean-root /path/to/project -uv run autoform-visualize /path/to/project/blueprint -uv run autoform render /path/to/project/blueprint \ - --output /path/to/project/site-src \ - --lean-root /path/to/project --require-declarations -uv run autoform dashboard /path/to/project --site-dir site -``` - -From a consumer project, resolve the installed plugin root and prefix commands -with `uv run --project ""`, or separately install the -Python package so its console scripts are on `PATH`. - -`check --lean-root` lexically resolves names in local Lean files; it does not -compile them or prove that they belong to a Lake target. Use `lake build` and -the verification workflow for compilation and audit, while treating the -blueprint-to-declaration match as a separate contract. - -`render` writes MkDocs source, not a deployed site. The generated Pages workflow -deploys from `main` only after GitHub Pages is enabled in repository settings. -`dashboard` serves that same built site on loopback and overlays current Git-ref -claims. It never publishes worker information or creates another graph. - -## Documentation +## Blueprint model -- [Cabannes thesis example](skills/setup/assets/cabannes-thesis-project/README.md) -- [Roadmap example](skills/roadmap/references/cabannes-thesis-roadmap.md) -- [Lean server architecture and operations](servers/README.md) +Autoform keeps the roadmap and dependency graph as Markdown under +`blueprint/`; publication graphs and pages are derived. See the +[blueprint format and CLI reference](autoform_cli/README.md) for the complete +format and command contracts, or browse the +[Cabannes thesis example](skills/setup/assets/cabannes-thesis-project/README.md). ## Development -Development also requires Make: - ```bash git clone https://github.com/facebookresearch/autoform-bot.git cd autoform-bot @@ -145,9 +75,9 @@ make test make check-example ``` -Claude Code uses `/autoform:develop-plugin`; Codex uses `$develop-plugin`. -`make check-example` validates, renders, and builds the example documentation. -Run `lake build` in the Cabannes fixture when changing its Lean sources or -declarations. +Lean server architecture and operations are documented in +[`servers/README.md`](servers/README.md). + +## License -AutoformBot is released under the [MIT License](LICENSE). +[MIT](LICENSE).