如何从外部软件调用校对助理Coq？Coq有一些API吗？Coq命令行界面是否足够丰富以传递文件中的参数并在文件中接收响应？我对Java或C++桥感兴趣.
这是合法的问题.Coq不是通常的商业软件,人们可以期待开发人员友好的API.我对Isabelle/HOL有类似的问题,这是一个非常简单的答案的合法问题.
ejg*_*ego 11
截至今天,有三种方式可以与Coq进行交互,从更多的努力到更低的功率排序:
OCaml API:这是Coq插件所做的,但是,OCaml API的某些部分众所周知难以掌握,并且通常需要高专业知识.API也从一个版本更改为另一个版本,从而使维护变得困难.除了查看源代码之外,还没有OCaml API的官方文档,但是有很多不同维护程度的教程正在浮动.
XML协议:这是IDE使用的.它允许客户端执行基本的Coq文档操作,例如检查它的一部分,有限的搜索,检索目标等... 官方文档
命令行:作为其他答案细节,这基本上允许检查Coq是否可以完全编译文件.
或者,有一个名为"SerAPI"的实验性协议[免责声明我是作者]位于1和2之间.SerAPI是XML协议的扩展(但使用SEXP),试图提供1的一些优点以及更丰富的查询操作,没有与OCaml链接的缺点.
这些天SerAPI处于非常实验阶段,但它可能对某些用户有用.网页
一些额外的链接:
| 归档时间： |
|
| 查看次数： |
440 次 |
| 最近记录： |