How to use Camltac with Dune

Camltac has a particular execution model that requires some setup to work properly with the Dune build system.

Support for Camltac Load

You must tell Dune about your OCaml files for the Camltac Load command to work properly:

dune

;; Create a dummy .v file that simply registers a dependency on your OCaml
;; files, making them available in the `_build` directory.
(rule
  (targets Dummy.v)
  (deps (glob_files *.ml))
  (action (write-file Dummy.v "(* generated dummy target *)")))

Creating a package

If you are creating a package and you’d like users to be able to reference your Camltac modules, you must instruct Dune to install your .camltac folder. For that, you’ll need to work-around some Dune quirks to make it track the .camltac directory:

dune-project

;; The following line may be required to generate directories:
(using directory-targets 0.1)

;; …

dune

;; We cannot simply install .camltac, since Dune complains that it is not
;; generated by a rule.  Hence, we make it believe that the .camltac
;; directory has an associated rule by creating two rules:
;;
;; 1. A rule that moves .camltac to .camltac-tmp, after all .vo files were
;;    produced (which guarantees that .camltac is complete);
;;
;;  2. A rule that moves .camltac-tmp back to .camltac
;;
;; Note that we can't have a single rule that generates .camltac, since
;; Dune eagerly runs `rm -rf .camltac` before the rule (to check that the
;; rule indeed produced the folder).

(rule
 (targets (dir .camltac-tmp))
 (deps (glob_files *.vo) (universe))
 (action (no-infer (run mv .camltac .camltac-tmp))))

(rule
 (targets (dir .camltac))
 (deps .camltac-tmp)
 (action (no-infer (run mv .camltac-tmp .camltac))))

The last step is to install .camltac in the user-contrib directory:

dune

(install
 (section lib_root)
 (package your_lib)
 (dirs (.camltac as coq/user-contrib/YourLib/.camltac)))