Comment appeler proof asistant Coq à partir d'un logiciel externe

Question

Comment appeler proof assistant Coq à partir d'un logiciel externe? Est-ce que Coq a une API? L'interface de ligne de commande Coq est-elle suffisamment riche pour transmettre des arguments dans un fichier et recevoir une réponse dans un fichier? Je suis intéressé par les ponts Java ou C++.

Ceci est une question légitime. Coq n'est pas le logiciel d'entreprise habituel à partir duquel on peut s'attendre à l'API conviviale pour les développeurs. J'avais une question similaire à propos d'Isabelle/HOL et c'était une question légitime avec une réponse non triviale.

Answer 1

A ce jour, il y a trois façons d'interagir avec Coq, commandé à plus d'efforts pour moins de puissance:

1. Utilisation de l'API OCaml: C'est ce que les plugins Coq font, cependant, certaines parties du OCaml API sont notoirement difficiles à maîtriser et une haute expertise est généralement nécessaire. L'API change également d'une version à l'autre, ce qui rend la maintenance difficile. Il n'y a pas de documentation officielle pour l'API OCaml autre que de regarder le code source, mais quelques tutoriels avec différents niveaux de maintenance circulent.

2. Utilisation du protocole XML: c'est ce que les EDI utilisent. Il permet au client d'effectuer des opérations de base de documents Coq tels que la vérification d'une partie, recherche limitée, la récupération de buts, etc ... official documentation

3. Utilisation de la ligne de commande: Comme les autres détails de réponse, ce qui permet essentiellement de vérifier si un fichier peut être entièrement compilé par Coq.

Sinon, il y a un protocole expérimental appelé « Serapi » [disclaimer je suis l'auteur] qui se trouve entre 1 et 2. Serapi est une extension du protocole XML (mais en utilisant sexps) qui tente de fournir des avantages de 1 avec des opérations de requête plus riches, sans les inconvénients de la liaison avec OCaml. SerAPI est à un stade très expérimental ces jours-ci, mais il peut s'avérer utile pour certains utilisateurs.webpage

Quelques liens supplémentaires:

• 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

La ligne de commande semble être la voie à suivre.

Coq inclut plusieurs outils de ligne de commande, y compris le compilateur coqc. Ce programme prend un fichier de théorie Coq en entrée et essaie de le compiler. Si quelque chose ne va pas avec la théorie, la commande échoue avec un code de sortie différent de zéro et écrit des commentaires sur ses flux de sortie. Si tout est OK, la commande est (généralement) silencieuse, quitte avec un code de sortie zéro et écrit un fichier .vo contenant la théorie compilée.

Par exemple:

$ 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 

Voici les documents pour les outils de ligne de commande Coq, qui peut prendre plusieurs drapeaux: https://coq.inria.fr/distrib/current/refman/Reference-Manual016.html

Je suis au courant de deux outils qui utilisent Coq comme moteur preuve subordonné: Frama-C et Why3. En regardant les sources à https://github.com/Frama-C/Frama-C-snapshot/blob/master/src/plugins/wp/ProverCoq.ml (méthodes compile et check) et au https://github.com/AdaCore/why3/tree/master/drivers, ces outils semblent également déverser des théories Coq dans un fichier, puis appeler les outils de ligne de commande de Coq. Pour autant que je sache, il n'y a plus d'API directe pour Coq.