acorn-prover

# Acorn Prover ## Setup (MUST DO WHEN RUNNING FIRST TIME) If `config.env` does not exist in the skill directory: 1. **Ask the user** for the following paths: - `ACORN_LIB` - Path to acornlib (e.g., `/path/to/acornprover/acornlib`) - `ACORN_PROJECT` - Path to project directory for `.ac` files (e.g., `/path/to/acorn-playground`) 2. **Verify** the paths exist using `list_dir` or equivalent. If a path is invalid, inform the user and ask again. 3. **Run setup.sh** with the validated paths: ```bash bash skills/acorn-prover/scripts/setup.sh "<ACORN_LIB>" "<ACORN_PROJECT>" ``` 4. **Source the config** to get `ACORN_LIB`, `ACORN_PROJECT`, and `USE_MISE` variables: ```bash source skills/acorn-prover/config.env ``` If any of the above are blank / not set, inform the user to set the variable manually. If any of the above are changed, ask the user for new paths and run setup again. ## Configuration Config values are stored in `skills/acorn-prover/config.env`: | Variable | Description | | --------------- | ------------------------------- | | `ACORN_LIB` | Path to acornlib | | `ACORN_PROJECT` | Project directory for .ac files | | `USE_MISE` | `true` if mise is available | ## Verify Proofs If `USE_MISE=true`: ```bash mise run acorn verify <filename>.ac ``` Otherwise, use the direct CLI: ```bash acorn --lib "$ACORN_LIB" verify <filename>.ac ``` ## Reverify Proofs (CI/CD) Check that all proofs are cached with no AI searches required: ```bash # With mise mise run acorn reverify # Or direct CLI acorn --lib "$ACORN_LIB" reverify ``` Use for CI pipelines to ensure all proofs are complete. ## Training Data Generation Generate training data (problem-proof pairs) for AI model development: ```bash # With mise mise run acorn training ./training_data # Or direct CLI acorn --lib "$ACORN_LIB" training ./training_data ``` Argument: `DIR` - Directory to output training data. ## Documentation Generation Generate library reference documentation: ```bash # With mise mise run acorn docs ./docs/library # Or direct CLI acorn --lib "$ACORN_LIB" docs ./docs/library ``` Argument: `DIR` - Directory to output documentation. ## Workflow 1. Source config: `source skills/acorn-prover/config.env` 2. Write proof file in `$ACORN_PROJECT/` 3. Run the appropriate command (verify, reverify, training, docs) 4. **Always show the full command output to the user** (success or error) 5. Debug errors using the common errors table in [references/syntax.md](references/syntax.md) 6. Iterate until verification passes ## Quick Syntax Overview ```acorn from nat import Nat from add_comm_group import AddCommGroup // Theorems - auto-proved or with hints theorem example(a: Nat, b: Nat) { a < b implies a != b } // Typeclasses - axioms are named blocks, no "axiom" keyword typeclass A: AddGroup extends Zero, Neg, Add { inverse_right(a: A) { a + -a = A.0 } } // Structures structure Pair[T, U] { first: T second: U } // Inductive types - constructors MUST be lowercase inductive MyBool { tru fls } ``` Key points: - Built-in logic keywords (`not`, `and`, `or`, `implies`, `iff`, `true`, `false`) are reserved - do not redefine - Constructor names must be lowercase - Typeclass axioms use named blocks, not the `axiom` keyword ## Standard Library (`acornlib`) Key modules in `$ACORN_LIB/src`: | Module | Contents | | ------------------- | ------------------------------------------ | | `nat/` | Natural number axioms, induction, addition | | `add_group.ac` | `AddGroup` with `a + -a = A.0` | | `add_comm_group.ac` | Abelian groups (`AddCommGroup`) | ## References - **Full syntax, error table, examples**: See [references/syntax.md](references/syntax.md) - **Context7 docs**: Use `context7` MCP with `/acornprover/acorn` or `/acornprover/acornlib` for latest documentation