Introduce a [coq.extraction] stanza

CHANGES.md

@@ -38,6 +38,9 @@ Unreleased
 
 - Allow per-package `version` in generated `opam` files (#3287, @toots)
 
+- [coq] Introduce the `coq.extraction` stanza. It can be used to extract OCaml
+  sources (#3299, fixes #2178, @rgrinberg)
+
 2.4.0 (06/03/2020)
 ------------------
 

doc/dune-files.rst

@@ -1635,6 +1635,31 @@ which for each ``g_mod`` in ``<mlg_list>`` is equivalent to:
      (deps (:mlg-file g_mod.mlg))
      (action (run coqpp %{mlg-file})))
 
+coq.extraction
+--------------
+
+Coq may be instructed to *extract* OCaml sources as part of the compilation
+process. This is done using the ``coq.extraction`` stanza:
+
+.. code:: lisp
+
+   (coq.extraction
+    (prelude <name>)
+    (extracted_modules <names>)
+    <optional-fields>)
+
+- ``(prelude <name>)`` refers to the coq source that contains the extraction
+  commands.
+
+- ``(extraced_modules <names>)`` is an exhaustive list of OCaml modules
+  extracted.
+
+- ``<optional-fields>`` are ``flags``, ``theories``, and ``libraries``. All of
+  these fields have the same meaning as in the ``coq.theory`` stanza.
+
+The extracted sources can then be used in ``executable`` or ``library`` stanzas
+as any other sources.
+
 .. _dune-workspace:
 
 mdx (since 2.4)

src/dune/build.ml

@@ -168,6 +168,8 @@ module With_targets = struct
     ; targets : Path.Build.Set.t
     }
 
+  let map_build t ~f = { t with build = f t.build }
+
   let return x = { build = Pure x; targets = Path.Build.Set.empty }
 
   let add t ~targets =

src/dune/build.mli

@@ -6,11 +6,15 @@ open! Import
 type 'a t
 
 module With_targets : sig
+  type 'a build
+
   type nonrec 'a t =
     { build : 'a t
     ; targets : Path.Build.Set.t
     }
 
+  val map_build : 'a t -> f:('a build -> 'b build) -> 'b t
+
   val return : 'a -> 'a t
 
   val add : 'a t -> targets:Path.Build.t list -> 'a t
@@ -38,6 +42,7 @@ module With_targets : sig
     val ( and+ ) : 'a t -> 'b t -> ('a * 'b) t
   end
 end
+with type 'a build := 'a t
 
 (** This function should be called before analysing build expressions using
     [static_deps], [lib_deps] or [exec], which all require some file system

src/dune/coq_lib.ml

@@ -38,7 +38,7 @@ module Error = struct
     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 loc, name = theory.Coq_stanza.Theory.name in
     let name = Coq_lib_name.to_string name in
     make ~loc [ Pp.textf "Duplicate theory name: %s" name ]
 
@@ -56,7 +56,9 @@ module Error = struct
       ]
 
   let duplicate_boot_lib ~loc boot_theory =
-    let name = Coq_lib_name.to_string (snd boot_theory.Dune_file.Coq.name) in
+    let name =
+      Coq_lib_name.to_string (snd boot_theory.Coq_stanza.Theory.name)
+    in
     make ~loc [ Pp.textf "Cannot have more than one boot library: %s)" name ]
 
   let cycle_found ~loc cycle =
@@ -77,15 +79,15 @@ module DB = struct
 
   let boot_library { boot; _ } = boot
 
-  let create_from_stanza ((dir, s) : Path.Build.t * Dune_file.Coq.t) =
+  let create_from_stanza ((dir, s) : Path.Build.t * Coq_stanza.Theory.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
+      ; theories = s.buildable.theories
+      ; libraries = s.buildable.libraries
       ; package = s.package
       } )
 
@@ -98,11 +100,11 @@ module DB = struct
         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
+      match List.find_all ~f:(fun (_, s) -> s.Coq_stanza.Theory.boot) sl with
       | [] -> None
-      | [ l ] -> Some ((snd l).loc, snd (create_from_stanza l))
+      | [ l ] -> Some ((snd l).buildable.loc, snd (create_from_stanza l))
       | _ :: (_, s2) :: _ ->
-        Result.ok_exn (Error.duplicate_boot_lib ~loc:s2.loc s2)
+        Result.ok_exn (Error.duplicate_boot_lib ~loc:s2.buildable.loc s2)
     in
     { boot; libs }
 
@@ -119,26 +121,41 @@ module DB = struct
 
   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 add_boot db theories =
+    match db.boot with
+    | None -> 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) :: theories
+
+  let top_closure db theories ~allow_private_deps ~loc =
     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
+      add_boot db theories
+      |> Result.List.map ~f:(resolve ~allow_private_deps db)
     in
-    let key t = Coq_lib_name.to_string (snd t.name) in
-    let deps t =
+    let key (t : lib) = Coq_lib_name.to_string (snd t.name) in
+    let deps (t : lib) =
       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)
+    match Coq_lib_closure.top_closure theories ~key ~deps with
+    | Ok (Ok s) -> Ok s
+    | Ok (Error cycle) -> Error.cycle_found ~loc cycle
+    | Error exn -> Error exn
+
+  let requires db (t : lib) : lib list Or_exn.t =
+    let allow_private_deps = Option.is_none t.package in
+    let loc = location t in
+    top_closure db t.theories ~loc ~allow_private_deps
+
+  let requires_for_user_written db = function
+    | [] -> Ok []
+    | start :: xs as theories ->
+      let loc =
+        let stop = Option.value (List.last xs) ~default:start in
+        Loc.span (fst start) (fst stop)
+      in
+      top_closure db theories ~loc ~allow_private_deps:true
 
   let resolve db l = resolve db l
 end

src/dune/coq_lib.mli

@@ -25,7 +25,8 @@ module DB : sig
 
   type t
 
-  val create_from_coqlib_stanzas : (Path.Build.t * Dune_file.Coq.t) list -> t
+  val create_from_coqlib_stanzas :
+    (Path.Build.t * Coq_stanza.Theory.t) list -> t
 
   val find_many : t -> loc:Loc.t -> Coq_lib_name.t list -> lib list Or_exn.t
 
@@ -35,5 +36,8 @@ module DB : sig
 
   (** Return the list of dependencies needed for compiling this library *)
   val requires : t -> lib -> lib list Or_exn.t
+
+  val requires_for_user_written :
+    t -> (Loc.t * Coq_lib_name.t) list -> lib list Or_exn.t
 end
 with type lib := t

src/dune/coq_module.ml

@@ -11,7 +11,11 @@ module Name = struct
 
   let compare = String.compare
 
+  let equal = String.equal
+
   let to_dyn s = Dyn.String s
+
+  let to_string s = s
 end
 
 (* We keep prefix and name separated as the handling of `From Foo Require Bar.`

src/dune/coq_module.mli

@@ -11,7 +11,11 @@ module Name : sig
 
   val compare : t -> t -> Ordering.t
 
+  val equal : t -> t -> bool
+
   val to_dyn : t -> Dyn.t
+
+  val to_string : t -> string
 end
 
 type t
@@ -30,7 +34,7 @@ val source : t -> Path.Build.t
 
 val prefix : t -> string list
 
-val name : t -> string
+val name : t -> Name.t
 
 val dep_file : obj_dir:Path.Build.t -> t -> Path.Build.t