From fbac626c50950204236cc828053442af1915277f Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 8 Nov 2022 22:27:20 +0100 Subject: [PATCH] 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 #6049. This continues and finishes an earlier attempt to do someting similar in #4722. Signed-off-by: Ali Caglayan ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be --- CHANGES.md | 3 ++ doc/coq.rst | 28 +++++++++---------- src/dune_rules/coq_rules.ml | 25 +++++++++++++---- src/dune_rules/coq_stanza.ml | 15 +++++----- src/dune_rules/coq_stanza.mli | 2 +- .../coq/coqdep-on-rebuild.t/dune-project | 4 +-- .../test-cases/coq/coqdep-on-rebuild.t/run.t | 8 +++--- .../coq/coqtop/coqtop-flags.t/run.t | 6 ++-- 8 files changed, 55 insertions(+), 36 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 4134eab7b3bc..2098f73f3346 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -59,6 +59,9 @@ diff` command can be used to just display the promotion without applying it. (#6160, fixes #5368, @emillon) +- Coq native mode is now automatically detected by Dune starting with Coq lang + 0.7 (#6409, @Alizter) + 3.5.0 (2022-10-19) ------------------ diff --git a/doc/coq.rst b/doc/coq.rst index 9e8126fb125e..843347d18a65 100644 --- a/doc/coq.rst +++ b/doc/coq.rst @@ -142,19 +142,17 @@ 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 - ```` 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`. - - 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` onwards, if Coq has been configured + with ``-native-compiler yes`` or ``ondemand``, Dune will always build the + ``cmxs`` files together with the ``vo`` files. + + You may override this by specifying ``(mode native)`` or ``(mode vo)``. Before + :ref:`Coq lang 0.7`, the native mode had to be manually specified. + + When developing with native, you may want the compilation to be faster. You + may add ``(mode vo)`` to your stanza to override the native mode and only + compile ``vo`` files. Previous versions of Dune before 3.6 would disable the + native rules depending on whether or not the ``dev`` profile was selected. Coq Documentation ~~~~~~~~~~~~~~~~~ @@ -249,8 +247,10 @@ 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``: ``(mode )`` is automatically detected from the configuration of Coq. .. _coq-lang-1.0: diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml index 4b40e7f82199..4619ae458307 100644 --- a/src/dune_rules/coq_rules.ml +++ b/src/dune_rules/coq_rules.ml @@ -178,9 +178,24 @@ 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 buildable.mode with + | Some x -> + if + buildable.coq_lang_version < (0, 7) + && Profile.is_dev (Super_context.context sctx).profile + then Memo.return Coq_mode.VoOnly + else 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 +345,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 -> @@ -692,8 +707,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 diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml index a2b90359274b..1121269e2a79 100644 --- a/src/dune_rules/coq_stanza.ml +++ b/src/dune_rules/coq_stanza.ml @@ -32,7 +32,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 : 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 *) @@ -56,12 +56,13 @@ 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 - (Dune_lang.Syntax.since coq_syntax (0, 3) >>> Coq_mode.decode)) + field_o "mode" + (Dune_lang.Syntax.since coq_syntax (0, 3) + >>> Dune_sexp.Syntax.deprecated_in coq_syntax (0, 7) + ~extra_info: + "Since Coq lang 0.7 the mode is automatically inferred from \ + the configuration of Coq." + >>> Coq_mode.decode) and+ use_stdlib = field ~default:true "stdlib" (Dune_lang.Syntax.since coq_syntax (0, 6) diff --git a/src/dune_rules/coq_stanza.mli b/src/dune_rules/coq_stanza.mli index 48084c7a7cc5..681f6980a698 100644 --- a/src/dune_rules/coq_stanza.mli +++ b/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 : 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 *) diff --git a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/dune-project b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/dune-project index 9ef6b81a34a1..db7dbbd4b5f7 100644 --- a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/dune-project +++ b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.5) +(lang dune 3.6) -(using coq 0.2) +(using coq 0.7) diff --git a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t index 536144c99886..8699c67504e2 100644 --- a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t @@ -17,9 +17,9 @@ coqdep a/a.v.d coqdep b/b.v.d coqdep b/d.v.d - coqc a/a.{glob,vo} - coqc b/b.{glob,vo} - coqc b/d.{glob,vo} + coqc a/Na_a.{cmi,cmxs},a/a.{glob,vo} + coqc b/Nb_b.{cmi,cmxs},b/b.{glob,vo} + coqc b/Nb_d.{cmi,cmxs},b/d.{glob,vo} $ cat > b/b.v < From a Require Import a. > Definition bar := a.foo. @@ -27,4 +27,4 @@ > EOF $ dune build --display short --debug-dependency-path coqdep b/b.v.d - coqc b/b.{glob,vo} + coqc b/Nb_b.{cmi,cmxs},b/b.{glob,vo} diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t index 72e62891652a..ee79499d0400 100644 --- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t @@ -1,9 +1,9 @@ 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) The flags passed to coqtop: $ dune coq top --toplevel=echo Test.v | sed 's/-nI .*coq-core/some-coq-core/' - -topfile $TESTCASE_ROOT/_build/default/Test.v -w -notation-overridden -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default minimal + -topfile $TESTCASE_ROOT/_build/default/Test.v -w -notation-overridden -w -deprecated-native-compiler-option -native-output-dir . -native-compiler on some-coq-core/kernel -nI $TESTCASE_ROOT/_build/default -R $TESTCASE_ROOT/_build/default minimal