[coq] Allow Coq libraries to depend on OCaml ones.

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,18 @@ 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 include_paths ts =
+    List.fold_left ts ~init:Path.Set.empty ~f:(fun acc t ->
+      Path.Set.add acc (Lib.src_dir t))
+
+  let include_flags ts = include_paths ts |> Lib.L.to_iflags
+
+end
+
 type coq_context =
   { coqdep : Action.program
   ; coqc   : Action.program
@@ -43,21 +55,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 +84,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 +111,39 @@ let create_ccoq sctx ~dir =
   ; coqpp  = rr "coqpp"
   }
 
+(* compute include flags and mlpack rules *)
+let setup_ml_deps ~scope ~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 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 +157,17 @@ 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 expander = SC.expander sctx ~dir in
-
   let wrapper_name = coqlib_wrapper_name s in
+
+  let ml_iflags, mlpack_rule =
+    setup_ml_deps ~scope ~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/dir_contents.ml

@@ -406,6 +406,10 @@ let check_no_qualified loc qualif_mode =
   if qualif_mode = Include_subdirs.Qualified then
     Errors.fail loc "(include_subdirs qualified) is not supported yet"
 
+let check_no_unqualified loc qualif_mode =
+  if qualif_mode = Include_subdirs.Unqualified then
+    Errors.fail loc "(include_subdirs qualified) is not supported yet"
+
 let get0_impl (sctx, dir) : result0 =
   let dir_status_db = Super_context.dir_status_db sctx in
   match Dir_status.DB.get dir_status_db ~dir with
@@ -532,6 +536,7 @@ let get0_impl (sctx, dir) : result0 =
       C_sources.make d ~c_sources
     ) in
     let coq_modules = Memo.lazy_ (fun () ->
+      check_no_unqualified Loc.none qualif_mode;
       build_coq_modules_map d ~dir:d.ctx_dir
         ~modules:(coq_modules_of_files ~subdirs:((dir,[],files)::subdirs))) in
     let t =

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/lib.mli

@@ -65,6 +65,8 @@ module L : sig
   type lib
   type nonrec t = t list
 
+  val to_iflags : Path.Set.t -> ('a, 'b) Arg_spec.t
+
   val include_paths : t -> stdlib_dir:Path.t -> Path.Set.t
   val include_flags : t -> stdlib_dir:Path.t -> _ Arg_spec.t
 

src/stdune/path.ml

@@ -51,6 +51,7 @@ module External : sig
   val extension : t -> string
   val is_suffix : t -> suffix:string -> bool
   val split_extension : t -> t * string
+  val set_extension : t -> ext:string -> t
   val as_local : t -> string
 end = struct
   include Interned.No_interning(struct
@@ -124,6 +125,11 @@ end = struct
     let s, ext = Filename.split_extension (to_string t) in
     (make s, ext)
 
+  let set_extension t ~ext =
+    let (base, _) = split_extension t in
+    (to_string base) ^ ext
+    |> make
+
   let cwd () = make (Sys.getcwd ())
   let initial_cwd = cwd ()
 
@@ -159,6 +165,8 @@ module Local : sig
   val split_extension : t -> t * string
   val pp : Format.formatter -> t -> unit
 
+  val set_extension : t -> ext:string -> t
+
   module L : sig
     val relative : ?error_loc:Loc0.t -> t -> string list -> t
   end
@@ -390,6 +398,11 @@ end = struct
     let s, ext = Filename.split_extension (to_string t) in
     (make s, ext)
 
+  let set_extension t ~ext =
+    let (base, _) = split_extension t in
+    (to_string base) ^ ext
+    |> make
+
   module Prefix = struct
     let make_path = make
 
@@ -975,6 +988,12 @@ let split_extension t =
     let t, ext = Local.split_extension t in
     (in_source_tree t, ext)
 
+let set_extension t ~ext =
+  match t with
+  | External t -> external_ (External.set_extension t ~ext)
+  | In_build_dir t -> in_build_dir (Local.set_extension t ~ext)
+  | In_source_tree t -> in_source_tree (Local.set_extension 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: [