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 b562c26514ce..ba3e96b4a7b7 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_mode.ml b/src/dune_rules/coq_mode.ml index e28650f628a4..b512dc3214f8 100644 --- a/src/dune_rules/coq_mode.ml +++ b/src/dune_rules/coq_mode.ml @@ -11,4 +11,14 @@ type t = | VoOnly | Native -let decode = Dune_lang.Decoder.(enum [ ("vo", VoOnly); ("native", Native) ]) +let decode ~coq_syntax = + Dune_lang.Decoder.( + enum' + [ ("vo", return VoOnly) + ; ( "native" + , Dune_sexp.Syntax.deprecated_in coq_syntax (0, 7) + ~extra_info: + "Since Coq lang 0.7 native mode is automatically inferred from \ + the configuration of Coq." + >>> return Native ) + ]) diff --git a/src/dune_rules/coq_mode.mli b/src/dune_rules/coq_mode.mli index 44de8b5bec44..2f9dbdde53c9 100644 --- a/src/dune_rules/coq_mode.mli +++ b/src/dune_rules/coq_mode.mli @@ -11,4 +11,4 @@ type t = | VoOnly | Native -val decode : t Dune_lang.Decoder.t +val decode : coq_syntax:Dune_lang.Syntax.t -> t Dune_lang.Decoder.t 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 2749d74077be..4e3f946aac1f 100644 --- a/src/dune_rules/coq_stanza.ml +++ b/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 : 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,12 +57,9 @@ 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) + >>> Coq_mode.decode ~coq_syntax) 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/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