Skip to content

Add a rule to run coq-of-ocaml in the CI

Guillaume Claret requested to merge guillaume-claret@add-coq-of-ocaml-to-ci into proto-proposal

Attempt to add a CI rule to check the conversion to Coq. I hope to get some kind of linting from coq-of-ocaml, so that:

  • it is quick to fix if needed;
  • main errors are avoided.

What we do:

  • run coq-of-ocaml on each file of the protocol;
  • stop at the first conversion errors, with a "failure is allowed" mode.

We add an entry in the CI file, plus a coq-of-ocaml folder in the protocol with the configuration for coq-of-ocaml. Note that we check that coq-of-ocaml generate some Coq with no errors, but we do not check that the generated code compiles. This is not necessarily true, name collisions or missing GADTs annotations are examples of errors.

Part of the task https://gitlab.com/nomadic-labs/tezos/-/issues/161

Edited by Guillaume Claret

Merge request reports