如何从外部软件呼叫proof asistant Coq

Question

如何从外部软件呼叫证明助手Coq？ Coq是否有一些API？ Coq命令行界面是否足够丰富，可以在文件中传递参数并在文件中接收响应？我对Java或C++桥梁感兴趣。

这是一个合法的问题。 Coq不是通常的商业软件，人们可以期望开发者友好的API。对于Isabelle/HOL我有类似的问题，这是一个非常重要的问题。

Answer 1

截至今天，有三种方式与勒柯克，从更多的努力责令较少的电力进行交互：

1. 使用OCaml的API：这是什么勒柯克插件做的，但是，有些部位众所周知，OCaml API难以掌握，通常需要很高的专业知识。 API也从一个版本变为另一个版本，这使得维护变得困难。除了查看源代码外，OCaml API还没有官方文档，但有不少程度不同的维护教程正在浮动。

2. 使用XML协议：这是IDE使用的。它允许客户端执行基本的Coq文档操作，例如检查它的一部分，限制搜索，检索目标等等。official documentation

3. 使用命令行：作为其他答案的细节，这基本上允许检查是否可以由Coq完全编译文件。

可选择地，有一个被称为“SerAPI” [声明我提交]为处于1个2之间SerAPI是XML协议的扩展（但使用SEXPs）实验方案，试图提供一些1的优点以及更丰富的查询操作，没有与OCaml链接的缺点。

SerAPI目前处于非常实验阶段，但它可能对某些用户有用。webpage

一些额外的链接：

• https://andy-morris.xyz/blog/20161001-coq-protocol.html
• https://github.com/mattam82/Constructors
• http://gallium.inria.fr/blog/your-first-coq-plugin/
• https://github.com/uwplse/CoqAST

Answer 2

命令行似乎是要走的路。

Coq包含几个命令行工具，包括coqc编译器。这个程序将一个Coq理论文件作为输入并尝试编译它。如果理论出了问题，命令会失败，并返回一个非零的退出代码，并在输出流中写入一些反馈。如果一切正常，该命令（通常）是无声的，以零退出代码退出，并写入一个包含编译理论的文件。

例如：

$ cat bad.v 
Lemma zero_less_than_one: 0 < 1. 
$ coqc bad.v ; echo $? 
Error: There are pending proofs 
1 
$ cat good.v 
Lemma zero_less_than_one: 0 < 1. 
Proof. 
    auto. 
Qed. 
$ coqc good.v ; echo $? 
0 

这里是勒柯克的命令行工具的文档，可以采取各种标志：https://coq.inria.fr/distrib/current/refman/Reference-Manual016.html

我知道使用勒柯克为下级证明发动机两种工具： Frama-C和Why3。查看https://github.com/Frama-C/Frama-C-snapshot/blob/master/src/plugins/wp/ProverCoq.ml（方法compile和check）和https://github.com/AdaCore/why3/tree/master/drivers的源代码，这些工具似乎也将Coq理论转储到文件中，然后调用Coq的命令行工具。据我所知，Coq没有更直接的API。