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

Question

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

这是一个合理的问题。 Coq 不是通常的商业软件，人们可以从中获得对开发人员友好的 API。我对 Isabelle/HOL 有类似的问题，这是一个合理的问题，答案很重要。

Answer 1

到今天为止，可以通过三种方式与 Coq 交互，按照从多到少的顺序排列:

OCaml API:这是 Coq 插件所做的，然而，众所周知，OCaml API 的某些部分很难掌握，通常需要高超的专业知识。 API 还会从一个版本更改为另一个版本，从而使维护变得困难。除了查看源代码之外，OCaml API 没有官方文档，但是有很多不同程度的维护教程在流传。

XML 协议(protocol):这是 IDE 使用的。它允许客户端执行基本的 Coq 文档操作，例如检查其中的一部分、有限搜索、检索目标等... official documentation

命令行:作为其他答案的详细信息，这基本上允许检查文件是否可以被 Coq 完全编译。

或者，有一个名为“SerAPI”的实验性协议(protocol)[我是作者的免责声明]，它位于 1 和 2 之间。SerAPI 是 XML 协议(protocol)的扩展(但使用 SEXP)，它试图提供 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