feature(coq): automatic detection of native

We omit the need for native to be specified in the coq.theory stanza
and instead allow for Dune to automatically detect whether to enable
native compilation via the output of `coqc -config` which was exposed
in ocaml#6049. This continues and finishes an earlier attempt to do
someting similar in ocaml#4722.

Signed-off-by: Ali Caglayan <alizter@gmail.com>

ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
Signed-off-by: Ali Caglayan <alizter@gmail.com>

.github/workflows/workflow.yml

@@ -147,7 +147,15 @@ jobs:
           dune-cache: true
 
       - name: Install Coq
-        run: opam install coq.8.16.0 coq-native
+        run: opam install coq.8.16.0
+
+      - run: opam exec -- make test-coq
+        env:
+          # We disable the Dune cache when running the tests
+          DUNE_CACHE: disabled
+
+      - run: Install Coq native
+        run: opam install coq-native
 
       - run: opam exec -- make test-coq
         env:

doc/coq.rst

@@ -142,19 +142,10 @@ The semantics of the fields are:
   You may still use installed libraries in your Coq project, but there is
   currently no way for Dune to know about it.
 
-- You can enable the production of Coq's native compiler object files by setting
-  ``<coq_native_mode>`` to ``native``. This passes ``-native-compiler on`` to
-  Coq and install the corresponding object files under ``.coq-native``, when in
-  the ``release`` profile. The regular ``dev`` profile skips native compilation
-  to make the build faster. This has been available since :ref:`Coq lang
-  0.3<coq-lang>`.
-
-  Please note: support for ``native_compute`` is **experimental** and requires a
-  version of Coq later than 8.12.1. Furthermore, dependent theories *must* be
-  built with the ``(mode native)`` enabled. In addition to that, Coq must be
-  configured to support native compilation. Dune explicitly disables the
-  generation of native compilation objects when ``(mode vo)`` is enabled,
-  irrespective of the configuration of Coq. This will be improved in the future.
+- From version :ref:`Coq lang 0.7<coq-lang>` onwards, the native mode can be
+  automatically detected by Dune by querying ``coqc -config``. You may override
+  this by specifying ``<coq_native_mode>``. Before :ref:`Coq lang
+  0.6<coq-lang>`, the native mode must be manually specified.
 
 Coq Documentation
 ~~~~~~~~~~~~~~~~~
@@ -249,8 +240,11 @@ The supported Coq language versions (not the version of Coq) are:
 - ``0.3``: Support for ``(mode native)`` requires Coq >= 8.10 (and Dune >= 2.9
   for Coq >= 8.14).
 - ``0.4``: Support for interproject composition of theories.
-- ``0.5``: ``(libraries ...)`` field deprecated in favor of ``(plugins ...)`` field.
+- ``0.5``: ``(libraries ...)`` field deprecated in favor of ``(plugins ...)``
+  field.
 - ``0.6``: Support for ``(stdlib no)``.
+- ``0.7``: Support for automatic handling of native compilation according to Coq
+  compilation.
 
 .. _coq-lang-1.0:
 

src/dune_rules/coq_rules.ml

@@ -178,9 +178,19 @@ end
 (* get_libraries from Coq's ML dependencies *)
 let libs_of_coq_deps ~lib_db = Resolve.Memo.List.map ~f:(Lib.DB.resolve lib_db)
 
-let select_native_mode ~sctx ~(buildable : Buildable.t) : Coq_mode.t =
-  let profile = (Super_context.context sctx).profile in
-  if Profile.is_dev profile then VoOnly else snd buildable.mode
+let select_native_mode ~sctx ~dir (buildable : Coq_stanza.Buildable.t) =
+  match snd buildable.mode with
+  | Some x -> Memo.return x
+  | None -> (
+    if buildable.coq_lang_version < (0, 3) then Memo.return Coq_mode.Legacy
+    else if buildable.coq_lang_version < (0, 7) then Memo.return Coq_mode.VoOnly
+    else
+      let* coqc = resolve_program sctx ~dir ~loc:buildable.loc "coqc" in
+      let+ config = Coq_config.make ~bin:(Action.Prog.ok_exn coqc) in
+      match Coq_config.by_name config "coq_native_compiler_default" with
+      | Some (Coq_config.Value.String "yes")
+      | Some (Coq_config.Value.String "ondemand") -> Coq_mode.Native
+      | _ -> Coq_mode.VoOnly)
 
 let rec resolve_first lib_db = function
   | [] -> assert false
@@ -330,7 +340,7 @@ module Context = struct
     let ml_flags, mlpack_rule =
       Coq_plugin.of_buildable ~context ~theories_deps ~lib_db buildable
     in
-    let mode = select_native_mode ~sctx ~buildable in
+    let* mode = select_native_mode ~sctx ~dir buildable in
     let* native_includes =
       let open Resolve.Memo.O in
       resolve_first lib_db [ "coq-core.kernel"; "coq.kernel" ] >>| fun lib ->
@@ -687,8 +697,8 @@ let install_rules ~sctx ~dir s =
   match s with
   | { Theory.package = None; _ } -> Memo.return []
   | { Theory.package = Some package; buildable; _ } ->
-    let mode = select_native_mode ~sctx ~buildable in
     let loc = s.buildable.loc in
+    let* mode = select_native_mode ~sctx ~dir buildable in
     let* scope = Scope.DB.find_by_dir dir in
     let* dir_contents = Dir_contents.get sctx ~dir in
     let name = snd s.name in

src/dune_rules/coq_stanza.ml

@@ -33,7 +33,7 @@ module Buildable = struct
   type t =
     { flags : Ordered_set_lang.Unexpanded.t
     ; coq_lang_version : Dune_sexp.Syntax.Version.t
-    ; mode : Loc.t * Coq_mode.t
+    ; mode : Loc.t * Coq_mode.t option
     ; use_stdlib : bool
     ; plugins : (Loc.t * Lib_name.t) list  (** ocaml libraries *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)
@@ -57,11 +57,8 @@ module Buildable = struct
     let+ loc = loc
     and+ flags = Ordered_set_lang.Unexpanded.field "flags"
     and+ mode =
-      let default =
-        if coq_lang_version < (0, 3) then Coq_mode.Legacy else Coq_mode.VoOnly
-      in
       located
-        (field "mode" ~default
+        (field_o "mode"
            (Dune_lang.Syntax.since coq_syntax (0, 3) >>> Coq_mode.decode))
     and+ use_stdlib =
       field ~default:true "stdlib"

src/dune_rules/coq_stanza.mli

@@ -4,7 +4,7 @@ module Buildable : sig
   type t =
     { flags : Ordered_set_lang.Unexpanded.t
     ; coq_lang_version : Dune_sexp.Syntax.Version.t
-    ; mode : Loc.t * Coq_mode.t
+    ; mode : Loc.t * Coq_mode.t option
     ; use_stdlib : bool
     ; plugins : (Loc.t * Lib_name.t) list  (** ocaml plugins *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)

test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t

@@ -1,12 +1,12 @@
 Testing that the correct flags are being passed to dune coq top
 
 The flags passed to coqc:
-  $ dune build && tail -1 _build/log | sed 's/(cd .*coqc/coqc/' | sed 's/$ //'
-  coqc -w -notation-overridden -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R . minimal Test.v)
+  $ dune build && tail -1 _build/log | sed 's/(cd .*coqc/coqc/' | sed 's/$ //' | sed 's/-nI .*coq-core/some-coq-core/'
+  coqc -w -notation-overridden -w -deprecated-native-compiler-option -native-output-dir . -native-compiler on some-coq-core/kernel -nI . -R . minimal Test.v)
 
 BUG: coqtop flags are missing. Specifically ones from Context.coq_flags in
 coq_rules.ml
 
 The flags passed to coqtop:
-  $ dune coq top --toplevel=echo Test.v
+  $ dune coq top --toplevel=echo Test.v | sed 's/-nI .*coq-core/some-coq-core/'
   -topfile $TESTCASE_ROOT/_build/default/Test.v -R $TESTCASE_ROOT/_build/default minimal