[coq] Add coqpp preprocessing stanza.

We add a

```
(coqpp (modules foo bar))
````

stanza, that will look for a `foo.mlg` file and produce a
pre-processed `foo.ml`; similarly for `bar`.

This helps Coq plugin writers to avoid boilerplate and more
importantly, to get the right path on error messages.

doc/coq.rst

@@ -49,6 +49,26 @@ The stanza will build all `.v` files on the given directory. The semantics of fi
   ``coqdep`` and ``coqc`` using Coq's ``-I`` flag; this allows for a Coq
   library to depend on a ML plugin.
 
+Preprocessing with ``coqpp``
+============================
+
+Coq plugin writers usually need to write ``.mlg`` files to extend Coq
+grammar. Such files are pre-processed with `coqpp`; to help plugin
+writers avoid boilerplate we provide a `(coqpp ...)` stanza:
+
+.. code:: scheme
+
+    (coqq (modules <mlg_list>))
+
+which for each ``g_mod`` in ``<mlg_list>```is equivalent to:
+
+.. code:: scheme
+
+    (rule
+     (targets g_mod.ml)
+     (deps (:mlg-file g_mod.mlg))
+     (action (run coqpp %{mlg-file})))
+
 Recursive Qualification of Modules
 ==================================
 

src/coq_rules.ml

@@ -211,3 +211,17 @@ let install_rules ~sctx ~dir s =
       let dst = Path.to_string dst in
       None, Install.(Entry.make Section.Lib_root ~dst vofile))
     |> List.rev_append (coq_plugins_install_rules ~scope ~package ~dst_dir s)
+
+let coqpp_rules ~sctx ~dir (s : Dune_file.CoqPp.t) =
+
+  let scope = SC.find_scope_by_dir sctx dir in
+  let base_dir = Scope.root scope in
+  let cc = create_ccoq sctx ~dir in
+
+  let mlg_rule m =
+    let source = Path.relative dir (m ^ ".mlg") in
+    let target = Path.relative dir (m ^ ".ml") in
+    let args = Arg_spec.[Dep source; Hidden_targets [target]] in
+    Build.run ~dir:base_dir cc.coqpp args in
+
+  List.map ~f:mlg_rule s.modules

src/coq_rules.mli

@@ -18,3 +18,9 @@ val install_rules
   -> dir:Path.t
   -> Dune_file.Coq.t
   -> (Loc.t option * Install.Entry.t) list
+
+val coqpp_rules
+  :  sctx:Super_context.t
+  -> dir:Path.t
+  -> Dune_file.CoqPp.t
+  -> (unit, Action.t) Build.t list

src/dir_contents.ml

@@ -266,10 +266,8 @@ let load_text_files sctx ft_dir
   let generated_files =
     List.concat_map stanzas ~f:(fun stanza ->
       match (stanza : Stanza.t) with
-      | Coq.T _coq ->
-        (* Format.eprintf "[coq] generated_files called at sctx: %a@\n%!" Path.pp (File_tree.Dir.path ft_dir); *)
-        (* FIXME: Need to generate ml files from mlg ? *)
-        []
+      | CoqPp.T { modules; _ } ->
+        List.map modules ~f:(fun m -> m ^ ".ml")
       | Menhir.T menhir ->
         Menhir_rules.targets menhir
       | Rule rule ->

src/dune_file.ml

@@ -1812,6 +1812,25 @@ module Menhir = struct
        })
 end
 
+module CoqPp = struct
+
+  type t =
+    { modules    : string list
+    ; loc        : Loc.t
+    }
+
+  let decode =
+    record
+      (let+ modules = field "modules" (list string)
+       and+ loc = loc in
+       { modules
+       ; loc
+       })
+
+  type Stanza.t += T of t
+
+end
+
 module Coq = struct
 
   type t =
@@ -1867,8 +1886,11 @@ module Coq = struct
 
   let unit_to_sexp () = Sexp.List []
 
+  let coqlib_p = "coqlib", decode >>| fun x -> [T x]
+  let coqpp_p = "coqpp", CoqPp.(decode >>| fun x -> [T x])
+
   let unit_stanzas =
-    let+ r = return ["coqlib", decode >>| fun x -> [T x]] in
+    let+ r = return [coqlib_p; coqpp_p] in
     ((), r)
 
   let key =

src/dune_file.mli

@@ -372,6 +372,16 @@ module Coq : sig
   type Stanza.t += T of t
 end
 
+module CoqPp : sig
+
+  type t =
+    { modules    : string list
+    ; loc        : Loc.t
+    }
+
+  type Stanza.t += T of t
+end
+
 module Alias_conf : sig
   type t =
     { name    : string

src/gen_rules.ml

@@ -188,6 +188,10 @@ module Gen(P : sig val sctx : Super_context.t end) = struct
         let dir = ctx_dir in
         let coq_rules = Coq_rules.setup_rules ~sctx ~dir ~dir_contents m in
         SC.add_rules ~dir:ctx_dir sctx coq_rules
+      | CoqPp.T m ->
+        let dir = ctx_dir in
+        let coqpp_rules = Coq_rules.coqpp_rules ~sctx ~dir m in
+        SC.add_rules ~dir:ctx_dir sctx coqpp_rules
       | _ -> ());
     let dyn_deps =
       let pred =