如何從外部軟件呼叫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。