How to call proof asistant Coq from external software

10
votes

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.

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.

2
coq
I see 3 close votes on this question, saying the question is too broad. I, personally, think it is a legitimate question. Probably someone could share some insight on how to make the question better (more focused, if you will), instead of just closing it right away? – Anton Trunov
The framing of the question already seems to be precise enough to get an informative answer from a Coq developer. :-) But if the OP has a specific application in mind perhaps people can be even more helpful. – Benjamin Pierce
My intention is to control Coq from github.com/opencog and use it as formal reasoning component (I am trying to implement additional logics in it) along the soft reasoning and knowledge representation available in OpenCog. But programming is not an issue here at all. If Coq is somehow available (and it is - as it can been from answers) from outside then that is fine. I can adapt, no problems. Programmatically talking to Coq is the simplest issue in my plans. – TomR

2 Answers

13
votes

As of today, there are three ways to interact with Coq, ordered from more effort to less power:

  1. 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.

  2. 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

  3. The command line: As the other answer details, this basically allows to check whether a file can be fully compiled by Coq.

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 is at a very experimental stage these days, however it may prove useful for some users. webpage

Some additional links:

2
votes

The command line seems to be the way to go.

Coq includes several command-line tools, including the coqc compiler. This program takes a Coq theory file as input and tries to compile it. If something is wrong with the theory, the command fails with a non-zero exit code and writes some feedback onto its output streams. If everything is OK, the command is (typically) silent, exits with a zero exit code, and writes a .vo file containing the compiled theory.

For example:

$ 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

Here are the docs for Coq's command line tools, which can take various flags: https://coq.inria.fr/refman/practical-tools/coq-commands.html

I am aware of two tools that use Coq as a subordinate proof engine: Frama-C and Why3. Looking at the sources at 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, these tools also seem to dump Coq theories to a file and then call Coq's command-line tools. As far as I can tell, there is no more direct API for Coq.