Quickstart#

This page gives simple examples of using Camltac. You can also follow the tour, follow our tutorials, or have a look at examples for more examples of projects using Camltac.

To try these examples, you’ll need to have Camltac installed on your machine. See Installation.

Initializing a project#

To add Camltac to an existing project, you simply need to declare a dependency on the Camltac theory (in your rocq.theory stanza, if you’re using Dune), and add the following line to your file:

Require Import Camltac.Camltac.[Loading ML file rocq-runtime.plugins.ltac2 (implicit dependency) ... done]
[Loading ML file ppx_rocq.runtime (implicit dependency) ... done]
[Loading ML file rocq-mltac2 (implicit dependency) ... done]
[Loading ML file rocq-camltac.plugin.api (implicit dependency) ... done]
[Loading ML file rocq-camltac.plugin.runtime (implicit dependency) ... done]
[Loading ML file rocq-camltac.plugin ... done]

“Hello, world!”#

In Camltac, the most primitive command is Camltac Run, which runs OCaml code in the current context:

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

Defining a module#

Camltac lets you define modules to reuse definitions across OCaml snippets:

Camltac Module M := ocaml:{{
  let one = 1
}}.

Camltac Run ocaml:{{
  Feedback.msg_info (Pp.int (M.one))
}}.1

Modules in Camltac follow Rocq’s locality attributes, so the following works as well:

Module M.
  (* This module is not visible outside of M. *)
  #[local]
  Camltac Module Local := ocaml:{{
    let foo = "foo"
  }}.

  (* This module is: *)
  #[export]
  Camltac Module Export := ocaml:{{
    let bar = Local.foo
  }}.
End M.

Import M.

Camltac Run ocaml:{{ Feedback.msg_info (Pp.str Export.bar) }}.foo

Camltac Run ocaml:{{ Feedback.msg_info (Pp.str Local.foo) }}.Unbound module Local

Writing a tactic#

A tactic is a value of type a tactic for some a. To evaluate a tactic, use Camltac Eval:

Camltac Eval ocaml:(return 0).- : int = 0
Camltac Eval ocaml:({%constr| forall x : nat, x = x |}).- : constr = (forall x : nat, x = x)
Camltac Eval ocaml:(let* x = {%constr| 1 |} in {%constr| %{x} + %{x} |}).- : constr = (1 + 1)