`Camltac Run`#

Compiles and runs the given OCaml code in the current Rocq state.

Locality attributes and build directives.

Warning

OCaml code that mutates Rocq’s global state, such as using Summary.ref, should not be made non-local, since their effects would be performed multiple times:

Module M.
  #[export]
  Camltac Run ocaml:{{
    let _ = Summary.ref ~name:"test-value" 0
  }}.
End M.

Import M.Anomaly
"in Summary.declare_summary: Colliding summary names: test-value-SUMMARY vs. test-value-SUMMARY."
Please report at http://rocq-prover.org/bugs/.

Camltac Run#

`Camltac Run`#