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

We support simple composition of Coq libraries using the
 `(theories ...)` field. The main changes are:

- Coq libraries now have a `Coq_lib.t` type

- Stanza scanning does now initialize a `Coq_lib.DB`, per
  scope. Supporting inter-scope public libraries is left for a future
  PR.

- We properly compose when the stdlib is in scope, this allows to have
  a compositional build with Coq itself; note that as of today, in a
  composed build the stdlib prefix `Coq` is introduced qualified; this
  reflects upstream roadmap of deprecating implicit libs. See comment
  in `Scope.public_libs`

We have added tests for:

 - simple composition
 - composition with plugin
 - cyclic composition
 - boot composition [disabled until Coq 8.12 is released]
 - inter-scope composition [fails for now]

We leave for future work:

- Allow to depend on theories in a different scope
- Allow to depend on theories installed globally, likely this will
  require the 2.0 version of the Coq language
- Validation of Coq library names should be improved [clarify upstream
  rules]

Includes changes by Rudi Grinberg [many suggestions] and Théo
Zimmerman [documentation review]

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

CHANGES.md

@@ -1,3 +1,9 @@
+unreleased
+----------
+
+- [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,124 @@
+(* 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 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 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) ->
+        let loc = (snd w2).loc in
+        User_error.raise ~loc
+          [ Pp.textf "Duplicate theory name: %s" (Coq_lib_name.to_string name) ]
+    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) :: _ ->
+        User_error.raise ~loc:s2.loc
+          [ Pp.textf "Cannot have more than one boot library: %s)"
+              (Coq_lib_name.to_string (snd s2.name))
+          ]
+    in
+    { boot; libs }
+
+  let resolve db (loc, name) =
+    match Coq_lib_name.Map.find db.libs name with
+    | None ->
+      Error
+        User_error.(
+          E
+            (make ~loc
+               [ Pp.textf "Theory %s not found" (Coq_lib_name.to_string name) ]))
+    | Some s -> Ok s
+
+  let find_many t ~loc = Result.List.map ~f:(fun name -> resolve t (loc, name))
+
+  (* Where should we move this? *)
+  module Result_monad : Monad_intf.S with type 'a t = ('a, exn) Result.t =
+  struct
+    type 'a t = ('a, exn) Result.t
+
+    let return x = Ok x
+
+    let ( >>= ) = Result.O.( >>= )
+  end
+
+  module Coq_lib_closure = Top_closure.Make (String.Set) (Result_monad)
+
+  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* theories = Result.List.map ~f:(resolve db) theories in
+    let key t = Coq_lib_name.to_string (snd t.name) in
+    let deps t = Result.List.map ~f:(resolve db) t.theories in
+    Result.bind (Coq_lib_closure.top_closure theories ~key ~deps) ~f:(function
+      | Ok libs -> Ok libs
+      | Error cycle ->
+        let msg =
+          [ Pp.textf "Cycle found"
+          ; Pp.enumerate cycle ~f:(fun t ->
+                Pp.text (Coq_lib_name.to_string (snd t.name)))
+          ]
+        in
+        Error User_error.(E (make ~loc:(fst t.name) msg)))
+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 fmt x = Fmt.text fmt (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 Fmt.t
+
 val to_dyn : t -> Dyn.t
 
 module Map : Map.S with type key = t