[coq] Allow Coq libraries to depend on ML plugins.

We add a new field `(libraries <ocaml_libraries>)` to the `coqlib`
stanza for specifying dependencies on OCaml libs, such as plugins.

The current implementation has to workaround a couple of `coqdep`
problem:

- `-I` flags to `coqdep` must refer to the build tree as to find the
  `.cmxs` file, this is different from what OCaml needs;
- `coqdep` needs to find the `foo.mlpack` file as to emit the correct
  `cmxs` dependency. However such file won't be available for
  system-installed plugins.

We solve the first one by manually computing the include flags, and
the second one by adding a conditional dependency so we don't fail if
the file is missing.

We should improve `coqdep` so these kind of hacks are not necessary.

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

doc/coq.rst

@@ -31,10 +31,10 @@ The basic form for defining Coq libraries is very similar to the OCaml form:
      (public_name <package.lib_name>)
      (synopsis <text>)
      (modules <ordered_set_lang>)
+     (libraries <ocaml_libraries>)
      (flags <coq_flags>))
 
-The stanza will build all `.v` files on the given directory.
-The semantics of fields is:
+The stanza will build all `.v` files on the given directory. The semantics of fields is:
 
 - ``<module_prefix>>`` will be used as the default Coq library prefix ``-R``,
 - the ``modules`` field does allow to constraint the set of modules
@@ -43,27 +43,30 @@ The semantics of fields is:
   files; files will be installed in
   ``lib/coq/user-contrib/<module_prefix>``, as customary in the
   make-based Coq package eco-system,
-- ``<coq_flags>`` will be passed to ``coqc``.
+- ``<coq_flags>`` will be passed to ``coqc``,
+- the path to installed locations of ``<ocaml_libraries>`` will be passed to
+  ``coqdep`` and ``coqc`` using Coq's ``-I`` flag; this allows for a Coq
+  library to depend on a ML plugin.
 
-Library Composition and Handling
-================================
+Recursive Qualification of Modules
+==================================
 
-The ``coqlib`` stanza does not yet support composition of Coq
-libraries. In the 0.1 version of the language, libraries are located
-using Coq's built-in library management, thus Coq will always resort
-to the installed version of a particular library.
+If you add:
 
-This will be fixed in the future.
+.. code:: scheme
 
-Recursive modules
-=================
+    (include_subdirs qualified)
 
-Adding:
+to a ``dune`` file, Dune will to consider that all the modules in
+their directory and sub-directories, adding a prefix to the module
+name in the usual Coq style for sub-directories. For example, file ``A/b/C.v`` will be module ``A.b.C``.
 
-.. code:: scheme
+Limitations
+===========
+
+- composition and scoping of Coq libraries is still not possible. For now, libraries are located using Coq's built-in library management,
+- .v always depend on the native version of a plugin,
+- a ``foo.mlpack`` file must the present for locally defined plugins to work, this is a limitation of coqdep,
+- Coq plugins are installed into their regular OCaml library path.
 
-    (include_subdirs qualified)
 
-to the ``dune`` file will make Dune to consider all the modules in the
-current directory and sub-directories, qualified in the current Coq
-style.

src/build.ml

@@ -154,6 +154,16 @@ let file_exists_opt p t =
     ~then_:(t >>^ Option.some)
     ~else_:(arr (Fn.const None))
 
+let paths_existing paths =
+  List.fold_left paths
+    ~init:(return true)
+    ~f:(fun acc file ->
+      if_file_exists file
+        ~then_:(path file)
+        ~else_:(arr Fn.id)
+      >>>
+      acc)
+
 let fail ?targets x =
   match targets with
   | None -> Fail x

src/build.mli

@@ -69,6 +69,10 @@ val path_set : Path.Set.t -> ('a, 'a) t
     dependencies of the action produced by the build arrow. *)
 val paths_matching : loc:Loc.t -> File_selector.t -> ('a, Path.Set.t) t
 
+(** [paths_existing paths] will require as dependencies the files that
+    actually exist, and return true if the all the paths do actually exist. *)
+val paths_existing : Path.t list -> ('a, bool) t
+
 (** [env_var v] records [v] as an environment variable that is read by the
     action produced by the build arrow. *)
 val env_var : string -> ('a, 'a) t

src/coq_rules.ml

@@ -8,6 +8,27 @@ module SC = Super_context
 
 let coq_debug = false
 
+(* Coqdep / Coq expect the deps to the directory where the plugin cmxs
+   file are. This seems to correspond to src_dir. *)
+module Util = struct
+
+  let to_iflags dirs =
+    Arg_spec.S
+      (Path.Set.fold dirs ~init:[] ~f:(fun dir acc ->
+         Arg_spec.Path dir :: A "-I" :: acc)
+       |> List.rev)
+
+  let include_paths ts ~stdlib_dir =
+    let dirs =
+      List.fold_left ts ~init:Path.Set.empty ~f:(fun acc t ->
+        Path.Set.add acc (Lib.src_dir t))
+    in
+    Path.Set.remove dirs stdlib_dir
+
+  let include_flags ts ~stdlib_dir =
+    to_iflags (include_paths ts ~stdlib_dir)
+end
+
 type coq_context =
   { coqdep : Action.program
   ; coqc   : Action.program
@@ -43,21 +64,26 @@ let parse_coqdep ~coq_module (lines : string list) =
     then Format.eprintf "deps for %a: %a@\n%!" Path.pp source Fmt.(list text) deps;
     deps
 
-let setup_rule ~expander ~dir ~cc ~source_rule ~wrapper_name ~cflags coq_module =
+let setup_rule ~expander ~dir ~cc ~source_rule ~wrapper_name
+      ~coq_flags ~ml_iflags ~mlpack_rule coq_module =
 
   if coq_debug
   then Format.eprintf "gen_rule coq_module: %a@\n%!" Coq_module.pp coq_module;
+
   let obj_dir = dir in
   let source    = Coq_module.source coq_module in
   let stdout_to = Coq_module.obj_file ~obj_dir ~ext:".v.d" coq_module in
   let object_to = Coq_module.obj_file ~obj_dir ~ext:".vo"  coq_module in
 
   let iflags = Arg_spec.As ["-R"; "."; wrapper_name] in
-  let cd_arg = Arg_spec.[ iflags; Dep source ] in
+  let cd_arg : (string list, _) Arg_spec.t list =
+    Arg_spec.[ As ["-dyndep"; "opt"]; iflags; ml_iflags; Dep source ] in
 
-  (* coqdep needs the full source to be present :( *)
+  (* coqdep needs the full source + plugin's mlpack to be present :( *)
   let coqdep_rule =
-    source_rule >>>
+    (* This is weird stuff in order to adapt the rule so we can reuse
+       ml_iflags :( I wish we had more flexible typing. *)
+    ((fun () -> []) ^>> source_rule &&& mlpack_rule) >>^ fst >>>
     Build.run ~dir ~stdout_to cc.coqdep cd_arg
   in
 
@@ -67,14 +93,18 @@ let setup_rule ~expander ~dir ~cc ~source_rule ~wrapper_name ~cflags coq_module
     parse_coqdep ~coq_module >>^
     List.map ~f:(Path.relative dir)
   ) in
+
   let cc_arg = Arg_spec.[
     iflags;
+    ml_iflags;
     Dep source;
     Hidden_targets [object_to] ]
   in
+
+  (* Rules for the files *)
   [coqdep_rule;
    deps_of >>>
-   Expander.expand_and_eval_set expander cflags ~standard:(Build.return []) >>>
+   Expander.expand_and_eval_set expander coq_flags ~standard:(Build.return []) >>>
    Build.run ~dir cc.coqc (Dyn (fun flags -> As flags) :: cc_arg)
   ]
 
@@ -90,11 +120,39 @@ let create_ccoq sctx ~dir =
   ; coqpp  = rr "coqpp"
   }
 
+(* compute include flags and mlpack rules *)
+let setup_ml_deps ~scope ~stdlib_dir ~loc libs =
+
+  (* coqdep expects an mlpack file next to the sources otherwise it
+   * will omit the cmxs deps *)
+  let ml_pack_files lib =
+    let plugins = Mode.Dict.get (Lib.plugins lib) Mode.Native in
+    let to_mlpack file = Path.set_extension file ~ext:".mlpack" in
+    List.map plugins ~f:to_mlpack
+  in
+
+  (* Pair of include flags and paths to mlpack *)
+  let ml_iflags, mlpack =
+    let lib_db = Scope.libs scope in
+    match Lib.DB.find_many ~loc lib_db
+            (List.concat_map ~f:Dune_file.Lib_dep.to_lib_names libs) with
+    | Ok libs ->
+      Util.include_flags ~stdlib_dir libs, List.concat_map ~f:ml_pack_files libs
+    | Error exn ->
+      Errors.fail loc "ML dependencies for Coq library %a"
+        (Exn.pp_uncaught ~backtrace:"") exn
+  in
+
+  (* If the mlpack files don't exist, don't fail *)
+  ml_iflags, Build.paths_existing mlpack
+
 let coqlib_wrapper_name (s : Dune_file.Coq.t) =
   Lib_name.Local.to_string (snd s.name)
 
 let setup_rules ~sctx ~dir ~dir_contents (s : Dune_file.Coq.t) =
 
+  let scope = SC.find_scope_by_dir sctx dir in
+
   if coq_debug then begin
     let scope = SC.find_scope_by_dir sctx dir in
     Format.eprintf "[gen_rules] @[dir: %a@\nscope: %a@]@\n%!"
@@ -108,13 +166,18 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Dune_file.Coq.t) =
   (* coqdep requires all the files to be in the tree to produce correct
      dependencies *)
   let source_rule = Build.paths (List.map ~f:Coq_module.source coq_modules) in
-  let cflags = s.flags in
+  let coq_flags = s.flags in
+  let stdlib_dir = (SC.context sctx).stdlib_dir in
   let expander = SC.expander sctx ~dir in
-
   let wrapper_name = coqlib_wrapper_name s in
+
+  let ml_iflags, mlpack_rule =
+    setup_ml_deps ~scope ~stdlib_dir ~loc:s.loc s.libraries in
+
   let coq_rules =
     List.concat_map
-      ~f:(setup_rule ~expander ~dir ~cc ~source_rule ~wrapper_name ~cflags) coq_modules in
+      ~f:(setup_rule ~expander ~dir ~cc ~source_rule ~wrapper_name ~coq_flags
+            ~ml_iflags ~mlpack_rule) coq_modules in
   coq_rules
 
 let install_rules ~sctx ~dir s =

src/format_rules.ml

@@ -22,24 +22,10 @@ let rec subdirs_until_root dir =
   | None -> [dir]
   | Some d -> dir :: subdirs_until_root d
 
-let depend_on_existing_paths paths =
-  let open Build.O in
-  let build_id = Build.arr Fn.id in
-  List.fold_left
-    ~f:(fun acc path ->
-      Build.if_file_exists
-        path
-        ~then_:(Build.path path)
-        ~else_:build_id
-      >>>
-      acc)
-    ~init:build_id
-    paths
-
 let depend_on_files ~named dir =
   subdirs_until_root dir
   |> List.concat_map ~f:(fun dir -> List.map named ~f:(Path.relative dir))
-  |> depend_on_existing_paths
+  |> Build.paths_existing
 
 let formatted = ".formatted"
 

src/stdune/path.ml

@@ -975,6 +975,10 @@ let split_extension t =
     let t, ext = Local.split_extension t in
     (in_source_tree t, ext)
 
+let set_extension t ~ext =
+  let t, _ = split_extension t in
+  of_string (to_string t ^ ext)
+
 let pp ppf t = Format.pp_print_string ppf (to_string_maybe_quoted t)
 
 let pp_in_source ppf t =

src/stdune/path.mli

@@ -163,6 +163,9 @@ val mkdir_p : t -> unit
 val extension : t -> string
 val split_extension : t -> t * string
 
+(** [set_extension path ~ext] replaces extension of [path] by [ext] *)
+val set_extension : t -> ext:string -> t
+
 val pp : Format.formatter -> t -> unit
 val pp_in_source : Format.formatter -> t -> unit
 val pp_debug : Format.formatter -> t -> unit

test/blackbox-tests/test-cases/coq/ml_lib/dune-project

@@ -0,0 +1,3 @@
+(lang dune 1.8)
+
+(using coq 0.1)

test/blackbox-tests/test-cases/coq/ml_lib/ml_lib.opam

@@ -0,0 +1 @@
+

test/blackbox-tests/test-cases/coq/ml_lib/src/dune

@@ -0,0 +1,4 @@
+(library
+ (public_name ml_lib.ml_plugin)
+ (name ml_plugin)
+ (libraries coq.plugins.ltac))

test/blackbox-tests/test-cases/coq/ml_lib/src/simple.ml

@@ -0,0 +1 @@
+let _ = 3

test/blackbox-tests/test-cases/coq/ml_lib/theories/a.v

@@ -0,0 +1,2 @@
+Declare ML Module "ml_plugin".
+

test/blackbox-tests/test-cases/coq/ml_lib/theories/dune

@@ -0,0 +1,6 @@
+(coqlib
+ (name Plugin)
+ (public_name ml_lib.Plugin)
+ (synopsis "Test Plugin")
+ (libraries coq.plugins.ltac ml_lib.ml_plugin)
+ (modules :standard))

test/blackbox-tests/test-cases/coq/run.t

@@ -16,6 +16,19 @@
           coqc c/ooo.vo
           coqc a/bar.vo
 
+  $ dune build --root ml_lib --display short --debug-dependency-path @all
+  Entering directory 'ml_lib'
+        ocamlc src/.ml_plugin.objs/byte/ml_plugin.{cmi,cmo,cmt}
+      ocamlopt src/.ml_plugin.objs/native/ml_plugin.{cmx,o}
+      ocamldep src/.ml_plugin.objs/simple.ml.d
+        ocamlc src/.ml_plugin.objs/byte/ml_plugin__Simple.{cmi,cmo,cmt}
+        ocamlc src/ml_plugin.cma
+        coqdep theories/a.v.d
+      ocamlopt src/.ml_plugin.objs/native/ml_plugin__Simple.{cmx,o}
+      ocamlopt src/ml_plugin.{a,cmxa}
+      ocamlopt src/ml_plugin.cmxs
+          coqc theories/a.vo
+
   $ dune build --root base --display short --debug-dependency-path @default
   Entering directory 'base'
   lib: [