[coq] Check version for Coq's (theories ...) field.
#3283
Conversation
ejgallego
force-pushed
the
coq+version_theory_field
branch
2 times, most recently
from
d087d3f to
a9800dd
Compare
src/dune/dune_file.ml
Outdated
| and+ theories = field "theories" (repeat Coq_lib_name.decode) ~default:[] | ||
| and+ theories = | ||
| field "theories" | ||
| ( Dune_lang.Syntax.since Stanza.syntax (2, 5) |
There was a problem hiding this comment.
Why don't you version it using the version of the coq extension? (syntax in this case).
I just noticed that you're using dune's versions for other fields as well. I might be missing something obvious here.
There was a problem hiding this comment.
The main reason is that we declared "0.1" a moving, unsupported target, but you are right this is an ugly hack.
I wasn't planning to version coq lang until we do the first call for "beta testers", the idea was then to set the version to 0.99 , and then if no problem arises declare 1.0 and have regular support.
I think this can happen in 2.5 ; but I'd be happy to bump Coq lang to 0.2 and remove these checks instead (also looking forward to #3270 )
There was a problem hiding this comment.
Note that after #3270 if we bump Coq to 0.2 we will have to bump dune lang too anyways.
|
Sure, but that still seems like the right way to go (require dune 2.5 and 0.2 for coq).
@diml what do you think we should do in this case? My impressions is that we need an official policy with regards to versioning that we follow mechanically. Otherwise, it becomes confusing to users.
…On Mar 19, 2020, 11:27 PM -0700, Emilio Jesús Gallego Arias ***@***.***>, wrote:
@ejgallego commented on this pull request.
In src/dune/dune_file.ml:
> @@ -2045,7 +2045,11 @@ module Coq = struct
and+ modules = modules_field "modules"
and+ libraries =
field "libraries" (repeat (located Lib_name.decode)) ~default:[]
- and+ theories = field "theories" (repeat Coq_lib_name.decode) ~default:[]
+ and+ theories =
+ field "theories"
+ ( Dune_lang.Syntax.since Stanza.syntax (2, 5)
Note that after #3270 if we bump Coq to 0.2 we will have to bump dune lang too anyways.
—
You are receiving this because your review was requested.
Reply to this email directly, view it on GitHub, or unsubscribe.
|
Ok, will bump Coq to 0.2 then, and keep the 2.5 bump. |
ejgallego
force-pushed
the
coq+version_theory_field
branch
from
a9800dd to
5d3aeec
Compare
|
The versioning of coq fields should be controlled by the version of the coq extension, not the version of the dune language. For extensions that are still in the |
ejgallego
force-pushed
the
coq+version_theory_field
branch
from
5d3aeec to
6a3363a
Compare
|
Sounds good, even if the 0.x versions of Coq are not meant to stay for long, let's bump in this case. |
Users willing to use this indeed need to bump their `dune-project` version. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
ejgallego
force-pushed
the
coq+version_theory_field
branch
from
6a3363a to
8dababa
Compare
…lugin, dune-private-libs and dune-glob (2.5.0) CHANGES: - Add a `--release` option meaning the same as `-p` but without the package filtering. This is useful for custom `dune` invocation in opam files where we don't want `-p` (ocaml/dune#3260, @diml) - Fix a bug introduced in 2.4.0 causing `.bc` programs to be built with `-custom` by default (ocaml/dune#3269, fixes ocaml/dune#3262, @diml) - Allow contexts to be defined with local switches in workspace files (ocaml/dune#3265, fix ocaml/dune#3264, @rgrinberg) - Delay expansion errors until the rule is used to build something (ocaml/dune#3261, fix ocaml/dune#3252, @rgrinberg, @diml) - [coq] Support for theory dependencies and compositional builds using new field `(theories ...)` (ocaml/dune#2053, @ejgallego, @rgrinberg) - From now on, each version of a syntax extension must be explicitely tied to a minimum version of the dune language. Inconsistent versions in a `dune-project` will trigger a warning for version <=2.4 and an error for versions >2.4 of the dune language. (ocaml/dune#3270, fixes ocaml/dune#2957, @voodoos) - [coq] Bump coq lang version to 0.2. New coq features presented this release require this version of the coq lang. (ocaml/dune#3283, @ejgallego) - Prevent installation of public executables disabled using the `enabled_if` field. Installation will now simply skip such executables instead of raising an error. (ocaml/dune#3195, @voodoos) - `dune upgrade` will now try to upgrade projects using versions <2.0 to version 2.0 of the dune language. (ocaml/dune#3174, @voodoos) - Add a `top` command to integrate dune with any toplevel, not just utop. It is meant to be used with the new `#use_output` directive of OCaml 4.11 (ocaml/dune#2952, @mbernat, @diml) - Allow per-package `version` in generated `opam` files (ocaml/dune#3287, @toots) - [coq] Introduce the `coq.extraction` stanza. It can be used to extract OCaml sources (ocaml/dune#3299, fixes ocaml/dune#2178, @rgrinberg) - Load ppx rewriters in dune utop and add pps field to toplevel stanza. Ppx extensions will now be usable in the toplevel (ocaml/dune#3266, fixes ocaml/dune#346, @stephanieyou) - Add a `(subdir ..)` stanza to allow evaluating stanzas in sub directories. (ocaml/dune#3268, @rgrinberg) - Fix a bug preventing one from running inline tests in multiple modes (ocaml/dune#3352, @diml) - Allow the use of the `%{profile}` variable in the `enabled_if` field of the library stanza. (ocaml/dune#3344, @mrmr1993) - Allow the use of `%{ocaml_version}` variable in `enabled_if` field of the library stanza. (ocaml/dune#3339, @voodoos) - Fix dune build freezing on MacOS when cache is enabled. (ocaml/dune#3249, fixes #ocaml/dune#2973, @artempyanykh)
Users willing to use this indeed need to bump their
dune-projectversion.