Installation#

We recommend using opam to install Camltac.

Using opam#

Camltac is available on the rocq-released opam repository, and requires Rocq ≥ 9.0 with OCaml ≥ 4.14. To install Camltac:

  1. Add the rocq-released opam repository:

    opam repo add rocq-released https://rocq-prover.github.io/opam/released/

  2. Install Camltac:

    opam install rocq-camltac

Building from sources#

You can build Camltac from sources using Dune:

git clone https://github.com/epfl-systemf/camltac.git
cd camltac
dune build @install -p rocq-camltac

Testing your setup#

To test that your setup is OK, the following code should evaluate correctly:

[Loading ML file rocq-runtime.plugins.ltac2 (implicit dependency) ... done]
[Loading ML file ppx_rocq.runtime (implicit dependency) ... done]
[Loading ML file rocq-mltac2 (implicit dependency) ... done]
[Loading ML file rocq-camltac.plugin.api (implicit dependency) ... done]
[Loading ML file rocq-camltac.plugin.runtime (implicit dependency) ... done]
[Loading ML file rocq-camltac.plugin ... done]



- : int = 2