[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_mode.ml

@@ -0,0 +1,10 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2020                              *)
+(* Written by: Emilio Jesús Gallego Arias *)
+
+type t =
+  | VoOnly
+  | Native
+
+let decode = Dune_lang.Decoder.(enum [ ("vo", VoOnly); ("native", Native) ])

src/dune/coq_mode.mli

@@ -0,0 +1,11 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2020                              *)
+(* Written by: Emilio Jesús Gallego Arias *)
+
+type t =
+  | VoOnly
+  | Native
+
+  val decode : t Dune_lang.Decoder.t
+

src/dune/coq_module.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
@@ -37,13 +38,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
+    | 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

@@ -38,7 +38,14 @@ val name : t -> Name.t
 
 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: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

@@ -1,7 +1,8 @@
 (* This file is licensed under The MIT License *)
 (* (c) MINES ParisTech 2018-2019               *)
 (* (c) INRIA 2020                              *)
-(* Written by: Emilio Jesús Gallego Arias *)
+(* Written by: Emilio Jesús Gallego Arias      *)
+(* Written by: Rudi Grinberg *)
 
 open! Stdune
 open Coq_stanza
@@ -17,6 +18,13 @@ module Util = struct
         let info = Lib.info t in
         Lib_info.src_dir info)
 
+  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
@@ -93,6 +101,8 @@ module Context = struct
     ; scope : Scope.t
     ; boot_type : Bootstrap.t
     ; build_dir : Path.Build.t
+    ; mode : Coq_mode.t
+    ; native_includes : Path.Set.t Or_exn.t
     }
 
   let coqc ?stdout_to t args =
@@ -139,7 +149,7 @@ module Context = struct
           (* If the mlpack files don't exist, don't fail *)
           Build.paths_existing (List.concat_map ~f:Util.ml_pack_files libs)) )
 
-  let create ~coqc_dir sctx ~dir ~wrapper_name ~theories_deps
+  let create ~coqc_dir sctx ~dir ~wrapper_name ~theories_deps ~mode ~native_includes
       (buildable : Buildable.t) =
     let loc = buildable.loc in
     let rr = resolve_program sctx ~dir ~loc in
@@ -163,6 +173,8 @@ module Context = struct
     ; scope
     ; boot_type = Bootstrap.No_boot
     ; build_dir
+    ; mode
+    ; native_includes
     }
 
   let for_module t coq_module =
@@ -251,8 +263,27 @@ let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module =
 let coqc_rule (cctx : _ Context.t) ~file_flags coq_module =
   let source = Coq_module.source coq_module in
   let file_flags =
-    let object_to = Coq_module.obj_file ~obj_dir:cctx.dir coq_module in
-    [ Command.Args.Hidden_targets [ object_to ]
+    let wrapper_name, mode, native_includes = cctx.wrapper_name, cctx.mode, cctx.native_includes in
+    let objects_to = Coq_module.obj_files ~wrapper_name ~mode ~obj_dir:cctx.dir coq_module |> List.map ~f:fst in
+    let native_flags =
+      match mode with
+      | Coq_mode.VoOnly -> file_flags
+      | Coq_mode.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
+        let obj_dir = cctx.dir 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)
     ]
@@ -310,6 +341,7 @@ let source_rule ~sctx theories =
 let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
   let name = snd s.name in
   let scope = SC.find_scope_by_dir sctx dir in
+  let lib_db = Scope.libs scope in
   let coq_lib_db = Scope.coq_libs scope in
   let theory = Coq_lib.DB.resolve coq_lib_db s.name |> Result.ok_exn in
 
@@ -318,7 +350,12 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
     (* Coq flags for depending libraries *)
     let theories_deps = Coq_lib.DB.requires coq_lib_db theory in
     let coqc_dir = Super_context.build_dir sctx in
-    Context.create sctx ~coqc_dir ~dir ~wrapper_name ~theories_deps s.buildable
+    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
+    Context.create sctx ~coqc_dir ~dir ~wrapper_name ~theories_deps ~mode ~native_includes s.buildable
   in
 
   (* List of modules to compile for this library *)
@@ -377,7 +414,7 @@ let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Theory.t) =
 let install_rules ~sctx ~dir s =
   match s with
   | { Theory.package = None; _ } -> []
-  | { Theory.package = Some package; _ } ->
+  | { Theory.package = Some package; mode; _ } ->
     let loc = s.buildable.loc in
     let scope = SC.find_scope_by_dir sctx dir in
     let dir_contents = Dir_contents.get sctx ~dir in
@@ -401,18 +438,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
-           ( Some loc
-           , 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
+                  ( Some loc
+                  , 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 ~dir (s : Coqpp.t) =
@@ -433,7 +470,8 @@ let extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) =
       let coq_lib_db = Scope.coq_libs scope in
       Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories
     in
-    Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps
+    let mode, native_includes = Coq_mode.VoOnly, Ok Path.Set.empty in
+    Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps ~mode ~native_includes
       s.buildable
   in
   let coq_module =

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/coq_stanza.ml

@@ -70,6 +70,7 @@ module Extraction = struct
 end
 
 module Theory = struct
+
   type t =
     { name : Loc.t * Coq_lib_name.t
     ; package : Package.t option
@@ -78,6 +79,7 @@ module Theory = struct
     ; modules : Ordered_set_lang.t
     ; boot : bool
     ; enabled_if : Blang.t
+    ; mode : Loc.t * Coq_mode.t
     ; buildable : Buildable.t
     }
 
@@ -127,6 +129,7 @@ module Theory = struct
        and+ synopsis = field_o "synopsis" string
        and+ boot =
          field_b "boot" ~check:(Dune_lang.Syntax.since coq_syntax (0, 2))
+       and+ mode = located (field "mode" ~default:Coq_mode.VoOnly Coq_mode.decode)
        and+ modules = modules_field "modules"
        and+ enabled_if = enabled_if ~since:None
        and+ buildable = Buildable.decode in
@@ -139,6 +142,7 @@ module Theory = struct
        ; boot
        ; buildable
        ; enabled_if
+       ; mode
        })
 
   type Stanza.t += T of t

src/dune/coq_stanza.mli

@@ -30,6 +30,7 @@ module Theory : sig
     ; modules : Ordered_set_lang.t
     ; boot : bool
     ; enabled_if : Blang.t
+    ; mode : Loc.t * Coq_mode.t
     ; buildable : Buildable.t
     }