Merge pull request #2053 from ejgallego/coq+compose_local

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

CHANGES.md

@@ -13,6 +13,9 @@ Unreleased
 - Delay expansion errors until the rule is used to build something (#3261, fix
   #3252, @rgrinberg, @diml)
 
+- [coq] Support for theory dependencies and compositional builds using
+  new field `(theories ...)` (#2053, @ejgallego, @rgrinberg)
+
 2.4.0 (06/03/2020)
 ------------------
 

doc/dune-files.rst

@@ -1548,7 +1548,8 @@ The basic form for defining Coq libraries is very similar to the OCaml form:
      (synopsis <text>)
      (modules <ordered_set_lang>)
      (libraries <ocaml_libraries>)
-     (flags <coq_flags>))
+     (flags <coq_flags>)
+     (theories <coq_theories>))
 
 The stanza will build all ``.v`` files on the given directory. The semantics of fields is:
 
@@ -1580,6 +1581,15 @@ The stanza will build all ``.v`` files on the given directory. The semantics of
 - 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
   theory to depend on a ML plugin,
+- your Coq theory can depend on other theories by specifying them in
+  the ``<coq_theories>`` field. Dune will then pass to Coq the
+  corresponding flags for everything to compile correctly [ ``-Q``
+  ]. As of today, we only support composition with libraries defined
+  in the same scope (that is to say, under the same ``dune-project``
+  domain). We will lift this restriction in the future. Note that
+  composition with the Coq's standard library is supported, but in
+  this case the ``Coq`` prefix will be made available in a qualified
+  way.
 
 Recursive qualification of modules
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1598,11 +1608,11 @@ Coq style for sub-directories. For example, file ``A/b/C.v`` will be module
 Limitations
 ~~~~~~~~~~~
 
-- composition and scoping of Coq libraries is still not possible. For now,
-  libraries are located using Coq's built-in library management,
-- ``.v`` files 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.
+- ``.v`` files always depend on the native version of Coq / plugins,
+- a ``foo.mlpack`` file must the present in directories of locally
+  defined plugins for things to work, this is a limitation of
+  ``coqdep``, see the template at
+  <https://github.com/ejgallego/coq-plugin-template>
 
 coq.pp
 ------

src/dune/coq_lib.ml

@@ -0,0 +1,144 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(* Written by: Emilio Jesús Gallego Arias *)
+
+open! Stdune
+
+(* At some point we may want to reify this into resolved status, for example:
+
+   ; libraries : Lib.t list Or_exn.t
+
+   etc.. *)
+type t =
+  { name : Loc.t * Coq_lib_name.t
+  ; wrapper : string
+  ; src_root : Path.Build.t
+  ; obj_root : Path.Build.t
+  ; theories : (Loc.t * Coq_lib_name.t) list
+  ; libraries : (Loc.t * Lib_name.t) list
+  ; package : Package.t option
+  }
+
+let name l = snd l.name
+
+let location l = fst l.name
+
+let wrapper l = l.wrapper
+
+let src_root l = l.src_root
+
+let obj_root l = l.obj_root
+
+let libraries l = l.libraries
+
+let package l = l.package
+
+module Error = struct
+  let make ?loc ?hints paragraphs =
+    Error (User_error.E (User_error.make ?loc ?hints paragraphs))
+
+  let duplicate_theory_name theory =
+    let loc, name = theory.Dune_file.Coq.name in
+    let name = Coq_lib_name.to_string name in
+    make ~loc [ Pp.textf "Duplicate theory name: %s" name ]
+
+  let theory_not_found ~loc name =
+    let name = Coq_lib_name.to_string name in
+    make ~loc [ Pp.textf "Theory %s not found" name ]
+
+  let private_deps_not_allowed ~loc private_dep =
+    let name = Coq_lib_name.to_string (name private_dep) in
+    make ~loc
+      [ Pp.textf
+          "Theory %S is private, it cannot be a dependency of a public theory. \
+           You need to associate %S to a package."
+          name name
+      ]
+
+  let duplicate_boot_lib ~loc boot_theory =
+    let name = Coq_lib_name.to_string (snd boot_theory.Dune_file.Coq.name) in
+    make ~loc [ Pp.textf "Cannot have more than one boot library: %s)" name ]
+
+  let cycle_found ~loc cycle =
+    make ~loc
+      [ Pp.textf "Cycle found"
+      ; Pp.enumerate cycle ~f:(fun t ->
+            Pp.text (Coq_lib_name.to_string (snd t.name)))
+      ]
+end
+
+module DB = struct
+  type lib = t
+
+  type nonrec t =
+    { boot : (Loc.t * t) option
+    ; libs : t Coq_lib_name.Map.t
+    }
+
+  let boot_library { boot; _ } = boot
+
+  let create_from_stanza ((dir, s) : Path.Build.t * Dune_file.Coq.t) =
+    let name = snd s.name in
+    ( name
+    , { name = s.name
+      ; wrapper = Coq_lib_name.wrapper name
+      ; obj_root = dir
+      ; src_root = dir
+      ; theories = s.theories
+      ; libraries = s.libraries
+      ; package = s.package
+      } )
+
+  (* Should we register errors and printers, or raise is OK? *)
+  let create_from_coqlib_stanzas sl =
+    let libs =
+      match Coq_lib_name.Map.of_list_map ~f:create_from_stanza sl with
+      | Ok m -> m
+      | Error (_name, _w1, (_, w2)) ->
+        Result.ok_exn (Error.duplicate_theory_name w2)
+    in
+    let boot =
+      match List.find_all ~f:(fun (_, s) -> s.Dune_file.Coq.boot) sl with
+      | [] -> None
+      | [ l ] -> Some ((snd l).loc, snd (create_from_stanza l))
+      | _ :: (_, s2) :: _ ->
+        Result.ok_exn (Error.duplicate_boot_lib ~loc:s2.loc s2)
+    in
+    { boot; libs }
+
+  let resolve ?(allow_private_deps = true) db (loc, name) =
+    match Coq_lib_name.Map.find db.libs name with
+    | Some s ->
+      if (not allow_private_deps) && Option.is_none s.package then
+        Error.private_deps_not_allowed ~loc s
+      else
+        Ok s
+    | None -> Error.theory_not_found ~loc name
+
+  let find_many t ~loc = Result.List.map ~f:(fun name -> resolve t (loc, name))
+
+  module Coq_lib_closure = Top_closure.Make (String.Set) (Or_exn)
+
+  let requires db t : lib list Or_exn.t =
+    let theories =
+      match db.boot with
+      | None -> t.theories
+      (* XXX: Note that this means that we will prefix Coq with -Q, not sure we
+         want to do that (yet), but seems like good practice. *)
+      | Some (loc, stdlib) -> (loc, snd stdlib.name) :: t.theories
+    in
+    let open Result.O in
+    let allow_private_deps = Option.is_none t.package in
+    let* theories =
+      Result.List.map ~f:(resolve ~allow_private_deps db) theories
+    in
+    let key t = Coq_lib_name.to_string (snd t.name) in
+    let deps t =
+      Result.List.map ~f:(resolve ~allow_private_deps db) t.theories
+    in
+    Result.bind (Coq_lib_closure.top_closure theories ~key ~deps) ~f:(function
+      | Ok libs -> Ok libs
+      | Error cycle -> Error.cycle_found ~loc:(location t) cycle)
+
+  let resolve db l = resolve db l
+end

src/dune/coq_lib.mli

@@ -0,0 +1,39 @@
+(* 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 -> Coq_lib_name.t
+
+(* this is not really a wrapper for the prefix path *)
+val wrapper : t -> string
+
+(** ml libraries *)
+val libraries : t -> (Loc.t * Lib_name.t) list
+
+val src_root : t -> Path.Build.t
+
+val obj_root : t -> Path.Build.t
+
+val package : t -> Package.t option
+
+module DB : sig
+  type lib
+
+  type t
+
+  val create_from_coqlib_stanzas : (Path.Build.t * Dune_file.Coq.t) list -> t
+
+  val find_many : t -> loc:Loc.t -> Coq_lib_name.t list -> lib list Or_exn.t
+
+  val boot_library : t -> (Loc.t * lib) option
+
+  val resolve : t -> Loc.t * Coq_lib_name.t -> lib Or_exn.t
+
+  (** Return the list of dependencies needed for compiling this library *)
+  val requires : t -> lib -> lib list Or_exn.t
+end
+with type lib := t

src/dune/coq_lib_name.ml

@@ -12,13 +12,16 @@ let to_string x = String.concat ~sep:"." x
 
 let wrapper x = to_string x
 
+(* We should add some further validation to Coq library names; the rules in Coq
+   itself have been tweaked due to Unicode, etc... so this is not trivial *)
 let decode : (Loc.t * t) Dune_lang.Decoder.t =
   Dune_lang.Decoder.plain_string (fun ~loc s -> (loc, String.split ~on:'.' s))
 
 let encode : t Dune_lang.Encoder.t =
  fun lib -> Dune_lang.Encoder.string (to_string lib)
 
-(* let pp x = Pp.text (to_string x) *)
+let pp x = Pp.text (to_string x)
+
 let to_dyn = Dyn.Encoder.(list string)
 
 module Rep = struct

src/dune/coq_lib_name.mli

@@ -16,7 +16,10 @@ val encode : t Dune_lang.Encoder.t
 val decode : (Loc.t * t) Dune_lang.Decoder.t
 
 (* to be removed in favor of encode / decode *)
-(* val _pp : t -> Pp.t *)
+val to_string : t -> string
+
+val pp : t -> t Pp.t
+
 val to_dyn : t -> Dyn.t
 
 module Map : Map.S with type key = t