Skip to content

Integrate the output of coq-of-ocaml with the interpreter

Guillaume Claret requested to merge guillaume-claret-integrate-coq-of-ocaml-output into dev

We aim to integrate the whole Coq code generated by coq-of-ocaml from the Tezos economic protocol. We start by a first set of files. It does not include everything, but includes the interpreter and most of its dependencies (for some dependencies, only the .mli file using axioms in there). Concretely, the changes are the followings:

  • update the .gitignore for Coq 8.11;
  • force dependency on Coq >= 8.11;
  • update the dependencies of the project to add the development version of coq-of-ocaml (even if we include the generated Coq files, we need the coq-of-ocaml Coq library for some definitions);
  • activate the -impredicative-set option;
  • include the generated Coq code of the protocol in a of-ocaml/Tezos/ folder;
  • include injection from the types and the syntax of Mi-Cho-Coq; no proofs.
Edited by Raphaël Cauderlier

Merge request reports