All geek questions in one place

How to call asidant Coq confirmation from external software

How to call Coq corrector from external software? Does Coq have an API? Is Coq's command line interface rich enough to pass arguments to a file and get a response in the file? I'm interested in Java or C ++ bridges.

This is a legitimate question. Coq is no ordinary business software from which you can expect a developer-compatible API. I had a similar question about Isabelle / HOL and it was a legitimate question with a non-trivial answer.

+4
source share
2 answers

To date, there are three ways to interact with Coq, which are ordered from more effort to less power:

  1. API OCaml: , Coq, OCaml API, , , . API , . OCaml API , , .

  2. XML-: , IDE. Coq, , , .....

  3. . , , Coq.

, "SerAPI" [ ], 1 2. SerAPI XML- ( SEXP), 1 - OCaml.

SerAPI , . -

:

+9

, .

Coq , coqc. Coq . - , . , () , .vo .

:

$ 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

Coq, : https://coq.inria.fr/refman/practical-tools/coq-commands.html

, Coq : 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.

+2

Source: https://habr.com/ru/post/1685007/

More articles:


All Articles