[coq] Allow to install Coq native files under a different package.

The code changes doesn't make me super-happy, tho I think that in general it makes sense for stanzas to produce object files that do belong to multiple packages, as for example it is common in some upstream packagers to allow to install debug and doc files into a different package. However this implies that `Dune_file.stanza_package stanza` is not canonical anymore. Likely to model this better, we may need to define the notion of sub-packages of a stanza / package, but awaiting for feedback.
ocaml · Jun 23, 2021 · ba117da · ba117da
1 parent ed195f9
commit ba117da
Show file tree

Hide file tree

Showing 15 changed files with 175 additions and 74 deletions.
diff --git a/src/dune_rules/coq_mode.ml b/src/dune_rules/coq_mode.ml
@@ -11,7 +11,7 @@ type t =
   | VoOnly
   | Native
   | Split of
-      { package : string option
+      { package : Dune_engine.Package.t option
       ; profile : string list
       }
 
@@ -25,7 +25,7 @@ let decode_v04 =
   let open Dune_lang.Decoder in
   let native =
     fields
-      (let+ package = field_o "package" string
+      (let+ package = field_o "package" Stanza_common.Pkg.decode
        and+ profile =
          field ~default:default_profile "profile" (repeat string)
        in

diff --git a/src/dune_rules/coq_mode.mli b/src/dune_rules/coq_mode.mli
@@ -11,7 +11,7 @@ type t =
   | VoOnly
   | Native
   | Split of
-      { package : string option
+      { package : Dune_engine.Package.t option
       ; profile : string list
       }
 

diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml
@@ -597,7 +597,9 @@ let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Theory.t) =
              let dst =
                Path.Local.(to_string (relative dst_dir plugin_file_basename))
              in
-             (Some loc, Install.Entry.make Section.Lib_root ~dst plugin_file))
+             ( package
+             , (Some loc, Install.Entry.make Section.Lib_root ~dst plugin_file)
+             ))
     else
       []
   in
@@ -633,29 +635,37 @@ let install_rules ~sctx ~dir s =
     in
     let to_path f = Path.reach ~from:(Path.build dir) (Path.build f) in
     let to_dst f = Path.Local.to_string @@ Path.Local.relative dst_dir f in
-    let make_entry (orig_file : Path.Build.t) (dst_file : string) =
-      ( Some loc
-      , Install.Entry.make Section.Lib_root ~dst:(to_dst dst_file) orig_file )
+    let make_entry ~package (orig_file : Path.Build.t) (dst_file : string) =
+      ( package
+      , ( Some loc
+        , Install.Entry.make Section.Lib_root ~dst:(to_dst dst_file) orig_file
+        ) )
     in
+    let coq_file_spec_to_entry ~package (vo_file, install_vo_file) =
+      make_entry ~package vo_file install_vo_file
+    in
+
     let wrapper_name = Coq_lib_name.wrapper (snd s.name) in
     let+ coq_sources = Dir_contents.coq dir_contents in
     coq_sources |> Coq_sources.library ~name
     |> List.concat_map ~f:(fun (vfile : Coq_module.t) ->
-           (* FIXME: take into account the package override *)
-           let obj_files =
-             (match mode with
-             | Split _ ->
+           let native_obj_files =
+             match mode with
+             | Split { package = native_package; _ } ->
+               let package = Option.value ~default:package native_package in
                Coq_module.native_obj_files ~wrapper_name ~obj_dir:dir vfile
-             | _ -> [])
-             @ Coq_module.obj_files ~wrapper_name ~mode ~obj_dir:dir
-                 ~obj_files_mode:Coq_module.Install vfile
-             |> List.map
-                  ~f:(fun ((vo_file : Path.Build.t), (install_vo_file : string))
-                     -> make_entry vo_file install_vo_file)
+               |> List.map ~f:(coq_file_spec_to_entry ~package)
+             | _ -> []
+           in
+           let vo_obj_files =
+             Coq_module.obj_files ~wrapper_name ~mode ~obj_dir:dir
+               ~obj_files_mode:Coq_module.Install vfile
+             |> List.map ~f:(coq_file_spec_to_entry ~package)
            in
            let vfile = Coq_module.source vfile in
            let vfile_dst = to_path vfile in
-           make_entry vfile vfile_dst :: obj_files)
+           let source_entry = make_entry ~package vfile vfile_dst in
+           source_entry :: vo_obj_files @ native_obj_files)
     |> List.rev_append coq_plugins_install_rules
 
 let coqpp_rules ~sctx ~dir (s : Coqpp.t) =

diff --git a/src/dune_rules/coq_rules.mli b/src/dune_rules/coq_rules.mli
@@ -17,11 +17,14 @@ val setup_rules :
   -> Theory.t
   -> Action.t Action_builder.With_targets.t list Memo.Build.t
 
+(* We allos to override the install package for some files, for example, those
+   coming from the Coq native compiler *)
 val install_rules :
      sctx:Super_context.t
   -> dir:Path.Build.t
   -> Theory.t
-  -> (Loc.t option * Path.Build.t Install.Entry.t) list Memo.Build.t
+  -> (Package.t * (Loc.t option * Path.Build.t Install.Entry.t)) list
+     Memo.Build.t
 
 val coqpp_rules :
      sctx:Super_context.t

diff --git a/src/dune_rules/install_rules.ml b/src/dune_rules/install_rules.ml
@@ -249,40 +249,59 @@ end = struct
     List.exists [ "README"; "LICENSE"; "CHANGE"; "HISTORY" ] ~f:(fun prefix ->
         String.is_prefix fn ~prefix)
 
-  let stanza_to_entries ~sctx ~scope ~dir ~expander stanza =
-    match (stanza : Stanza.t) with
-    | Dune_file.Install i
-    | Dune_file.Executables { install_conf = Some i; _ } ->
-      let path_expander =
-        File_binding.Unexpanded.expand ~dir
-          ~f:(Expander.No_deps.expand_str expander)
-      in
-      let section = i.section in
-      Memo.Build.List.map i.files ~f:(fun unexpanded ->
-          let+ fb = path_expander unexpanded in
-          let loc = File_binding.Expanded.src_loc fb in
-          let src = File_binding.Expanded.src fb in
-          let dst = File_binding.Expanded.dst fb in
-          ( Some loc
-          , Install.Entry.make_with_site section
-              (Super_context.get_site_of_packages sctx)
-              src ?dst ))
-    | Dune_file.Library lib ->
-      let sub_dir = Dune_file.Library.sub_dir lib in
-      let* dir_contents = Dir_contents.get sctx ~dir in
-      lib_install_files sctx ~scope ~dir ~sub_dir lib ~dir_contents
-    | Coq_stanza.Theory.T coqlib -> Coq_rules.install_rules ~sctx ~dir coqlib
-    | Dune_file.Documentation d ->
-      let* dc = Dir_contents.get sctx ~dir in
-      let+ mlds = Dir_contents.mlds dc d in
-      List.map mlds ~f:(fun mld ->
-          ( None
-          , Install.Entry.make
-              ~dst:(sprintf "odoc-pages/%s" (Path.Build.basename mld))
-              Section.Doc mld ))
-    | Dune_file.Plugin t ->
-      Memo.Build.return (Plugin_rules.install_rules ~sctx ~dir t)
-    | _ -> Memo.Build.return []
+  let stanza_to_entries ~sctx ~scope ~dir ~expander stanza :
+      (Package.Name.t * _) list Memo.Build.t =
+    let* stanza_and_package =
+      let+ stanza = keep_if expander stanza ~scope in
+      let open Option.O in
+      let* stanza = stanza in
+      let+ package = Dune_file.stanza_package stanza in
+      (stanza, package)
+    in
+    match stanza_and_package with
+    | None -> Memo.Build.return []
+    | Some (stanza, package) -> (
+      let name = Package.name package in
+      match (stanza : Stanza.t) with
+      | Dune_file.Install i
+      | Dune_file.Executables { install_conf = Some i; _ } ->
+        let path_expander =
+          File_binding.Unexpanded.expand ~dir
+            ~f:(Expander.No_deps.expand_str expander)
+        in
+        let section = i.section in
+        Memo.Build.List.map i.files ~f:(fun unexpanded ->
+            let+ fb = path_expander unexpanded in
+            let loc = File_binding.Expanded.src_loc fb in
+            let src = File_binding.Expanded.src fb in
+            let dst = File_binding.Expanded.dst fb in
+            ( name
+            , ( Some loc
+              , Install.Entry.make_with_site section
+                  (Super_context.get_site_of_packages sctx)
+                  src ?dst ) ))
+      | Dune_file.Library lib ->
+        let sub_dir = Dune_file.Library.sub_dir lib in
+        let* dir_contents = Dir_contents.get sctx ~dir in
+        lib_install_files sctx ~scope ~dir ~sub_dir lib ~dir_contents
+        >>| List.map ~f:(fun entry -> (name, entry))
+      | Coq_stanza.Theory.T coqlib ->
+        Coq_rules.install_rules ~sctx ~dir coqlib
+        >>| List.map ~f:(fun (pkg, entry) -> (Package.name pkg, entry))
+      | Dune_file.Documentation d ->
+        let* dc = Dir_contents.get sctx ~dir in
+        let+ mlds = Dir_contents.mlds dc d in
+        List.map mlds ~f:(fun mld ->
+            ( name
+            , ( None
+              , Install.Entry.make
+                  ~dst:(sprintf "odoc-pages/%s" (Path.Build.basename mld))
+                  Section.Doc mld ) ))
+      | Dune_file.Plugin t ->
+        Plugin_rules.install_rules ~sctx ~dir t
+        |> List.map ~f:(fun entry -> (name, entry))
+        |> Memo.Build.return
+      | _ -> Memo.Build.return [])
 
   let stanzas_to_entries sctx =
     let ctx = Super_context.context sctx in
@@ -344,31 +363,14 @@ end = struct
           let named_entries =
             let { Dir_with_dune.ctx_dir = dir; scope; _ } = d in
             let* expander = Super_context.expander sctx ~dir in
-            let* stanza_and_package =
-              let+ stanza = keep_if expander stanza ~scope in
-              let open Option.O in
-              let* stanza = stanza in
-              let+ package = Dune_file.stanza_package stanza in
-              (stanza, package)
-            in
-            match stanza_and_package with
-            | None -> Memo.Build.return None
-            | Some (stanza, package) ->
-              let new_entries =
-                stanza_to_entries ~sctx ~dir ~scope ~expander stanza
-              in
-              let name = Package.name package in
-              let+ entries = new_entries in
-              Some (name, entries)
+            stanza_to_entries ~sctx ~dir ~scope ~expander stanza
           in
           named_entries :: acc)
       |> Memo.Build.parallel_map ~f:Fun.id
+      |> Memo.Build.map ~f:List.concat
     in
-    List.fold_left l ~init ~f:(fun acc named_entries ->
-        match named_entries with
-        | None -> acc
-        | Some (name, entries) ->
-          Package.Name.Map.Multi.add_all acc name entries)
+    List.fold_left l ~init ~f:(fun acc (name, entry) ->
+        Package.Name.Map.Multi.add_all acc name [ entry ])
     |> Package.Name.Map.map ~f:(fun entries ->
            (* Sort entries so that the ordering in [dune-package] is independent
               of Dune's current implementation. *)

diff --git a/test/blackbox-tests/test-cases/coq/native-split-package.t/bar/bar.v b/test/blackbox-tests/test-cases/coq/native-split-package.t/bar/bar.v
@@ -0,0 +1,3 @@
+From foo Require Import foo.
+
+Definition mynum (i : mynat) := 3.
diff --git a/test/blackbox-tests/test-cases/coq/native-split-package.t/bar/dune b/test/blackbox-tests/test-cases/coq/native-split-package.t/bar/dune
@@ -0,0 +1,9 @@
+(coq.theory
+ (name bar)
+ (package base)
+ (mode
+  (native
+   (package base-native)))
+ (theories foo)
+ (modules :standard)
+ (synopsis "Test Coq library"))
diff --git a/test/blackbox-tests/test-cases/coq/native-split-package.t/baz/a/a.v b/test/blackbox-tests/test-cases/coq/native-split-package.t/baz/a/a.v
@@ -0,0 +1 @@
+Definition aa := 4.
diff --git a/test/blackbox-tests/test-cases/coq/native-split-package.t/baz/b/uu.v b/test/blackbox-tests/test-cases/coq/native-split-package.t/baz/b/uu.v
@@ -0,0 +1 @@
+Definition uu := 5.
diff --git a/test/blackbox-tests/test-cases/coq/native-split-package.t/baz/dune b/test/blackbox-tests/test-cases/coq/native-split-package.t/baz/dune
@@ -0,0 +1,6 @@
+(coq.theory
+ (name moo.baz)
+ (package base)
+ (theories foo bar))
+
+(include_subdirs qualified)
diff --git a/test/blackbox-tests/test-cases/coq/native-split-package.t/dune b/test/blackbox-tests/test-cases/coq/native-split-package.t/dune
@@ -0,0 +1,6 @@
+(rule
+ (alias default)
+ (action
+  (progn
+   (echo "%{read:base.install}")
+   (echo "%{read:base-native.install}"))))
diff --git a/test/blackbox-tests/test-cases/coq/native-split-package.t/dune-project b/test/blackbox-tests/test-cases/coq/native-split-package.t/dune-project
@@ -0,0 +1,10 @@
+(lang dune 3.0)
+(using coq 0.4)
+
+(package
+ (name base))
+
+(package
+ (name base-native)
+ (depends
+  (base (= :version))))
diff --git a/test/blackbox-tests/test-cases/coq/native-split-package.t/foo/dune b/test/blackbox-tests/test-cases/coq/native-split-package.t/foo/dune
@@ -0,0 +1,6 @@
+(coq.theory
+ (name foo)
+ (package base)
+ (mode native)
+ (modules :standard)
+ (synopsis "Test Coq library"))
diff --git a/test/blackbox-tests/test-cases/coq/native-split-package.t/foo/foo.v b/test/blackbox-tests/test-cases/coq/native-split-package.t/foo/foo.v
@@ -0,0 +1 @@
+Definition mynat := nat.
diff --git a/test/blackbox-tests/test-cases/coq/native-split-package.t/run.t b/test/blackbox-tests/test-cases/coq/native-split-package.t/run.t
@@ -0,0 +1,43 @@
+  $ dune build --profile=release --display short --debug-dependency-path @all
+        coqdep bar/bar.v.d
+        coqdep foo/foo.v.d
+        coqdep baz/a/a.v.d
+        coqdep baz/b/uu.v.d
+          coqc foo/.foo.aux,foo/foo.{glob,vo}
+          coqc baz/a/.a.aux,baz/a/a.{glob,vo}
+          coqc baz/b/.uu.aux,baz/b/uu.{glob,vo}
+     coqnative foo/Nfoo_foo.{cmi,cmxs}
+          coqc bar/.bar.aux,bar/bar.{glob,vo}
+     coqnative baz/a/Nmoo_baz_a_a.{cmi,cmxs}
+     coqnative baz/b/Nmoo_baz_b_uu.{cmi,cmxs}
+     coqnative bar/Nbar_bar.{cmi,cmxs}
+
+  $ dune build --profile=release --debug-dependency-path @default
+  lib: [
+    "_build/install/default/lib/base/META"
+    "_build/install/default/lib/base/dune-package"
+  ]
+  lib_root: [
+    "_build/install/default/lib/coq/user-contrib/bar/bar.v" {"coq/user-contrib/bar/bar.v"}
+    "_build/install/default/lib/coq/user-contrib/bar/bar.vo" {"coq/user-contrib/bar/bar.vo"}
+    "_build/install/default/lib/coq/user-contrib/foo/.coq-native/Nfoo_foo.cmi" {"coq/user-contrib/foo/.coq-native/Nfoo_foo.cmi"}
+    "_build/install/default/lib/coq/user-contrib/foo/.coq-native/Nfoo_foo.cmxs" {"coq/user-contrib/foo/.coq-native/Nfoo_foo.cmxs"}
+    "_build/install/default/lib/coq/user-contrib/foo/foo.v" {"coq/user-contrib/foo/foo.v"}
+    "_build/install/default/lib/coq/user-contrib/foo/foo.vo" {"coq/user-contrib/foo/foo.vo"}
+    "_build/install/default/lib/coq/user-contrib/moo/baz/a/.coq-native/Nmoo_baz_a_a.cmi" {"coq/user-contrib/moo/baz/a/.coq-native/Nmoo_baz_a_a.cmi"}
+    "_build/install/default/lib/coq/user-contrib/moo/baz/a/.coq-native/Nmoo_baz_a_a.cmxs" {"coq/user-contrib/moo/baz/a/.coq-native/Nmoo_baz_a_a.cmxs"}
+    "_build/install/default/lib/coq/user-contrib/moo/baz/a/a.v" {"coq/user-contrib/moo/baz/a/a.v"}
+    "_build/install/default/lib/coq/user-contrib/moo/baz/a/a.vo" {"coq/user-contrib/moo/baz/a/a.vo"}
+    "_build/install/default/lib/coq/user-contrib/moo/baz/b/.coq-native/Nmoo_baz_b_uu.cmi" {"coq/user-contrib/moo/baz/b/.coq-native/Nmoo_baz_b_uu.cmi"}
+    "_build/install/default/lib/coq/user-contrib/moo/baz/b/.coq-native/Nmoo_baz_b_uu.cmxs" {"coq/user-contrib/moo/baz/b/.coq-native/Nmoo_baz_b_uu.cmxs"}
+    "_build/install/default/lib/coq/user-contrib/moo/baz/b/uu.v" {"coq/user-contrib/moo/baz/b/uu.v"}
+    "_build/install/default/lib/coq/user-contrib/moo/baz/b/uu.vo" {"coq/user-contrib/moo/baz/b/uu.vo"}
+  ]
+  lib: [
+    "_build/install/default/lib/base-native/META"
+    "_build/install/default/lib/base-native/dune-package"
+  ]
+  lib_root: [
+    "_build/install/default/lib/coq/user-contrib/bar/.coq-native/Nbar_bar.cmi" {"coq/user-contrib/bar/.coq-native/Nbar_bar.cmi"}
+    "_build/install/default/lib/coq/user-contrib/bar/.coq-native/Nbar_bar.cmxs" {"coq/user-contrib/bar/.coq-native/Nbar_bar.cmxs"}
+  ]
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		From foo Require Import foo.

		Definition mynum (i : mynat) := 3.