[coq] pick flags from profile #3547

gares · 2020-06-11T12:55:36Z

disclaimer I don't know the code of dune at all, this is symbol pushing

This PR adds (coq (flags <osl>)) to profile

OUTDATED:
~This PR makes it possible to use different Coq compilation backends via profiles. Today Coq can produce object files in 3 ways:

complete check (slow, safe)
check statement, drop proofs (fast cpu, fast io, totally unsafe wrt proofs)
check statements, keep proof "thunks" (fast cpu, slow io, mostly safe wrt proofs when the thunks are forced, see @check-proofs below)

Currently Coq names the files .vo, .vos and .vio respectively but internally the format is the same (it is a segment based format, some segments are optional). Via make Coq supports various workflows, and indeed the different file names are motivated by the fact that this way different make rules are easily written/selected. The idea discussed at a Coq call was to support most of these workflows/backends by

letting one chose a backend via --profile (or (profile ..))
implement dune specific Coq options to name the output .vo independently of the backend (so that dune rules can stay the same).

This is a WIP, and I don't have yet a Coq branch supporting the -vos-dune and -vio-dune flags I used there (but I'm pretty sure I can do this). I open the draft PR mainly to gather feedback and avoid duplication of work for #3486 . make test-coq seems to suggest I'm calling Coq with the expected flags in the blackbox test I've added.

Things to be checked by someone understanding dune internals:

when the backend changes the .vo files need to be rebuilt (invalidated)
eventually one can add a target @check-proofs. This target succeed immediately with the first backend, always fails with the second. With the third backend it runs a rule that depends on all .vo files and runs a specific coqc invocation (all proofs can be checked in parallel)~

Fix #3486
CC @Zimmi48 @ejgallego

ejgallego · 2020-06-11T18:24:24Z

Thanks for the PR @gares, a couple of comments:

it seems you don't intend to change the rules, then wouldn't it better to just implement (coq (flags ...)) in the profile, and have users just put the flag there?
if you don't change the build rules, you don't gain a lot, right?
Wouldn't reusing .vo be confusing for the users too? IMHO it is better if we try to be consistent with the current way things are built.
indeed if you change the set of flags, Dune will invalidate the targets.

Once we agree on the first point I will make a pass on the rest of the file.

ejgallego · 2020-06-11T18:27:47Z

Note that it is easy for example to introduce an alias for all vio / vos in a library, such as @library/interfaces [that would compile for example .vos].

An advantage of using different extensions is that I think incremental behavior is a bit better, for example if you decide to compile some part of you workspace with quick, this will force a full rebuild.

The conditional dependency on a .vio / .vo can be actually captured pretty well I think, tho you may want to need some flag at some point, or just piggyback on the release profile to disable rules that may produce unsound type-checking.

ejgallego · 2020-06-11T18:28:33Z

src/dune/coq_rules.ml

@@ -93,15 +93,23 @@ module Context = struct
    ; scope : Scope.t
    ; boot_type : Bootstrap.t
    ; build_dir : Path.Build.t
+    ; backend : Dune_env.Stanza.Coq.backend
    }

  let coqc ?stdout_to t args =
    let dir = Path.build (snd t.coqc) in
    Command.run ~dir ?stdout_to (fst t.coqc) args

  let coq_flags t =


Small note, I will move this to Coq_flags soon as indeed handling of flags is becoming quite interesting.

gares · 2020-06-11T18:28:34Z

it seems you don't intend to change the rules, then wouldn't it better to just implement (coq (flags ...)) in the profile, and have users just put the flag there?

that would work as well, but asking one to write -vio-dune seems less declarative to me.
for experimenting it is perfectly fine.

if you don't change the build rules, you don't gain a lot, right?

of course you gain: even if the dag of dependencies is the same, coqc is much faster in vos or vio mode since it does not check proofs.

Wouldn't reusing .vo be confusing for the users too? IMHO it is better if we try to be consistent with the current way things are built.

no, because in dune they don't see the build artifacts

indeed if you change the set of flags, Dune will invalidate the targets.

great!

ejgallego · 2020-06-11T18:29:28Z

src/dune/super_context.mli

@@ -79,6 +79,9 @@ val local_binaries : t -> dir:Path.Build.t -> File_binding.Expanded.t list
 (** odoc config in the corresponding [(env)] stanza. *)
 val odoc : t -> dir:Path.Build.t -> Env_node.Odoc.t

+(** coq config in the corresponding [(env)] stanza. *)
+val coq : t -> dir:Path.Build.t -> Env_node.Coq.t


Need to have a closer look but the part related to env / SC seems OK to me.

ejgallego · 2020-06-11T18:30:11Z

Also, DCO is needed, it is also recommended to run make fmt once the PR is ready, but we do this just before merging usually.

gares · 2020-06-11T18:35:41Z

Is the DCO just about adding a sign-of line to commits as CI reports?

ejgallego · 2020-06-11T18:41:31Z

that would work as well, but asking one to write -vio-dune seems less declarative to me.
for experimenting it is perfectly fine.

I'd say let's add a general (coq (flags ...)) field for now, that may have other uses and it is fine indeed to keep supporting for a long time; a deeper change such a new quick profile may require more thinking, I'm not very convinced of adding a full new meaning for what amounts to setting a flag.

of course you gain: even if the dag of dependencies is the same, coqc is much faster in vos or vio mode since it does not check proofs.

Indeed that's quite a bit, but I mean you can do this already using (include ...) in the flags field; ideally you would also get best of both worlds and vio -> vo etc...

no, because in dune they don't see the build artifacts

Still people may want to look at _build to see what's going on, also this strategy of reusing names has a risk which is that people could install wrongly named libraries. Actually, this method won't produce installable packages that are both using vos/vo right?

Yup, the DCO is about signing-off your commits [which implies you agree with the contributing agreement]

More things needed: update documentation.

gares · 2020-06-11T18:42:44Z

An advantage of using different extensions is that I think incremental behavior is a bit better, for example if you decide to compile some part of you workspace with quick, this will force a full rebuild.

This is one thing I would avoid as it has always been a mess in Coq.
Do you remember the "heuristic" about loading the .vio, or maybe the .vo if more recent... and now we also have vos/vok with the empty file hack. What I proposed at the Coq call is to question this choice, and start from the simpler approach of making the 3 worlds disconnected, as profiles are if I'm not mistaken.

ejgallego · 2020-06-11T18:52:44Z

Do you remember the "heuristic" about loading the .vio, or maybe the .vo if more recent... and now we also have vos/vok with the empty file hack. What I proposed at the Coq call is to question this choice, and start from the simpler approach of making the 3 worlds disconnected, as profiles are if I'm not mistaken.

Yup, but indeed these worlds are quite disconnected IIUC, for example vos are supposed to be interfaces, so I'm not sure the same file name would work as they are too disconnected. Moreover, it seems this would prevent some valid use cases as I mention w.r.t. incremental setup.

I think it is OK to have interesting rules as long as we design them properly. Indeed that may mean we need to rethink the way vos/vio interact with profiles, but on the other hand this seems less radical than just bump all of them together.

gares · 2020-06-11T18:56:15Z

Still people may want to look at _build to see what's going on, also this strategy of reusing names has a risk which is that people could install wrongly named libraries.

I see no difference with using dev or release on ocaml file. You look in there and you see a .cmx. Was it compiler with -opaque? You don't see it from the file name.

I also never feel the need to look into _build when I develop OCaml code (unless I'm debugging the build system, which is not something we expect our users to do often). Why would it be different for Coq?

Actually, this method won't produce installable packages that are both using vos/vo right?

Having "both" serve no purpose, you only want the most complete one. In the approach I propose, it is always called vo. Print Assumption & Co can be updated to tell you that you are loading incomplete files.

Anyway, being able to to pass flags to coqc via profile is a good feature anyway, so maybe we should focus on that here.

gares · 2020-06-12T08:23:02Z

I've re targeted the PR to just support coq.flags. It works for me as well and requires no discussion about the design of alternative Coq backends.

ejgallego

Looks pretty good, some tweaks are possible. @rgrinberg how does this look to you?

While I finish the review, this is missing:

changelog entry
documentation update.

gares · 2020-06-19T11:16:15Z

ping

rgrinberg

Looks good and should be good to go for 2.7.

src/dune/dune_env.ml

src/dune/dune_env.mli

ejgallego · 2020-06-19T21:54:34Z

Thanks @rgrinberg ; @gares this looks good then, I will merge once the two comments are addressed.

Signed-off-by: Enrico Tassi <[email protected]>

gares · 2020-06-20T12:45:34Z

should be OK now

ejgallego · 2020-06-20T16:07:11Z

doc/dune-files.rst

@@ -1345,6 +1345,9 @@ Fields supported in ``<settings>`` are:
 - ``(odoc <fields>)``. This allows to pass options to Odoc, see
  :ref:`odoc-options` for more details.

+- ``(coq (flags <flags>))``. This allows to pass options to Coq, see
+  :ref:`coq-theory` for more details.
+


Nit: we could indeed also mention in the (coq.theory ...) documentation that flags can be set in env

@NathanReb

…lugin, dune-private-libs and dune-glob (2.7.0) CHANGES: - Write intermediate files in a `.mdx` folder for each `mdx` stanza to prevent the corresponding actions to be executed as part of the `@all` alias (ocaml/dune#3659, @NathanReb) - Read Coq flags from `env` (ocaml/dune#3547 , fixes ocaml/dune#3486, @gares) - Allow bisect_ppx to be enabled/disabled via dune-workspace. (ocaml/dune#3404, @stephanieyou) - Formatting of dune files is now done in the executing dune process instead of in a separate process. (ocaml/dune#3536, @nojb) - Add a `--debug-artifact-substution` flag to help debug problem with version not being captured by `dune-build-info` (ocaml/dune#3589, @jeremiedimino) - Allow the use of the `context_name` variable in the `enabled_if` fields of executable(s) and install stanzas. (ocaml/dune#3568, fixes ocaml/dune#3566, @voodoos) - Fix compatibility with OCaml 4.12.0 when compiling empty archives; no .a file is generated. (ocaml/dune#3576, @dra27) - `$ dune utop` no longer tries to load optional libraries that are unavailable (ocaml/dune#3612, fixes ocaml/dune#3188, @anuragsoni) - Fix dune-build-info on 4.10.0+flambda (ocaml/dune#3599, @emillon, @jeremiedimino). - Allow multiple libraries with `inline_tests` to be defined in the same directory (ocaml/dune#3621, @rgrinberg) - Run exit hooks in jsoo separate compilation mode (ocaml/dune#3626, fixes ocaml/dune#3622, @rgrinberg) - Add (alias ...), (mode ...) fields to (copy_fields ...) stanza (ocaml/dune#3631, @nojb) - (copy_files ...) now supports copying files from outside the workspace using absolute file names (ocaml/dune#3639, @nojb) - Dune does not use `ocamlc` as an intermediary to call C compiler anymore. Configuration flags `ocamlc_cflags` and `ocamlc_cppflags` are always prepended to the compiler arguments. (ocaml/dune#3565, fixes ocaml/dune#3346, @voodoos) - Revert the build optimization in ocaml/dune#2268. This optimization slows down building individual executables when they're part of an `executables` stanza group (ocaml/dune#3644, @rgrinberg) - Use `{dev}` rather than `{pinned}` in the generated `.opam` file. (ocaml/dune#3647, @kit-ty-kate) - Insert correct extension name when editing `dune-project` files. Previously, dune would just insert the stanza name. (ocaml/dune#3649, fixes ocaml/dune#3624, @rgrinberg) - Fix crash when evaluating an `mdx` stanza that depends on unavailable packages. (ocaml/dune#3650, @craigfe) - Fix typo in `cache-check-probablity` field in dune config files. This field now requires 2.7 as it wasn't usable before this version. (ocaml/dune#3652, @edwintorok) - Add `"odoc" {with-doc}` to the dependencies in the generated `.opam` files. (ocaml/dune#3667, @kit-ty-kate) - Do not allow user actions to capture dune's stdin (ocaml/dune#3677, fixes ocaml/dune#3672, @rgrinberg) - `(subdir ...)` stanzas can now appear in dune files used via `(include ...)`. (ocaml/dune#3676, @nojb)

@NathanReb

…lugin, dune-private-libs and dune-glob (2.7.0) CHANGES: - Write intermediate files in a `.mdx` folder for each `mdx` stanza to prevent the corresponding actions to be executed as part of the `@all` alias (ocaml/dune#3659, @NathanReb) - Read Coq flags from `env` (ocaml/dune#3547 , fixes ocaml/dune#3486, @gares) - Add instrumentation framework to toggle instrumentation by `bisect_ppx`, `landmarks`, etc, via dune-workspace and/or the command-line. (ocaml/dune#3404, ocaml/dune#3526 @stephanieyou, @nojb) - Formatting of dune files is now done in the executing dune process instead of in a separate process. (ocaml/dune#3536, @nojb) - Add a `--debug-artifact-substution` flag to help debug problem with version not being captured by `dune-build-info` (ocaml/dune#3589, @jeremiedimino) - Allow the use of the `context_name` variable in the `enabled_if` fields of executable(s) and install stanzas. (ocaml/dune#3568, fixes ocaml/dune#3566, @voodoos) - Fix compatibility with OCaml 4.12.0 when compiling empty archives; no .a file is generated. (ocaml/dune#3576, @dra27) - `$ dune utop` no longer tries to load optional libraries that are unavailable (ocaml/dune#3612, fixes ocaml/dune#3188, @anuragsoni) - Fix dune-build-info on 4.10.0+flambda (ocaml/dune#3599, @emillon, @jeremiedimino). - Allow multiple libraries with `inline_tests` to be defined in the same directory (ocaml/dune#3621, @rgrinberg) - Run exit hooks in jsoo separate compilation mode (ocaml/dune#3626, fixes ocaml/dune#3622, @rgrinberg) - Add (alias ...), (mode ...) fields to (copy_fields ...) stanza (ocaml/dune#3631, @nojb) - (copy_files ...) now supports copying files from outside the workspace using absolute file names (ocaml/dune#3639, @nojb) - Dune does not use `ocamlc` as an intermediary to call C compiler anymore. Configuration flags `ocamlc_cflags` and `ocamlc_cppflags` are always prepended to the compiler arguments. (ocaml/dune#3565, fixes ocaml/dune#3346, @voodoos) - Revert the build optimization in ocaml/dune#2268. This optimization slows down building individual executables when they're part of an `executables` stanza group (ocaml/dune#3644, @rgrinberg) - Use `{dev}` rather than `{pinned}` in the generated `.opam` file. (ocaml/dune#3647, @kit-ty-kate) - Insert correct extension name when editing `dune-project` files. Previously, dune would just insert the stanza name. (ocaml/dune#3649, fixes ocaml/dune#3624, @rgrinberg) - Fix crash when evaluating an `mdx` stanza that depends on unavailable packages. (ocaml/dune#3650, @craigfe) - Fix typo in `cache-check-probablity` field in dune config files. This field now requires 2.7 as it wasn't usable before this version. (ocaml/dune#3652, @edwintorok) - Add `"odoc" {with-doc}` to the dependencies in the generated `.opam` files. (ocaml/dune#3667, @kit-ty-kate) - Do not allow user actions to capture dune's stdin (ocaml/dune#3677, fixes ocaml/dune#3672, @rgrinberg) - `(subdir ...)` stanzas can now appear in dune files used via `(include ...)`. (ocaml/dune#3676, @nojb)

ejgallego reviewed Jun 11, 2020

View reviewed changes

gares force-pushed the coq-backend branch from 34e7973 to 530f106 Compare June 12, 2020 08:19

gares changed the title ~~[coq] pick backend from profile~~ [coq] pick flags from profile Jun 12, 2020

gares force-pushed the coq-backend branch from 530f106 to d1e1cfa Compare June 12, 2020 08:21

gares marked this pull request as ready for review June 12, 2020 08:21

ejgallego requested changes Jun 12, 2020

View reviewed changes

gares requested review from emillon, nojb and rgrinberg as code owners June 15, 2020 09:14

gares force-pushed the coq-backend branch from 4813075 to a9c0e64 Compare June 15, 2020 09:15

gares requested a review from ejgallego June 15, 2020 09:15

ejgallego self-assigned this Jun 19, 2020

rgrinberg approved these changes Jun 19, 2020

View reviewed changes

src/dune/dune_env.ml Outdated Show resolved Hide resolved

src/dune/dune_env.mli Outdated Show resolved Hide resolved

gares force-pushed the coq-backend branch from 31730f8 to 02c4b00 Compare June 20, 2020 12:44

gares added 3 commits June 20, 2020 14:45

[coq] env suppor for coq.flags

3d0c47e

Signed-off-by: Enrico Tassi <[email protected]>

[doc] document (coq (flags ..))

e37737a

Signed-off-by: Enrico Tassi <[email protected]>

update changelog

8ce5ed8

Signed-off-by: Enrico Tassi <[email protected]>

gares added 2 commits June 20, 2020 14:45

remove type alias in dune_env

dcae115

Signed-off-by: Enrico Tassi <[email protected]>

target version 2.7

80f4f41

Signed-off-by: Enrico Tassi <[email protected]>

gares force-pushed the coq-backend branch from 02c4b00 to 80f4f41 Compare June 20, 2020 12:45

ejgallego reviewed Jun 20, 2020

View reviewed changes

ejgallego approved these changes Jun 20, 2020

View reviewed changes

ejgallego merged commit 0160bfd into ocaml:master Jun 20, 2020

gares deleted the coq-backend branch June 20, 2020 17:04

rgrinberg mentioned this pull request Aug 14, 2020

[new release] dune-build-info, dune, dune-configurator, dune-action-plugin, dune-private-libs and dune-glob (2.7.0) ocaml/opam-repository#17005

Merged

Alizter added the coq label Jun 6, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[coq] pick flags from profile #3547

[coq] pick flags from profile #3547

gares commented Jun 11, 2020 •

edited

Loading

ejgallego commented Jun 11, 2020

ejgallego commented Jun 11, 2020

ejgallego Jun 11, 2020

gares commented Jun 11, 2020

ejgallego Jun 11, 2020

ejgallego commented Jun 11, 2020

gares commented Jun 11, 2020

ejgallego commented Jun 11, 2020

gares commented Jun 11, 2020 •

edited

Loading

ejgallego commented Jun 11, 2020

gares commented Jun 11, 2020

gares commented Jun 12, 2020

ejgallego left a comment •

edited

Loading

gares commented Jun 19, 2020

rgrinberg left a comment

ejgallego commented Jun 19, 2020

gares commented Jun 20, 2020

ejgallego Jun 20, 2020

[coq] pick flags from profile #3547

[coq] pick flags from profile #3547

Conversation

gares commented Jun 11, 2020 • edited Loading

ejgallego commented Jun 11, 2020

ejgallego commented Jun 11, 2020

ejgallego Jun 11, 2020

Choose a reason for hiding this comment

gares commented Jun 11, 2020

ejgallego Jun 11, 2020

Choose a reason for hiding this comment

ejgallego commented Jun 11, 2020

gares commented Jun 11, 2020

ejgallego commented Jun 11, 2020

gares commented Jun 11, 2020 • edited Loading

ejgallego commented Jun 11, 2020

gares commented Jun 11, 2020

gares commented Jun 12, 2020

ejgallego left a comment • edited Loading

Choose a reason for hiding this comment

gares commented Jun 19, 2020

rgrinberg left a comment

Choose a reason for hiding this comment

ejgallego commented Jun 19, 2020

gares commented Jun 20, 2020

ejgallego Jun 20, 2020

Choose a reason for hiding this comment

gares commented Jun 11, 2020 •

edited

Loading

gares commented Jun 11, 2020 •

edited

Loading

ejgallego left a comment •

edited

Loading