Using internal Rocq APIs#

Camltac provides full access to Rocq’s internal APIs, since the OCaml code runs in the Rocq process. This allows us to access Rocq’s latest features, query Rocq for detailed information, or implement features traditionally reserved to OCaml plugins.

For example, here’s an implementation of a simple mutable counter that follows backtracks using Rocq’s Summary module:

Camltac Module Counter := ocaml:{{
  let value =
    Summary.ref ~stage:Interp ~name:"counter" 0

  let inc () =
    value := !value + 1
  let print () =
    Feedback.msg_info (Pp.int !value)
}}.

Try it out for yourself: run over these snippets, and backtrack to see the effect!

Module M.
  
0

  Camltac Run ocaml:(Counter.inc ()).
  
1

End M.

(* At the end of the module, the counter is backtracked: *)

0


(* …and replayed upon import: *)
Camltac Run ocaml:(Counter.inc ()).

1
2