Skip to main content

Upgrade coq-of-ocaml to OCaml 4.14

· 3 min read

In an effort to support the latest version of the protocol of Tezos we upgraded coq-of-ocaml to add compatibility with OCaml 4.14. The result is available in the branch ocaml-4.14. We describe here how we made this upgrade.

Usage of Merlin

In coq-of-ocaml we are using Merlin to get the typed abstract syntax tree of OCaml files. We see the AST through the Typedtree interface, together with an access to all the definitions of the current compilation environment. Merlin computes the current environment by understanding how an OCaml project is configured and connecting to the dune build system. The environment is mandatory for certain transformations in coq-of-ocaml, like:

  • finding a canonical name for module types;
  • propagating phantom types.

In order to use Merlin as a library (rather than as a daemon), we vendor the LSP version of rgrinberg in the folder vendor/. This vendored version works with no extra configurations.

Upgrade

When a new version of OCaml is out, we upgrade our vendored version of Merlin to a compatible one. Then we do the necessary changes to coq-of-ocaml, as the interface of the AST generally evolves with small changes. For OCaml 4.14, the main change was some types becoming abstract such as Types.type_expr. To access to the fields of these types, we now need to use a specific getter and do changes such as:

+    match typ.desc with
- match Types.get_desc typ with

This made some patterns in match expressions more complex, but otherwise the changes were very minimal. We ran all the unit-tests of coq-of-ocaml after the upgrade and they were still valid.

Git submodule or copy & paste?

To vendor Merlin we have two possibilities:

  1. Using a Git submodule.
  2. Doing a copy & paste of the code.

The first possibility is more efficient in terms of space, but there are a few disadvantages:

  • we cannot make small modifications if needed;
  • the archives generated by Github do not contain the code of the submodules (see this issue)
  • if a commit in the repository for the submodule disappears, then the submodule is unusable.

The last reason forced us to do a copy & paste for OCaml 4.14. We now have to be cautious not to commit the generate .ml file for the OCaml parser.

Next

The next change will be doing the upgrade to OCaml 5. There should be much more changes, and in particular a new way of handling the effects. We do not know yet if it will be possible to translate the effect handlers to Coq in a nice way.