OCaml as a Tactic Language for the Rocq Prover
Follow the tour »

Tutorials · How-to guides · Docs · Reference

Overview

Camltac is an OCaml plugin for Rocq that lets you run OCaml code within Rocq scripts. Camltac makes it possible to define OCaml meta-programs and tactics, and run them in the current Rocq state without the friction and boilerplate of setting up a plugin.

Camltac is both a tactic and a meta-programming language:

• As a tactic language, Camltac provides constructs inspired by Ltac2, including term quotations ({%constr| … |}), pattern matching (match%rocq), and antiquotations using ppx_rocq. Camltac makes it easy to define new tactics by providing the usual tacticals from Ltac2, and a dedicated FFI with Ltac and Ltac2.
• As a meta-programming language, Camltac offers a complete meta-programming experience by allowing access to Rocq's internal APIs and state. To ensure stability, Camltac includes the Ltac2 APIs which provide a simple entry point to meta-programming in OCaml.

Have a look at the tour of Camltac for a walkthrough of Camltac's features, or the examples directory for self-contained examples of using Camltac.

Features

Quotations for building terms:

{%constr| … |}, {%open_constr| … |}, {%preterm| … |}, etc.

Antiquotations:

{%constr| %{x} + %{y} |}

Pattern-matching over terms:

match%rocq x with, match%lazy x with, match%multi x with

Pattern-matching over goals:

match%rocq goal with, match%lazy goal with, match%multi goal with

Modules:

Camltac Module M := ocaml:{{ … }}.

Interoperability with Ltac2:

Ltac2.FFI.define "my_tactic" (constr @-> tac constr) (fun t -> …)

Ltac2 APIs and tacticals:

See the Ltac2 APIs reference.

Support for OCaml libraries and preprocessors:

See examples/ParallelTactics.v and examples/Tracing.v.

Access to Rocq state and APIs:

See a few examples.

Setup

Camltac is available on Rocq's opam repository and supports Rocq ≥ 9.0 with OCaml ≥ 4.14.

To install from opam (rocq-released):

opam install rocq-camltac

To install from Git:

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

Then, import Camltac in your Rocq files (Require Import Camltac.Camltac.) and you're ready to go! 🎉

License

Camltac is free software under the GNU LGPL 2.1 license.