Acorn Prover
Setup (MUST DO WHEN RUNNING FIRST TIME)
If config.env does not exist in the skill directory:
-
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)
-
Verify the paths exist using list_dir or equivalent. If a path is invalid, inform the user and ask again.
-
Run setup.sh with the validated paths:
bash skills/acorn-prover/scripts/setup.sh "<ACORN_LIB>" "<ACORN_PROJECT>"
- Source the config to get
ACORN_LIB, ACORN_PROJECT, and USE_MISE variables:
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:
mise run acorn verify <filename>.ac
Otherwise, use the direct CLI:
acorn --lib "$ACORN_LIB" verify <filename>.ac
Reverify Proofs (CI/CD)
Check that all proofs are cached with no AI searches required:
# 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:
# 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:
# 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
- Source config:
source skills/acorn-prover/config.env
- Write proof file in
$ACORN_PROJECT/
- Run the appropriate command (verify, reverify, training, docs)
- Always show the full command output to the user (success or error)
- Debug errors using the common errors table in references/syntax.md
- Iterate until verification passes
Quick Syntax Overview
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
- Context7 docs: Use
context7 MCP with /acornprover/acorn or /acornprover/acornlib for latest documentation
