[wip] [coq] Allow dependencies and composition with local Coq libraries.

We support simple composition of Coq libraries using the `(theories ...)` field. This is a work-in-progress and I am submitting to gather feedback. - Todo Before Merge: + validation of library names must be adapted to Coq's conventions. + review error handling + add tests - Would be nice to have / next PRs: + Closure of theory dependencies. + Allow to depend on libraries installed globally. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ocaml · Apr 12, 2019 · bf5fff2 · bf5fff2
1 parent d08702b
commit bf5fff2
Show file tree

Hide file tree

Showing 12 changed files with 207 additions and 47 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,6 +1,9 @@
 unreleased
 ----------
 
+- [coq] Basic support for theory dependencies on Coq theories using
+  new field `(theories ...)` (#2053, @ejgallego, review by @rgrinberg)
+
 - [coq] Rename `(coqlib ...)` to `(coq.theory ...)`, support for
   `coqlib` will be dropped in the 1.0 version of the Coq language
   (#2055, @ejgallego)

diff --git a/doc/coq.rst b/doc/coq.rst
@@ -8,7 +8,8 @@ Dune is also able to build Coq developments. A Coq project is a mix of
 Coq ``.v`` files and (optionally) OCaml libraries linking to the Coq
 API (in which case we say the project is a *Coq plugin*). To enable
 Coq support in a dune project, the language version should be selected
-in the ``dune-project`` file. For example:
+in the ``dune-project`` file. As of today, the only version supported
+is ``0.1`` and is experimental:
 
 .. code:: scheme
 
@@ -32,11 +33,12 @@ The basic form for defining Coq libraries is very similar to the OCaml form:
      (synopsis <text>)
      (modules <ordered_set_lang>)
      (libraries <ocaml_libraries>)
+     (theories <coq_libraries>)
      (flags <coq_flags>))
 
 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``,
+- ``<module_prefix>`` will be used as the default Coq library prefix ``-R``,
 - the ``modules`` field does allow to constraint the set of modules
   included in the library, similarly to its OCaml counterpart,
 - ``public_name`` will make Dune generate install rules for the `.vo`
@@ -47,7 +49,10 @@ The stanza will build all `.v` files on the given directory. The semantics of fi
 - ``<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 to depend on a ML plugin,
+- you can depend on in-tree ``<coq_libraries>``, in this case, Dune
+  will pass to Coq the the corresponding `-Q` flag for the libraries
+  and their dependencies.
 
 Preprocessing with ``coqpp``
 ============================
@@ -82,9 +87,17 @@ 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``.
 
+Composition of Coq libraries
+============================
+
+For local Coq libraries, composition is possible using the
+``theories`` field. Libraries are wrapped, however for their own
+compilation the scope is opened so qualification is not necessary.
+
+TODO: "rules about prefix shadowing"
+
 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,
diff --git a/src/coq_lib.ml b/src/coq_lib.ml
@@ -0,0 +1,49 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(*     Written by: Emilio Jesús Gallego Arias  *)
+
+open! Stdune
+
+type t =
+  { name : Lib_name.t
+  ; src_root : Path.t
+  ; obj_root : Path.t
+  ; package : Package.Name.t option
+  }
+
+let name l = l.name
+let src_root l = l.src_root
+let obj_root l = l.obj_root
+let package l = l.package
+
+module DB = struct
+
+  type nonrec t = t Lib_name.Map.t
+
+  let create_from_stanza (dir, s : Path.t * Dune_file.Coq.t) =
+    let name = Dune_file.Coq.best_name s in
+    name,
+    { name
+    ; obj_root = dir
+    ; src_root = dir
+    ; package = Option.map s.public ~f:(fun p -> p.package.name)
+    }
+
+  (* XXX: Error handling: register errors and printers *)
+  let create_from_coqlib_stanzas sl =
+    match Lib_name.Map.of_list_map ~f:create_from_stanza sl with
+    | Ok m -> m
+    | Error (name, _w1, w2) ->
+      let loc = (snd w2).loc in
+      raise (Errors.exnf loc "Duplicate theory name: %a" Lib_name.pp name)
+
+  let resolve db (loc,name) =
+    match Lib_name.Map.find db name with
+    | None ->
+      Error (Errors.exnf loc "Theory %a not found" Lib_name.pp name)
+    | Some s -> Ok s
+
+  let find_many t ~loc =
+    Result.List.map ~f:(fun name -> resolve t (loc, name))
+
+end
diff --git a/src/coq_lib.mli b/src/coq_lib.mli
@@ -0,0 +1,33 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(*     Written by: Emilio Jesús Gallego Arias  *)
+
+open! Stdune
+
+type t
+
+val name : t -> Lib_name.t
+
+val src_root : t -> Path.t
+val obj_root : t -> Path.t
+
+val package : t -> Package.Name.t option
+
+module DB : sig
+
+  type lib
+  type t
+
+  val create_from_coqlib_stanzas
+    : (Path.t * Dune_file.Coq.t) list
+    -> t
+
+  val find_many
+    :  t
+    -> loc:Loc.t
+    -> Lib_name.t list
+    -> lib list Or_exn.t
+
+  val resolve : t -> Loc.t * Lib_name.t -> lib Or_exn.t
+
+end with type lib := t
diff --git a/src/coq_rules.ml b/src/coq_rules.ml
@@ -26,7 +26,7 @@ type coq_context =
   ; coqpp  : Action.program
   }
 
-let parse_coqdep ~coq_module (lines : string list) =
+let parse_coqdep ~dir ~coq_module (lines : string list) =
   if coq_debug then Format.eprintf "Parsing coqdep @\n%!";
   let source = Coq_module.source coq_module in
   let invalid p =
@@ -45,8 +45,8 @@ let parse_coqdep ~coq_module (lines : string list) =
   | Some (basename,deps) ->
     let ff = List.hd @@ String.extract_blank_separated_words basename in
     let depname, _ = Filename.split_extension ff in
-    let modname =
-      Coq_module.(String.concat ~sep:"/" (prefix coq_module @ [name coq_module])) in
+    let modname = String.concat ~sep:"/" Coq_module.(prefix coq_module @ [name coq_module]) in
+    let modname = Path.(to_string (relative (drop_build_context_exn dir) modname)) in
     if coq_debug
     then Format.eprintf "depname / modname: %s / %s@\n%!" depname modname;
     if depname <> modname then invalid "basename";
@@ -55,8 +55,13 @@ 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
-      ~coq_flags ~ml_iflags ~mlpack_rule coq_module =
+let setup_theory_flag lib =
+  let wrapper = Lib_name.to_string (Coq_lib.name lib) in
+  let dir = Coq_lib.src_root lib in
+  Arg_spec.[A "-Q"; Path dir; A wrapper]
+
+let setup_rule ~expander ~base_dir ~dir ~cc ~source_rule ~wrapper_name
+      ~coq_flags ~theories_libs ~ml_iflags ~mlpack_rule coq_module =
 
   if coq_debug
   then Format.eprintf "gen_rule coq_module: %a@\n%!" Coq_module.pp coq_module;
@@ -66,37 +71,35 @@ let setup_rule ~expander ~dir ~cc ~source_rule ~wrapper_name
   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 th_flags = List.concat_map theories_libs ~f:setup_theory_flag in
+  let file_flags =
+    th_flags @ Arg_spec.[ A "-R"; Path obj_dir; A wrapper_name; ml_iflags; Dep source ] in
+
   let cd_arg : (string list, _) Arg_spec.t list =
-    Arg_spec.[ As ["-dyndep"; "opt"]; iflags; ml_iflags; Dep source ] in
+    Arg_spec.[ As ["-dyndep"; "opt"] ] @ file_flags in
 
   (* coqdep needs the full source + plugin's mlpack to be present :( *)
   let coqdep_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
+    Build.run ~dir:base_dir ~stdout_to cc.coqdep cd_arg
   in
 
   (* Process coqdep and generate rules *)
   let deps_of = Build.dyn_paths (
     Build.lines_of stdout_to >>^
-    parse_coqdep ~coq_module >>^
-    List.map ~f:(Path.relative dir)
+    parse_coqdep ~dir ~coq_module >>^
+    List.map ~f:(Path.relative base_dir)
   ) in
 
-  let cc_arg = Arg_spec.[
-    iflags;
-    ml_iflags;
-    Dep source;
-    Hidden_targets [object_to] ]
-  in
+  let cc_arg = file_flags @ [ Arg_spec.Hidden_targets [object_to] ] in
 
   (* Rules for the files *)
   [coqdep_rule;
    deps_of >>>
    Expander.expand_and_eval_set expander coq_flags ~standard:(Build.return []) >>>
-   Build.run ~dir cc.coqc (Dyn (fun flags -> As flags) :: cc_arg)
+   Build.run ~dir:base_dir cc.coqc (Dyn (fun flags -> As flags) :: cc_arg)
   ]
 
 (* TODO: remove; rgrinberg points out:
@@ -112,14 +115,15 @@ let create_ccoq sctx ~dir =
   }
 
 (* get_libraries from Coq's ML dependencies *)
-let libs_of_coq_deps ~loc ~scope libs =
-  let lib_db = Scope.libs scope in
-  List.concat_map ~f:Dune_file.Lib_dep.to_lib_names libs
-  |> Lib.DB.find_many ~loc lib_db
-  |> Result.ok_exn
+let libs_of_coq_deps ~lib_db =
+  List.concat_map ~f:(fun lib_dep ->
+    let loc = Dune_file.Lib_dep.get_loc lib_dep in
+    Dune_file.Lib_dep.to_lib_names lib_dep
+    |> Lib.DB.find_many lib_db ~loc
+    |> Result.ok_exn)
 
 (* compute include flags and mlpack rules *)
-let setup_ml_deps ~scope ~loc libs =
+let setup_ml_deps ~lib_db libs =
 
   (* coqdep expects an mlpack file next to the sources otherwise it
    * will omit the cmxs deps *)
@@ -134,7 +138,7 @@ let setup_ml_deps ~scope ~loc libs =
 
   (* Pair of include flags and paths to mlpack *)
   let ml_iflags, mlpack =
-    let libs = libs_of_coq_deps ~loc ~scope libs in
+    let libs = libs_of_coq_deps ~lib_db libs in
     Util.include_flags libs, List.concat_map ~f:ml_pack_files libs
   in
 
@@ -144,40 +148,59 @@ let setup_ml_deps ~scope ~loc libs =
 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 coq_modules_of_dep ~sctx lib =
+  let name = Coq_lib.name lib in
+  let dir = Coq_lib.src_root lib in
+  let dir_contents = Dir_contents.get_without_rules sctx ~dir in
+  Dir_contents.coq_modules_of_library dir_contents ~name
 
-  let scope = SC.find_scope_by_dir sctx dir in
+let coq_theories_of_lib_deps ~coq_lib_db =
+  List.concat_map ~f:(fun lib_dep ->
+    let loc = Dune_file.Lib_dep.get_loc lib_dep in
+    Dune_file.Lib_dep.to_lib_names lib_dep
+    |> Coq_lib.DB.find_many coq_lib_db ~loc
+    |> Result.ok_exn)
 
-  if coq_debug then begin
-    let scope = SC.find_scope_by_dir sctx dir in
-    Format.eprintf "[gen_rules] @[dir: %a@\nscope: %a@]@\n%!"
-      Path.pp dir Path.pp (Scope.root scope)
-  end;
+let setup_rules ~sctx ~dir ~dir_contents (s : Dune_file.Coq.t) =
 
   let cc = create_ccoq sctx ~dir in
+  let scope = SC.find_scope_by_dir sctx dir in
+  let lib_db = Scope.libs scope in
+  let coq_lib_db = Scope.coq_libs scope in
+
   let name = Dune_file.Coq.best_name s in
+
   let coq_modules = Dir_contents.coq_modules_of_library dir_contents ~name in
 
+  let theories_libs = coq_theories_of_lib_deps ~coq_lib_db s.theories in
+  let theories_modules =
+    List.concat_map theories_libs ~f:(coq_modules_of_dep ~sctx) in
+
   (* 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
+     dependencies, including those of dependencies *)
+  let source_rule =
+    List.rev_map ~f:Coq_module.source theories_modules
+    |> List.rev_map_append ~f:Coq_module.source coq_modules
+    |> Build.paths 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 ml_iflags, mlpack_rule = setup_ml_deps ~lib_db s.libraries in
+  let base_dir = Scope.root scope in
 
   let coq_rules =
     List.concat_map
-      ~f:(setup_rule ~expander ~dir ~cc ~source_rule ~wrapper_name ~coq_flags
-            ~ml_iflags ~mlpack_rule) coq_modules in
+      ~f:(setup_rule ~expander ~base_dir ~dir ~cc ~source_rule ~wrapper_name ~coq_flags
+            ~theories_libs ~ml_iflags ~mlpack_rule) coq_modules in
   coq_rules
 
 (* This is here for compatibility with Coq < 8.11, which expects
    plugin files to be in the folder containing the `.vo` files *)
 let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Dune_file.Coq.t) =
-  let ml_libs = libs_of_coq_deps ~scope ~loc:s.loc s.libraries in
+  let lib_db = Scope.libs scope in
+  let ml_libs = libs_of_coq_deps ~lib_db s.libraries in
   let rules_for_lib lib =
     (* Don't install libraries that don't belong to this package *)
     if Option.equal Package.Name.equal

diff --git a/src/dune_file.ml b/src/dune_file.ml
@@ -509,6 +509,11 @@ module Lib_dep = struct
   let direct x = Direct x
 
   let of_lib_name (loc, pp) = Direct (loc, pp)
+
+  let get_loc = function
+    | Direct (loc,_) -> loc
+    | Select s -> s.loc
+
 end
 
 module Lib_deps = struct
@@ -1842,6 +1847,8 @@ module Coq = struct
     ; flags      : Ordered_set_lang.Unexpanded.t
     ; libraries  : Lib_dep.t list
     (** ocaml libraries *)
+    ; theories   : Lib_dep.t list
+    (** coq libraries *)
     ; loc        : Loc.t
     ; enabled_if : Blang.t
     }
@@ -1861,18 +1868,22 @@ module Coq = struct
        and+ flags = field_oslu "flags"
        and+ modules = modules_field "modules"
        and+ libraries = field "libraries" Lib_deps.decode ~default:[]
+       and+ theories = field "theories" Lib_deps.decode ~default:[]
        and+ enabled_if = enabled_if
        in
        let name =
          let (loc, res) = name in
-         (loc, Lib_name.Local.validate (loc, res) ~wrapped:None)
+         match res with
+         | Ok t | Warn t -> (loc, t)
+         | Invalid -> Errors.fail loc "%s" Lib_name.Local.invalid_message
        in
        { name
        ; public
        ; synopsis
        ; modules
        ; flags
        ; libraries
+       ; theories
        ; loc
        ; enabled_if
        })

diff --git a/src/dune_file.mli b/src/dune_file.mli
@@ -78,6 +78,7 @@ module Lib_dep : sig
   val to_lib_names : t -> Lib_name.t list
   val direct : Loc.t * Lib_name.t -> t
   val of_lib_name : Loc.t * Lib_name.t -> t
+  val get_loc : t -> Loc.t
 end
 
 module Lib_deps : sig
@@ -363,6 +364,8 @@ module Coq : sig
     ; flags      : Ordered_set_lang.Unexpanded.t
     ; libraries  : Lib_dep.t list
     (** ocaml libraries *)
+    ; theories   : Lib_dep.t list
+    (** coq libraries *)
     ; loc        : Loc.t
     ; enabled_if : Blang.t
     }