[coq] Preliminary support for split native compilation

Coq 8.14 can generate native files independently from .vo file
generation by using a new `coqnative` compiler, which will do the `.vo
-> .cmxs` translation.

This allows Dune to have a simpler rule setup, as it is always
possible to rely on coqnative to compile native files, as opposed to
before where native file generation was controlled by a Coq-level
configure flag.

The new rule setup is enabled for `(lang coq 0.4)`, and we provide a
couple of configuration options in the `mode` field via a couple of
optional fields:

```lisp
(coq.theory
  ...
  (mode
   (native
     (package pkg)
     (profile p1 ... pn))))
```

The first field, `(package )` allows to override the package under
which native files for the corresponding theory will be
installed. This is useful for packagers willing to split the native
compilation under a different package, given that it can be extremely
resource-intensive. The default for this setting is the same package
name.

The second field controls under which profiles Dune will setup the
native build rules; the default for this setting is `release`, so Dune
will skip Coq's native compilation when in `dev` mode.

`(mode vo)` is still accepted, in case developers would like to
completely disable native generation.

TODO: take into account the `(package field)` for `native` , to be
implemented in the next commit.

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

CHANGES.md

@@ -166,6 +166,8 @@ Unreleased
 
 - Handle renaming of `coq.kernel` library to `coq-core.kernel` in Coq 8.14 (#4713, @proux01)
 
+- Support new Coq 8.14 standalone native compiler mode (# , @ejgallego @ppedrot @Zimmi48)
+
 2.8.5 (28/03/2021)
 ------------------
 

doc/dune-files.rst

@@ -1691,6 +1691,8 @@ The supported Coq language versions are:
 - ``0.1``: basic Coq theory support,
 - ``0.2``: support for the ``theories`` field, and composition of theories in the same scope,
 - ``0.3``: support for ``(mode native)``, requires Coq >= 8.10 (and dune >= 2.9 for Coq >= 8.14).
+  This mode is deprecated and we strongly recommend native users to move to version ``0.4``
+- ``0.5``: reworked ``(mode native)`` using the standalone Coq native compiler, requires Coq >= 8.14 and dune >= 3.0.
 
 Guarantees with respect to stability are not provided yet,
 however, as implementation of features progresses, we hope to reach
@@ -1753,18 +1755,26 @@ 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`` when in ``release`` profile. The regular
-  ``dev`` profile will skip native compilation to make the build
-  faster. Since Coq's lang version ``0.3``. 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 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.
+
+- you can control the production of Coq's native compiler object files
+  by setting ``<coq_native_mode>`` to ``native`` [the default] or to
+  ``vo``, to disable the rules relative to Coq native objects.
+
+  By default, Dune uses the ``coqnative`` binary introduced in Coq
+  8.14 and will setup the rules for the compilation and install of
+  native objects when using the ``release`` Dune profile. This can be
+  tweaked using the ``profile`` field, to enable such rules for
+  different profiles, for example ``(mode (native (profile dev
+  release)))`` will enable the rules for the dev profile too.
+
+  Additionally, Dune provides support for installing the native object
+  files to a different package; by default, Dune will place the Coq
+  native object files in the main package for the corresponding
+  ``(coq.theory ...)`` stanza, but users can override that to provide
+  split compilation using the ``package`` field; example, using:
+  ``(mode (native (package coq-bar-native)))`` will allow users to use
+  ``dune -p coq-bar`` and ``dune -p coq-bar-native`` to build the
+  native files separately, if so desired.
 
 Recursive qualification of modules
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

src/dune_rules/coq_lib.ml

@@ -81,6 +81,7 @@ module DB = struct
   type nonrec t =
     { boot : (Loc.t * t) option
     ; libs : t Coq_lib_name.Map.t
+    ; obj_root_revmap : t Path.Build.Map.t
     }
 
   let boot_library { boot; _ } = boot
@@ -113,7 +114,12 @@ module DB = struct
       | _ :: (_, s2) :: _ ->
         Result.ok_exn (Error.duplicate_boot_lib ~loc:s2.buildable.loc s2)
     in
-    { boot; libs }
+    let obj_root_revmap =
+      Coq_lib_name.Map.fold libs ~init:Path.Build.Map.empty ~f:(fun lib rmap ->
+          let dir = obj_root lib in
+          Path.Build.Map.add_exn rmap dir lib)
+    in
+    { boot; libs; obj_root_revmap }
 
   let resolve ?(allow_private_deps = true) db (loc, name) =
     match Coq_lib_name.Map.find db.libs name with
@@ -165,4 +171,17 @@ module DB = struct
       top_closure db theories ~loc ~allow_private_deps:true
 
   let resolve db l = resolve db l
+
+  let module_of_source_file { obj_root_revmap; _ } file =
+    let name = Path.Build.basename file in
+    let dir = Path.Build.parent_exn file in
+    let rec aux acc_prefix dir =
+      match Path.Build.Map.find obj_root_revmap dir with
+      | None ->
+        let acc_prefix = Path.Build.basename dir :: acc_prefix in
+        let dir = Path.Build.parent_exn dir in
+        aux acc_prefix dir
+      | Some lib -> (lib, List.rev acc_prefix, name)
+    in
+    aux [] dir
 end

src/dune_rules/coq_lib.mli

@@ -43,5 +43,14 @@ module DB : sig
 
   val requires_for_user_written :
     t -> (Loc.t * Coq_lib_name.t) list -> lib list Or_exn.t
+
+  (** Reverse map from source names to a matching lib, plus the matching suffix;
+      this is only required because coqdep doesn't handle native dependencies,
+      so for a dependency [path/bar/foo.vo] we must correctly translate it to
+      its mangled Coq native form, which requires locating the library which a
+      source does belong to. The current matching function does return a triple
+      [lib,
+     prefix, name] for a given input path, or raises if not found *)
+  val module_of_source_file : t -> Path.Build.t -> lib * string list * string
 end
 with type lib := t

src/dune_rules/coq_mode.ml

@@ -10,5 +10,25 @@ type t =
   | Legacy
   | VoOnly
   | Native
+  | Split of
+      { package : string option
+      ; profile : string list
+      }
 
-let decode = Dune_lang.Decoder.(enum [ ("vo", VoOnly); ("native", Native) ])
+let default_profile = [ "release" ]
+
+let default = Split { package = None; profile = default_profile }
+
+let decode_v03 = Dune_lang.Decoder.(enum [ ("vo", VoOnly); ("native", Native) ])
+
+let decode_v04 =
+  let open Dune_lang.Decoder in
+  let native =
+    fields
+      (let+ package = field_o "package" string
+       and+ profile =
+         field ~default:default_profile "profile" (repeat string)
+       in
+       Split { package; profile })
+  in
+  sum [ ("vo", return VoOnly); ("native", native) ]

src/dune_rules/coq_mode.mli

@@ -10,5 +10,14 @@ type t =
   | Legacy
   | VoOnly
   | Native
+  | Split of
+      { package : string option
+      ; profile : string list
+      }
 
-val decode : t Dune_lang.Decoder.t
+val default : t
+
+(* We provide two different decoders depending on the Coq language syntax *)
+val decode_v03 : t Dune_lang.Decoder.t
+
+val decode_v04 : t Dune_lang.Decoder.t

src/dune_rules/coq_module.ml

@@ -37,37 +37,50 @@ let prefix x = x.prefix
 
 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 build_vo_dir ~obj_dir ~prefix =
+  List.fold_left prefix ~init:obj_dir ~f:Path.Build.relative
+
+let mangled_native_filename ~wrapper_name ~prefix ~name =
+  "N" ^ String.concat ~sep:"_" (wrapper_name :: prefix @ [ name ])
 
 let cmxs_of_mod ~wrapper_name x =
   let native_base =
-    "N" ^ String.concat ~sep:"_" (wrapper_name :: x.prefix @ [ x.name ])
+    mangled_native_filename ~wrapper_name ~prefix:x.prefix ~name:x.name
   in
   [ native_base ^ ".cmi"; native_base ^ ".cmxs" ]
 
+let native_mangle_filename ~wrapper_name ~prefix ~name ~obj_dir ~ext =
+  let native_base = mangled_native_filename ~wrapper_name ~prefix ~name in
+  let vo_dir = build_vo_dir ~obj_dir ~prefix in
+  Path.Build.relative vo_dir (native_base ^ ext)
+
 let dep_file x ~obj_dir =
-  let vo_dir = build_vo_dir ~obj_dir x in
+  let vo_dir = build_vo_dir ~obj_dir ~prefix:x.prefix in
   Path.Build.relative vo_dir (x.name ^ ".v.d")
 
 type obj_files_mode =
   | Build
   | Install
 
+let native_obj_files_core x ~wrapper_name ~vo_dir ~install_vo_dir =
+  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
+
 (* 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 vo_dir = build_vo_dir ~obj_dir ~prefix:x.prefix 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
+      native_obj_files_core x ~wrapper_name ~vo_dir ~install_vo_dir
+    (* split mode doesn't produce any file for coqc *)
+    | Split _
     | VoOnly
     | Legacy ->
       []
@@ -81,6 +94,16 @@ let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode =
       (Path.Build.relative vo_dir fname, Filename.concat install_vo_dir fname))
   @ native_objs
 
+let vo_obj_file x ~obj_dir =
+  let vo_dir = build_vo_dir ~obj_dir ~prefix:x.prefix in
+  let fname = x.name ^ ".vo" in
+  Path.Build.relative vo_dir fname
+
+let native_obj_files x ~wrapper_name ~obj_dir =
+  let vo_dir = build_vo_dir ~obj_dir ~prefix:x.prefix in
+  let install_vo_dir = String.concat ~sep:"/" x.prefix in
+  native_obj_files_core x ~wrapper_name ~vo_dir ~install_vo_dir
+
 let to_dyn { source; prefix; name } =
   let open Dyn.Encoder in
   record

src/dune_rules/coq_module.mli

@@ -46,8 +46,11 @@ 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 *)
+(** [obj_files t wrapper_name mode obj_dir obj_files_mode] returns the list of
+    object files produced by a [coqc] invocation.
+
+    Note that This returns a list of pairs [(obj_file, install_path)] due to
+    native files having a different install / build location *)
 val obj_files :
      t
   -> wrapper_name:string
@@ -56,6 +59,39 @@ val obj_files :
   -> obj_files_mode:obj_files_mode
   -> (Path.Build.t * string) list
 
+(** [obj_file t] returns just the .vo file of a module, this is the input to the
+    standalone Coq native compiler; we should likely refactor this to pass the
+    kind of object to obj_files as it was done some time ago by Rudi *)
+val vo_obj_file : t -> obj_dir:Path.Build.t -> Path.Build.t
+
+(** [native_obj_files] is the equivalent of [obj_files] but for the new
+    [coqnative] separate Coq native compiler, it is used in the setup of the
+    separate rules. *)
+val native_obj_files :
+     t
+  -> wrapper_name:string
+  -> obj_dir:Path.Build.t
+  -> (Path.Build.t * string) list
+
+(** [native_mangle_filename ~wrapper_name ~prefix ~name ~ext] will generate a
+    mangled Coq native module file name from its arguments, determining a Coq
+    module. Coq's native compiler needs to mangle filenames for a module
+    [bar/foo.vo] bound to a [wrapper_name] [baz] to [NBaz_Bar_Foo.cmxs] to
+    prevent collisions, as the OCaml compiler doesn't support encoding hiearchy
+    of modules using the filesystem. We should eventually improve the clients of
+    this API so we can just pass here a [Coq_module.t] *)
+val native_mangle_filename :
+     wrapper_name:string
+  -> prefix:string list
+  -> name:string
+  -> obj_dir:Path.Build.t
+  -> ext:string
+  -> Path.Build.t
+
+(** [vo_to_native file ~ext] will transform a file of the form , note we need a
+    reverse lookup from .vo file to Coq module *)
+(* val vo_to_native : Path.Build.t -> ext:string -> Path.Build.t *)
+
 val to_dyn : t -> Dyn.t
 
 val eval : dir:Path.Build.t -> standard:t list -> Ordered_set_lang.t -> t list