Running OCaml code

At its core, Camltac provides a way to run OCaml code within Rocq files. Following the tradition in the programming community, let’s print “Hello world!”:

Camltac Run ocaml:{{
  Feedback.msg_info (Pp.str "Hello world!")
}}.
Hello world!

Camltac recognizes OCaml syntax embedded between {{ and }}, and interprets it as top-level OCaml expressions (i.e. the same expressions that you would put in an .ml file). This means, for example, that you can use let bindings:

Camltac Run ocaml:{{
  let hello = "Hello"
  let world = " wonderful world!"

  let () = Feedback.msg_info (Pp.str (hello ^ world))
}}.
Hello wonderful world!

Here, hello and world cannot be accessed outside of the curly braces. To expose them, you need to define a module:

Camltac Module M := ocaml:{{
  let hello = "Hello"
  let world = " from module M!"
}}.

Camltac Run ocaml:{{
  Feedback.msg_info (Pp.str (M.hello ^ M.world))
}}.
Hello from module M!

Camltac can also load external .ml files:

Camltac Load "file.ml".
Hello from file.ml!

The Camltac Load "file.ml" command behaves equivalently to Camltac Module File := ocaml:(<contents of file.ml>).

Note

There is some setup required for Camltac Load to work with Dune, described in the How to use Camltac with Dune guide.