如何从外部软件调用证明助理Coq [英] How to call proof asistant Coq from external software
问题描述
如何从外部软件呼叫证明助理Coq？ Coq是否有一些API？ Coq命令行界面是否足够丰富，可以在文件中传递参数并在文件中接收响应？我对Java或C ++桥感兴趣。
How to call proof assistant Coq from external software? Does Coq have some API? Is Coq command line interface rich enough to pass arguments in file and receive response in file? I am interested in Java or C++ bridges.
这是合理的问题。 Coq不是可以期望开发人员友好的API的常用商业软件。我有一个关于Isabelle / HOL的类似问题，这是一个具有平凡答案的合理问题。
This is legitimate question. Coq is not the usual business software from which one can expect the developer friendly API. I had similary question about Isabelle/HOL and it was legitimate question with non-trivial answer.
推荐答案
到目前为止，与Coq进行交互的三种方式，从增加精力到降低功率依次进行：
As of today, there are three ways to interact with Coq, ordered from more effort to less power:
-
OCaml API：这就是Coq插件的作用但是，众所周知，OCaml API的某些部分很难掌握，通常需要很高的专业知识。该API也从一个发行版更改为另一个发行版，从而使维护变得很困难。除了查看源代码外，没有关于OCaml API的官方文档，但是有很多维护程度不同的教程随处可见。
The OCaml API: This is what Coq plugins do, however, some parts of the OCaml API are notoriously difficult to master and a high expertise is usually needed. The API also changes from one release to another making maintenance hard. There is not official documentation for the OCaml API other than looking at the source code, but quite a few tutorials with different degrees of maintenance are floating around.
XML协议：这是IDE所使用的。它允许客户端执行基本的Coq文档操作，例如检查部分文档，限制搜索，检索目标等... 官方文档
The XML protocol: This is what IDEs use. It allows the client to perform basic Coq document operations such as checking a part of it, limited search, retrieving goals, etc... official documentation
命令行：与其他答案一样，基本上可以检查Coq是否可以完全编译文件。
The command line: As the other answer details, this basically allows to check whether a file can be fully compiled by Coq.
或者，有一个称为 SerAPI（免责声明，我是作者）位于1到2之间。SerAPI是XML协议的扩展（但使用SEXP），试图提供1的一些优点以及更丰富的查询操作，而没有链接的缺点。 OCaml。
Alternatively, there is an experimental protocol called "SerAPI" [disclaimer I am the author] that lies between 1 and 2. SerAPI is an extension of the XML protocol (but using SEXPs) that tries to provide some advantages of 1 along with richer query operations, without the disadvantages of linking with OCaml.
SerAPI如今处于非常试验阶段，但是对于某些用户来说可能很有用。 网页
SerAPI is at a very experimental stage these days, however it may prove useful for some users. 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
- 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
这篇关于如何从外部软件调用证明助理Coq的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
