[coq] Add support for native-mode compilation.

We add a `(mode ...)` field to the `(coq.theory ...)` stanza that when
set to `native` will have the Coq compiler to generate and install
"native" objects, that is to say, `.cmxs` libraries containing an
ML-level version of the corresponding Coq module.

As of today, Coq itself does call the `ocamlfind ocaml` to compile the
object files, this restriction may be lifted in the future however it
is not easy as tactics do have access to "Just-In-Time" native
compilation too.

The patch itself is straightforward, except for a hack to handle
native compilation targets. By default, `coqc -native-compute on` will
generate the OCaml-level objects files under `.coq-native/`, and the
regular `.vo` object in the build dir. This scheme doesn't work well
with the restriction than a rule can only produce targets in the same
directory.

We workaround that by passing a special flag to Coq so `.coq-native`
is dropped from the output path; at install time we do set the rules
up so indeed the objects will be installed under `.coq-native` for
compatibility.

TODO:

- update doc
- disable on dev profile

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

src/dune/coq_lib.ml

@@ -1,5 +1,6 @@
 (* This file is licensed under The MIT License *)
 (* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
 open! Stdune

src/dune/coq_lib_name.mli

@@ -1,5 +1,6 @@
 (* This file is licensed under The MIT License *)
 (* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
 open! Stdune

src/dune/coq_module.ml

@@ -33,13 +33,34 @@ let name x = x.name
 let build_vo_dir ~obj_dir x =
   List.fold_left x.prefix ~init:obj_dir ~f:Path.Build.relative
 
+let cmxs_of_mod ~wrapper_name x =
+  let native_base =
+    "N" ^ String.concat ~sep:"_" ((wrapper_name :: x.prefix) @ [ x.name ])
+  in
+  [ native_base ^ ".cmi"; native_base ^ ".cmxs" ]
+
 let dep_file ~obj_dir x =
   let vo_dir = build_vo_dir ~obj_dir x in
   Path.Build.relative vo_dir (x.name ^ ".v.d")
 
-let obj_file ~obj_dir x =
+(* XXX: Remove the install .coq-native hack once rules can output targets in
+   multiple subdirs *)
+let obj_files ~wrapper_name ~mode ~obj_dir x =
   let vo_dir = build_vo_dir ~obj_dir x in
-  Path.Build.relative vo_dir (x.name ^ ".vo")
+  let install_vo_dir = String.concat ~sep:"/" x.prefix in
+  let native_objs =
+    match mode with
+    | Dune_file.Coq.Mode.Native ->
+      let cmxs_obj = cmxs_of_mod ~wrapper_name x in
+      List.map
+        ~f:(fun x ->
+          (Path.Build.relative vo_dir x, install_vo_dir ^ "/.coq_native/" ^ x))
+        cmxs_obj
+    | VoOnly -> []
+  in
+  let name = x.name ^ ".vo" in
+  (Path.Build.relative vo_dir name, Filename.concat install_vo_dir name)
+  :: native_objs
 
 let to_dyn { source; prefix; name } =
   let open Dyn.Encoder in

src/dune/coq_module.mli

@@ -34,7 +34,14 @@ val name : t -> string
 
 val dep_file : obj_dir:Path.Build.t -> t -> Path.Build.t
 
-val obj_file : obj_dir:Path.Build.t -> t -> Path.Build.t
+(** This returns a list of pairs [(obj_file, install_path)] due to native files
+    having a different install location *)
+val obj_files :
+     wrapper_name:string
+  -> mode:Dune_file.Coq.Mode.t
+  -> obj_dir:Path.Build.t
+  -> t
+  -> (Path.Build.t * string) list
 
 val to_dyn : t -> Dyn.t
 

src/dune/coq_rules.ml

@@ -17,6 +17,13 @@ module Util = struct
         let src_dir = Lib_info.src_dir info in
         Path.Set.add acc src_dir)
 
+  let native_paths ts =
+    List.fold_left ts ~init:Path.Set.empty ~f:(fun acc t ->
+        let info = Lib.info t in
+        (* We want the cmi files *)
+        let obj_dir = Obj_dir.public_cmi_dir (Lib_info.obj_dir info) in
+        Path.Set.add acc obj_dir)
+
   let include_flags ts = include_paths ts |> Lib.L.to_iflags
 
   (* coqdep expects an mlpack file next to the sources otherwise it
@@ -148,12 +155,33 @@ let coqdep_rule ~dir ~coqdep ~mlpack_rule ~source_rule ~file_flags coq_module =
   >>> Build.with_no_targets source_rule
   >>> Command.run ~dir ~stdout_to coqdep file_flags
 
-let coqc_rule ~build_dir ~expander ~dir ~coqc ~coq_flags ~file_flags coq_module
-    =
+let coqc_rule ~build_dir ~expander ~dir ~coqc ~coq_flags ~file_flags
+    ~wrapper_name ~native_includes ~mode coq_module =
   let source = Coq_module.source coq_module in
+  let obj_dir = dir in
   let file_flags =
-    let object_to = Coq_module.obj_file ~obj_dir:dir coq_module in
-    [ Command.Args.Hidden_targets [ object_to ]
+    let objects_to =
+      Coq_module.obj_files ~obj_dir ~wrapper_name ~mode coq_module
+      |> List.map ~f:fst
+    in
+    let native_flags =
+      match mode with
+      | Dune_file.Coq.Mode.VoOnly -> file_flags
+      | Native ->
+        let native_includes =
+          Path.Set.fold
+            (Result.ok_exn native_includes)
+            ~f:(fun dir acc -> Command.Args.Path dir :: A "-nI" :: acc)
+            ~init:[]
+        in
+        [ Command.Args.A "-native-output-dir"
+        ; Command.Args.Path (Path.build obj_dir)
+        ; Command.Args.As [ "-native-compiler"; "on" ]
+        ; Command.Args.S (List.rev native_includes)
+        ]
+    in
+    [ Command.Args.Hidden_targets objects_to
+    ; S native_flags
     ; S file_flags
     ; Command.Args.Dep (Path.build source)
     ]
@@ -171,7 +199,8 @@ let coqc_rule ~build_dir ~expander ~dir ~coqc ~coq_flags ~file_flags coq_module
   Command.run ~dir coqc (Command.Args.dyn coq_flags :: file_flags)
 
 let setup_rule ~build_dir ~dir ~cc ~wrapper_name ~file_flags ~expander
-    ~coq_flags ~source_rule ~mlpack_rule ~boot_lib coq_module =
+    ~coq_flags ~mode ~source_rule ~native_includes ~mlpack_rule ~boot_lib
+    coq_module =
   let open Build.With_targets.O in
   if coq_debug then
     Format.eprintf "gen_rule coq_module: %a@\n%!" Pp.render_ignore_tags
@@ -194,7 +223,7 @@ let setup_rule ~build_dir ~dir ~cc ~wrapper_name ~file_flags ~expander
   [ coqdep_rule
   ; Build.with_no_targets deps_of
     >>> coqc_rule ~build_dir ~expander ~dir ~coqc:cc.coqc ~coq_flags ~file_flags
-          coq_module
+          ~wrapper_name ~mode ~native_includes coq_module
   ]
 
 (* TODO: remove; rgrinberg points out: - resolve program is actually cached, -
@@ -279,6 +308,11 @@ let setup_rules ~sctx ~build_dir ~dir ~dir_contents (s : Dune_file.Coq.t) =
 
   let boot_lib = Coq_lib.DB.boot_library coq_lib_db in
   let coq_flags = s.flags in
+  let mode = snd s.mode in
+  let native_includes =
+    Lib.DB.resolve lib_db (Loc.none, Lib_name.of_string "coq.kernel")
+    |> Result.map ~f:(fun lib -> Util.native_paths [ lib ])
+  in
 
   (* List of modules to compile for this library *)
   let coq_modules =
@@ -289,7 +323,8 @@ let setup_rules ~sctx ~build_dir ~dir ~dir_contents (s : Dune_file.Coq.t) =
   List.concat_map
     ~f:
       (setup_rule ~build_dir ~dir ~cc ~expander ~coq_flags ~source_rule
-         ~wrapper_name ~file_flags ~mlpack_rule ~boot_lib)
+         ~wrapper_name ~file_flags ~mode ~native_includes ~mlpack_rule
+         ~boot_lib)
     coq_modules
 
 (******************************************************************************)
@@ -325,7 +360,7 @@ let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Dune_file.Coq.t) =
 let install_rules ~sctx ~dir s =
   match s with
   | { Dune_file.Coq.package = None; _ } -> []
-  | { Dune_file.Coq.package = Some package; _ } ->
+  | { Dune_file.Coq.package = Some package; mode; _ } ->
     let scope = SC.find_scope_by_dir sctx dir in
     let dir_contents = Dir_contents.get sctx ~dir in
     let name = snd s.name in
@@ -348,18 +383,18 @@ let install_rules ~sctx ~dir s =
       else
         coq_plugins_install_rules ~scope ~package ~dst_dir s
     in
+    let wrapper_name = dst_suffix in
+    let mode = snd mode in
     Dir_contents.coq dir_contents
     |> Coq_sources.library ~name
-    |> List.map ~f:(fun (vfile : Coq_module.t) ->
-           let vofile = Coq_module.obj_file ~obj_dir:dir vfile in
-           let vofile_rel =
-             Path.reach ~from:(Path.build dir) (Path.build vofile)
-           in
-           let dst = Path.Local.relative dst_dir vofile_rel in
-           ( None
-           , Install.(
-               Entry.make Section.Lib_root ~dst:(Path.Local.to_string dst)
-                 vofile) ))
+    |> List.concat_map ~f:(fun (vfile : Coq_module.t) ->
+           Coq_module.obj_files ~wrapper_name ~mode ~obj_dir:dir vfile
+           |> List.map ~f:(fun (vo_file, install_vo_file) ->
+                  let dst = Path.Local.relative dst_dir install_vo_file in
+                  ( None
+                  , Install.(
+                      Entry.make Section.Lib_root
+                        ~dst:(Path.Local.to_string dst) vo_file) )))
     |> List.rev_append coq_plugins_install_rules
 
 let coqpp_rules ~sctx ~build_dir ~dir (s : Dune_file.Coqpp.t) =

src/dune/coq_rules.mli

@@ -1,5 +1,6 @@
 (* This file is licensed under The MIT License *)
 (* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
 (* Build rules for Coq's .v -> .vo files *)

src/dune/dune_file.ml

@@ -1976,13 +1976,22 @@ module Coqpp = struct
 end
 
 module Coq = struct
+  module Mode = struct
+    type t =
+      | VoOnly
+      | Native
+
+    let decode = Dune_lang.Decoder.(enum [ ("vo", VoOnly); ("native", Native) ])
+  end
+
   type t =
     { name : Loc.t * Coq_lib_name.t
     ; package : Package.t option
     ; project : Dune_project.t
     ; synopsis : string option
     ; modules : Ordered_set_lang.t
     ; flags : Ordered_set_lang.Unexpanded.t
+    ; mode : Loc.t * Mode.t
     ; boot : bool
     ; libraries : (Loc.t * Lib_name.t) list  (** ocaml libraries *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)
@@ -2042,6 +2051,7 @@ module Coq = struct
        and+ flags = Ordered_set_lang.Unexpanded.field "flags"
        and+ boot =
          field_b "boot" ~check:(Dune_lang.Syntax.since Stanza.syntax (2, 3))
+       and+ mode = located (field "mode" ~default:Mode.VoOnly Mode.decode)
        and+ modules = modules_field "modules"
        and+ libraries =
          field "libraries" (repeat (located Lib_name.decode)) ~default:[]
@@ -2054,6 +2064,7 @@ module Coq = struct
        ; synopsis
        ; modules
        ; flags
+       ; mode
        ; boot
        ; libraries
        ; theories

src/dune/dune_file.mli

@@ -352,13 +352,20 @@ module Rule : sig
 end
 
 module Coq : sig
+  module Mode : sig
+    type t =
+      | VoOnly
+      | Native
+  end
+
   type t =
     { name : Loc.t * Coq_lib_name.t
     ; package : Package.t option
     ; project : Dune_project.t
     ; synopsis : string option
     ; modules : Ordered_set_lang.t
     ; flags : Ordered_set_lang.Unexpanded.t
+    ; mode : Loc.t * Mode.t
     ; boot : bool
     ; libraries : (Loc.t * Lib_name.t) list  (** ocaml libraries *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)