Search code examples
coq

How to call proof asistant Coq from external software

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.

Solution

  • answer edited for 2023 (disclaimer, I'm the main author of a few tools mentioned here)

    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, tho the automatically generated API docs may prove useful. There is an official plugin tutorial, and a few more unofficial ones floating around. Moreover the current Coq OCaml API is lacking some essential capabilities such as incremental document processing, see the next point.

    2. coq-lsp: The coq-lsp project allows users to talk to Coq using the Language Server Protocol standard. This is the protocol of choice for user interfaces. The protocol is language independent, but can be used easily from many other languages that provide LSP client libraries. coq-lsp is built on top a generic document manager called Flèche, implemented in OCaml, which offers a super-set of the LSP functionality.

    3. The command line: As the other answer details, this basically allows to check whether a file can be fully compiled by Coq. There are plans for the command line to become a simple LSP client.

    Experimental ways

    1. PyCoq: PyCoq provides a direct Python binding to Coq. As of today, PyCoq exposes the SerAPI 1.0 API, but in the future it will expose Flèche's API which is a superset of LSP. The project doesn't have a lot of manpower these days, so help is welcome.

    Deprecated ways:

    1. SerAPI: SerAPI is a protocol for machine-friendly communication with Coq, and provides mature interaction and seralization support. Some parts of it are tied to the OCaml API so it may not be fully stable, see webpage for more information. SerAPI's API has been deprecated in favor of LSP support, so while the project is still maintained, I strongly recommended to migrate your application to coq-lsp which offers many advantages over SerAPI.

    2. The XML protocol: This is what CoqIDE uses. It allows the client to perform basic Coq document operations such as checking a part of it, limited search, retrieving goals, etc... official documentation This API has several shortcomings and may be scheduled for removal. I don't recommend using it.

    3. Coqtop: some utils interact with the coqtop REPL, this is highly non-recommended.

    Some additional links: