Skip to content

Compile most protocol files in Coq 馃悢

Guillaume Claret requested to merge clarus1/tezos:guillaume-claret@compile-base-files-for-coq-of-ocaml into master

Context

With this MR we aim to compile most of the protocol files to working Coq files. This amounts to check that coq-of-ocaml runs without warnings, but also to compile the generated files in Coq (we test it locally).

We try to make minimal changes (renamings, type annotations, OCaml @ annotations). This is related to the issues #1141 and #1484

Manually testing the MR

There should be no regressions (code changes at various places in the economic protocol which should not impact the behavior).

Status

All the files are compiling but the following (we stop there in this MR):

  • script_interpreter.ml
  • script_interpreter_defs.ml
  • script_ir_translator.ml

We count the .ml files of the protocol (not the .mli files), and one file for the environment. We put into axiom some complex functions, especially the ones with GADTs.

Edited by Guillaume Claret

Merge request reports