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:
CODEBLOCK0
- 4. Source the config to get
ACORN_LIB, ACORN_PROJECT, and USE_MISE variables:
CODEBLOCK1
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 |
|---|
| INLINECODE11 | Path to acornlib |
| INLINECODE12 |
Project directory for .ac files |
|
USE_MISE |
true if mise is available |
Verify Proofs
If USE_MISE=true:
CODEBLOCK2
Otherwise, use the direct CLI:
CODEBLOCK3
Reverify Proofs (CI/CD)
Check that all proofs are cached with no AI searches required:
CODEBLOCK4
Use for CI pipelines to ensure all proofs are complete.
Training Data Generation
Generate training data (problem-proof pairs) for AI model development:
CODEBLOCK5
Argument: DIR - Directory to output training data.
Documentation Generation
Generate library reference documentation:
CODEBLOCK6
Argument: DIR - Directory to output documentation.
Workflow
- 1. Source config: INLINECODE18
- Write proof file in INLINECODE19
- 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
CODEBLOCK7
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 |
|---|
| INLINECODE30 | Natural number axioms, induction, addition |
| INLINECODE31 |
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
Acorn Prover
设置（首次运行时必须执行）
如果技能目录中不存在 config.env：
- 1. 询问用户以下路径：
- ACORN_LIB - acornlib 的路径（例如 /path/to/acornprover/acornlib）
- ACORN_PROJECT - 存放 .ac 文件的项目目录路径（例如 /path/to/acorn-playground）
- 2. 验证路径是否存在（使用 list_dir 或等效方法）。如果路径无效，告知用户并重新询问。
- 3. 运行 setup.sh，传入验证后的路径：
bash
bash skills/acorn-prover/scripts/setup.sh LIB> PROJECT>
- 4. 加载配置以获取 ACORNLIB、ACORNPROJECT 和 USE_MISE 变量：
bash
source skills/acorn-prover/config.env
如果上述任一变量为空/未设置，告知用户手动设置该变量。
如果上述任一变量发生更改，询问用户新的路径并重新运行 setup。
配置
配置值存储在 skills/acorn-prover/config.env 中：
| 变量 | 描述 |
|---|
| ACORNLIB | acornlib 的路径 |
| ACORNPROJECT |
存放 .ac 文件的项目目录 |
| USE_MISE | 如果 mise 可用则为 true |
验证证明
如果 USE_MISE=true：
bash
mise run acorn verify .ac
否则，使用直接 CLI：
bash
acorn --lib $ACORN_LIB verify .ac
重新验证证明（CI/CD）
检查所有证明是否已缓存且无需 AI 搜索：
bash
使用 mise
mise run acorn reverify
或直接 CLI
acorn --lib $ACORN_LIB reverify
用于 CI 流水线以确保所有证明完整。
训练数据生成
为 AI 模型开发生成训练数据（问题-证明对）：
bash
使用 mise
mise run acorn training ./training_data
或直接 CLI
acorn --lib $ACORN
LIB training ./trainingdata
参数：DIR - 输出训练数据的目录。
文档生成
生成库参考文档：
bash
使用 mise
mise run acorn docs ./docs/library
或直接 CLI
acorn --lib $ACORN_LIB docs ./docs/library
参数：DIR - 输出文档的目录。
工作流程
- 1. 加载配置：source skills/acorn-prover/config.env
- 在 $ACORNPROJECT/ 中编写证明文件
- 运行相应命令（verify、reverify、training、docs）
- 始终向用户显示完整的命令输出（成功或错误）
- 使用 references/syntax.md 中的常见错误表调试错误
- 迭代直至验证通过
快速语法概览
acorn
from nat import Nat
from addcommgroup import AddCommGroup
// 定理 - 自动证明或带提示
theorem example(a: Nat, b: Nat) {
a < b implies a != b
}
// 类型类 - 公理是命名块，没有 axiom 关键字
typeclass A: AddGroup extends Zero, Neg, Add {
inverse_right(a: A) { a + -a = A.0 }
}
// 结构体
structure Pair[T, U] { first: T second: U }
// 归纳类型 - 构造器必须小写
inductive MyBool { tru fls }
关键点：
- - 内置逻辑关键字（not、and、or、implies、iff、true、false）为保留字 - 请勿重定义
- 构造器名称必须小写
- 类型类公理使用命名块，而非 axiom 关键字
标准库（acornlib）
$ACORN_LIB/src 中的关键模块：
| 模块 | 内容 |
|---|
| nat/ | 自然数公理、归纳法、加法 |
| add_group.ac |
AddGroup，包含 a + -a = A.0 |
| add
commgroup.ac | 阿贝尔群（AddCommGroup） |
参考
- - 完整语法、错误表、示例：参见 references/syntax.md
- Context7 文档：使用 context7 MCP，路径为 /acornprover/acorn 或 /acornprover/acornlib 以获取最新文档
