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
标签
skill
ai
