Merge pull request #3210 from ejgallego/coq+native

[coq] Add support for native-mode compilation.

Author: rgrinberg

CHANGES.md

@@ -91,6 +91,8 @@ Unreleased
 
 - [coq] Add `-q` flag to `:standard` `coqc` flags , fixes #3924, (#3931 , @ejgallego)
 
+- Add support for Coq's native compute compilation mode (@ejgallego, #3210)
+
 2.7.1 (2/09/2020)
 -----------------
 

Makefile

@@ -11,7 +11,7 @@ BIN := ./dune.exe
 TEST_DEPS := \
 bisect_ppx \
 cinaps \
-coq \
+"coq>=8.12.1" \
 core_bench \
 "csexp>=1.3.0" \
 js_of_ocaml \

doc/dune-files.rst

@@ -1625,6 +1625,7 @@ The basic form for defining Coq libraries is very similar to the OCaml form:
      (modules <ordered_set_lang>)
      (libraries <ocaml_libraries>)
      (flags <coq_flags>)
+     (mode <coq_native_mode>)
      (theories <coq_theories>))
 
 The stanza will build all ``.v`` files on the given directory. The semantics of fields is:
@@ -1668,6 +1669,17 @@ The stanza will build all ``.v`` files on the given directory. The semantics of
   composition with the Coq's standard library is supported, but in
   this case the ``Coq`` prefix will be made available in a qualified
   way. Since Coq's lang version ``0.2``.
+- you can enable the production of Coq's native compiler object files
+  by setting ``<coq_native_mode>`` to ``native``, this will pass
+  ``-native-compiler on`` to Coq and install the corresponding object
+  files under `.coq-native`. Note that the support for native compute
+  is **experimental**, and requires Coq >= 8.12.1; moreover, depending
+  libraries *must* be built with ``(mode native)`` too for this to
+  work; also Coq must be configured to support native
+  compilation. Note that Dune will by explicitly disable output of
+  native compilation objects when `(mode vo)` even if the default
+  Coq's configure flag enabled it. This will be improved in the
+  future.
 
 Recursive qualification of modules
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1899,9 +1911,9 @@ a typical ``dune-workspace`` file looks like:
 .. code:: scheme
 
     (lang dune 2.8)
-    (context (opam (switch 4.02.3)))
-    (context (opam (switch 4.03.0)))
-    (context (opam (switch 4.04.0)))
+    (context (opam (switch 4.07.1)))
+    (context (opam (switch 4.08.1)))
+    (context (opam (switch 4.11.1)))
 
 The rest of this section describe the stanzas available.
 

src/dune_rules/coq_lib.ml

@@ -2,6 +2,7 @@ open! Dune_engine
 
 (* 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_rules/coq_lib_name.mli

@@ -2,6 +2,7 @@ open! Dune_engine
 
 (* 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_rules/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_rules/coq_mode.mli

@@ -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
+
+val decode : t Dune_lang.Decoder.t

src/dune_rules/coq_module.ml

@@ -2,6 +2,7 @@ open! Dune_engine
 
 (* 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
@@ -39,23 +40,44 @@ let name x = x.name
 let build_vo_dir ~obj_dir x =
   List.fold_left x.prefix ~init:obj_dir ~f:Path.Build.relative
 
-type obj =
-  | Dep
-  | Aux
-  | Glob
-  | Obj
-
-let fname_of_obj t obj =
-  match obj with
-  | Dep -> t.name ^ ".v.d"
-  | Aux -> "." ^ t.name ^ ".aux"
-  | Glob -> t.name ^ ".glob"
-  | Obj -> t.name ^ ".vo"
-
-let obj_file t obj ~obj_dir =
-  let vo_dir = build_vo_dir ~obj_dir t in
-  let fname = fname_of_obj t obj in
-  Path.Build.relative vo_dir fname
+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 x ~obj_dir =
+  let vo_dir = build_vo_dir ~obj_dir x in
+  Path.Build.relative vo_dir (x.name ^ ".v.d")
+
+type obj_files_mode =
+  | Build
+  | Install
+
+(* XXX: Remove the install .coq-native hack once rules can output targets in
+   multiple subdirs *)
+let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode =
+  let vo_dir = build_vo_dir ~obj_dir x in
+  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
+          , Filename.(concat (concat install_vo_dir ".coq-native") x) ))
+        cmxs_obj
+    | VoOnly -> []
+  in
+  let obj_files =
+    match obj_files_mode with
+    | Build -> [ x.name ^ ".vo"; "." ^ x.name ^ ".aux"; x.name ^ ".glob" ]
+    | Install -> [ x.name ^ ".vo" ]
+  in
+  List.map obj_files ~f:(fun fname ->
+      (Path.Build.relative vo_dir fname, Filename.concat install_vo_dir fname))
+  @ native_objs
 
 let to_dyn { source; prefix; name } =
   let open Dyn.Encoder in

src/dune_rules/coq_module.mli

@@ -38,13 +38,23 @@ val prefix : t -> string list
 
 val name : t -> Name.t
 
-type obj =
-  | Dep
-  | Aux
-  | Glob
-  | Obj
-
-val obj_file : t -> obj -> obj_dir:Path.Build.t -> Path.Build.t
+val dep_file : t -> obj_dir:Path.Build.t -> Path.Build.t
+
+(** Some of the object files should not be installed, we control this with the
+    following parameter *)
+type obj_files_mode =
+  | Build
+  | Install
+
+(** This returns a list of pairs [(obj_file, install_path)] due to native files
+    having a different install location *)
+val obj_files :
+     t
+  -> wrapper_name:string
+  -> mode:Coq_mode.t
+  -> obj_dir:Path.Build.t
+  -> obj_files_mode:obj_files_mode
+  -> (Path.Build.t * string) list
 
 val to_dyn : t -> Dyn.t