如何从外部软件调用证明助手Coq

Question

如何从外部软件调用打样助手Coq？ Coq 有一些 API 吗？ Coq 命令行接口是否足够丰富以在文件中传递参数并在文件中接收响应？我对 Java 或 C++ 桥感兴趣。

这是一个合理的问题。 Coq 不是通常的商业软件，人们可以期待它对开发人员友好 API。我有关于 Isabelle/HOL 的类似问题，这是一个具有重要答案的合法问题。

Answer 1

命令行似乎是可行的方法。

Coq 包括几个命令行工具，包括 coqc 编译器。该程序将 Coq 理论文件作为输入并尝试对其进行编译。如果理论有问题，命令将失败并返回非零退出代码并将一些反馈写入其输出流。如果一切正常，该命令（通常）是静默的，以零退出代码退出，并写入包含已编译理论的 .vo 文件。

例如：

$ 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

以下是 Coq 命令行工具的文档，可以使用各种标志： https://coq.inria.fr/refman/practical-tools/coq-commands.html

我知道有两个工具使用 Coq 作为从属证明引擎：Frama-C 和 Why3。查看 https://github.com/Frama-C/Frama-C-snapshot/blob/master/src/plugins/wp/ProverCoq.ml (methods compile and check) and at https://github.com/AdaCore/why3/tree/master/drivers 上的源代码，这些工具似乎也将 Coq 理论转储到文件中，然后调用 Coq 的命令行工具。据我所知，Coq 没有更直接的 API。

Answer 2

截至今天，共有三种与 Coq 交互的方式，从多到少排序：

OCaml API：这就是 Coq 插件所做的，然而，OCaml API 的某些部分是出了名的难以掌握，通常需要很高的专业知识。 API 也会从一个版本更改为另一个版本，这使得维护变得困难。 OCaml API 除了查看源代码外，没有官方文档，但是有很多维护程度不同的教程。
XML 协议：这是 IDE 使用的协议。它允许客户端执行基本的 Coq 文档操作，例如检查它的一部分、有限搜索、检索目标等...official documentation
命令行：作为其他答案的详细信息，这基本上允许检查一个文件是否可以被 Coq 完全编译。

或者，有一个名为 "SerAPI" [免责声明我是作者] 的实验协议位于 1 和 2 之间。SerAPI 是 XML 协议的扩展（但使用 SEXP）试图提供 1 的一些优点以及更丰富的查询操作，而没有与 OCaml 链接的缺点。

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

一些附加链接：

如何从外部软件调用证明助手Coq

How to call proof asistant Coq from external software

coq