diff --git a/CHANGES.md b/CHANGES.md index 090f13dccb8f..cbcde68015a2 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -59,6 +59,9 @@ Unreleased 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..632526c201ac 100644 --- a/doc/coq.rst +++ b/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 - ```` 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, the native mode is + automatically detected by Dune by querying ``coqc -config``. You may override + this by specifying ``(mode native)`` or ``(mode vo)``. Before :ref:`Coq lang + 0.6`, the native mode had to 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: diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml index 4b40e7f82199..3eb6aa7a6a1c 100644 --- a/src/dune_rules/coq_rules.ml +++ b/src/dune_rules/coq_rules.ml @@ -178,9 +178,21 @@ 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 -> + let profile = (Super_context.context sctx).profile in + Memo.return @@ if Profile.is_dev profile then Coq_mode.VoOnly else 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 +342,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 +704,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 5e3801d70f7d..ed71836e2db9 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,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 - (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) 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/coqtop/coqtop-flags.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t index 72e62891652a..dbfb8f652925 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 \ No newline at end of file