Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feature(coq): automatic detection of native #6409

Merged
merged 1 commit into from
Nov 15, 2022
Merged

feature(coq): automatic detection of native #6409

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,10 @@
Unreleased
----------

- Coq native mode is now automatically detected by Dune starting with Coq lang
0.7. `(mode native)` has been deprecated in favour of detection from the
configuration of Coq. (#6409, @Alizter)

3.6.0 (2022-11-14)
------------------

Expand Down
28 changes: 14 additions & 14 deletions doc/coq.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -142,19 +142,15 @@ 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
Comment on lines -148 to -149
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since the behavior is kept, the sentence "The regular dev profile skips native compilation to make the build faster." should also be kept. It can be a pretty disturbing behavior, so I think it should at the very least be documented.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah I am not a fan of it at all TBH.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Me neither, for the following reason, after this PR:

  • most users will use the default (no mode stanza)
  • when something is not compatible with coqnative, mode vo can be used
  • so mode native has probably no other use than to test compilation with native, the more complex behavior where it is disabled in dev mode can then be more disturbing than anything for those users

(of course I might be missing something)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I will remove it. If we want something like this in the future, we should support it correctly. Either we add the split native compilation which will allow users to compile native as a second step or we allow users to explicitly disable native themselves in their profiles.

But keeping this confusing default behavior isn't great. As you said, (mode vo) can always be used.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

mode native is indeed made obsolete by this PR. dev disabling native is indeed a mixed bag, and was also motivated by the lack of dynamic configuration, previosly you had to edit the stanza to disable native for example when developing Coq, as you don't want to take the expensive compilation route.

Now you can set it at configure time, so the tradeoff is a bit better.

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, 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<coq-lang>`, the native mode had to be manually specified.

Previous versions of Dune before 3.7 would disable the native rules depending
on whether or not the ``dev`` profile was selected.

Coq Documentation
~~~~~~~~~~~~~~~~~
Expand Down Expand Up @@ -249,8 +245,12 @@ 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
and ``(mode native)`` is deprecated. The ``dev`` profile also no longer
disables native compilation.

.. _coq-lang-1.0:

Expand Down
12 changes: 11 additions & 1 deletion src/dune_rules/coq_mode.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 )
])
2 changes: 1 addition & 1 deletion src/dune_rules/coq_mode.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
25 changes: 20 additions & 5 deletions src/dune_rules/coq_rules.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just an fyi, this breaks lazy loading absolutely everywhere where coq stanzas are present. I'm not sure if you care though.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we already broke lazy loading since coqc and coqdep were being resolved in the common context in Coq_rules.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't the resolution inside the monad tho?

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
Expand Down Expand Up @@ -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 ->
Expand Down Expand Up @@ -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
Expand Down
11 changes: 4 additions & 7 deletions src/dune_rules/coq_stanza.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've removed the Loc since we don't even use it.

; 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 *)
Expand All @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion src/dune_rules/coq_stanza.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
2 changes: 1 addition & 1 deletion test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/dune-project
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
(lang dune 3.7)

(using coq 0.3)
(using coq 0.7)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wouldn't it be better for this to correspond to the version the test was introduced?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see the point.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The point would be consistency with the common practice we do, the test doesn't require coq lang 0.7 so in this sense the new constraint is an over-requirement.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But 0.2 brings out the legacy native mode which is broken. I guess the next one to choose would be 0.3, but why not just use 0.7?

8 changes: 4 additions & 4 deletions test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,14 +17,14 @@
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 <<EOF
> From a Require Import a.
> Definition bar := a.foo.
> Definition zoo := 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}
6 changes: 3 additions & 3 deletions test/blackbox-tests/test-cases/coq/coqtop/coqtop-flags.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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