Synopsis

ocaml2zoo is a tool to translate OCaml programs into Zoo, a deeply embedded language living inside Coq.

To translate the dune project living in the proj directory to the dst directory (where Coq files are generated), run:

ocaml2zoo proj dst

Building

First, you need to install opam (>= 2.0).

To make sure it is up-to-date, run:

opam update --all --repositories

Then, you need to install this custom version of the OCaml compiler featuring atomic record fields, atomic arrays and generative constructors. Hopefully, it should be merged into the OCaml compiler one day.

The following commands take care of this:

opam switch create . --empty
eval $(opam env --switch=. --set-switch)
opam pin add ocaml-variants git+https://github.com/clef-men/ocaml#generative_constructors --yes

Then, install dependencies with:

opam install . --deps-only --yes

Finally, to compile ocaml2zoo, run:

make