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
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
- finding a canonical name for module types;
- propagating phantom types.
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:
- Using a Git submodule.
- 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.
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.