5 个版本 (3 个重大更新)
| 0.4.0 | 2022年6月9日 |
|---|---|
| 0.3.0 | 2021年9月2日 |
| 0.2.0 | 2021年7月19日 |
| 0.1.1 | 2021年3月11日 |
| 0.1.0 | 2020年8月14日 |
#334 在 并发 中排名
每月 25 次下载
在 kocheck 中使用
105KB
2.5K SLoC
Kontroli
Kontroli (世界语中的“验证”）是 Dedukti 逻辑框架的另一种实现，专注于验证证明。
Kontroli 的用例是验证由自动推理工具（如证明辅助工具和自动定理证明器）生成的证明。它通过提供“第二意见”来验证 Dedukti 的输出，并使用户更容易理解和从实现中学习。它也是一个并行化类型检查的测试平台。
用法
Kontroli 至少需要 Rust 1.56。安装说明可在 https://rustup.rs/ 查找。
在 Isabelle/Pure 生成的输出上运行 Kontroli
cargo run --release examples/pure.dk
命令行选项 -j 启用并发检查，- 启用并发解析。
安装 Kontroli
cargo install --path kocheck
Kontroli 提供了一个命令行程序 kocheck 和一个库。这意味着您可以将 Kontroli 用作您自己应用程序的一部分。鉴于 Kontroli 库不依赖于 Rust 的标准库，您还可以在网页等环境中使用它，提供类型检查作为一项服务。
目标
Kontroli 力求成为以下内容
- 小型：尽可能少写代码...
- 正确：...因为您没有写的代码不包含错误
- 高效：在主要用例中至少与 Dedukti 一样快
- 兼容：尽可能坚持 Dedukti 的语法/语义
- 保守：使用经过验证和良好测试的技术
差异
与 Dedukti 有一些不同之处
- Kontroli 有一个模块系统，允许嵌套模块。
- Kontroli 不支持高阶重写规则，因为这会使整个程序变得更加复杂，这与小型类型检查器的理念相矛盾。
- 如果所有自由模式变量都有类型注解，Kontroli 才能保证重写规则的类型安全性。
- Kontroli 不使用决策树进行重写。
- Kontroli 没有任何类似于
#EVAL或#ASSERT的命令，这些命令在 Dedukti 测试中特别常用。相反，更倾向于使用代码库中的测试。
语法
Kontroli 实现了 Dedukti 语法的一个子集。语法示例可以在 examples/nat.dk 或 examples/pure.dk 中查看。
开发
一些对开发 Kontroli 有用的命令
- 生成文档：
cargo doc --open - 运行测试：
cargo test - 运行基准测试：
cargo bench -p kontroli -- --sample-size 10
依赖项
约 2.5MB
约 27K SLoC