Camltac’s execution model

Camltac has a particular execution model, since it embeds a full programming language (OCaml) inside Rocq. Hence, several steps are required before OCaml code can be run.

We can broadly distinguish between actions taken during the syntactic interpretation (or synterp) phase, and actions during the interpretation (interp) phase.

Syntactic interpretation

During this phase, Camltac parses and compiles snippets, and internally keeps track of compiled modules to be able to reference them in later compilations.

• Parsing
• Build directives
• Compilation

Interpretation

The interpretation phase takes care of loading compiled OCaml code in the Rocq process, through dynamic linking and the runtime.

• Dynamic linking
• Camltac’s runtime