diff --git a/CHANGES.md b/CHANGES.md index db24531dc2c..ffb54464e41 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -16,12 +16,15 @@ Unreleased - [coq] Support for theory dependencies and compositional builds using new field `(theories ...)` (#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. (#3270, fixes #2957, @voodoos) +- [coq] Bump coq-lang version to 0.2, put new features under it + (#3283, @ejgallego) + 2.4.0 (06/03/2020) ------------------ diff --git a/doc/dune-files.rst b/doc/dune-files.rst index 9ad05dd6f09..729f215f1a3 100644 --- a/doc/dune-files.rst +++ b/doc/dune-files.rst @@ -1526,17 +1526,18 @@ in the ``dune-project`` file. For example: .. code:: scheme - (using coq 0.1) + (using coq 0.2) This will enable support for the ``coq.theory`` stanza in the current project. If the language version is absent, dune will automatically add this line with the latest Coq version to the project file once a ``(coq.theory ...)`` stanza is used anywhere. -The only version supported is ``0.1`` and it doesn't provide any kind -of guarantees with respect to stability, however, as implementation of -features progresses, we hope to bump ``0.1`` to ``1.0`` soon. The 1.0 -version will commit to a stable set of functionality; features marked -``1.0`` below are expected to reach 1.0 unchanged. +The supported Coq language versions are ``0.1``, and ``0.2`` which +adds support for the ``theories`` field. We don't provide any +guarantees with respect to stability yet, however, as implementation +of features progresses, we hope reach ``1.0`` soon. The ``1.0`` +version will commit to a stable set of functionality; all the features +below are expected to reach 1.0 unchanged or minimally modified. The basic form for defining Coq libraries is very similar to the OCaml form: @@ -1589,7 +1590,7 @@ The stanza will build all ``.v`` files on the given directory. The semantics of domain). We will lift this restriction in the future. Note that composition with the Coq's standard library is supported, but in this case the ``Coq`` prefix will be made available in a qualified - way. + way. Since Coq's lang version ``0.2``. Recursive qualification of modules ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/src/dune/dune_file.ml b/src/dune/dune_file.ml index 91a3b2c84b9..429ce7bf175 100644 --- a/src/dune/dune_file.ml +++ b/src/dune/dune_file.ml @@ -1994,7 +1994,8 @@ module Coq = struct let syntax = Dune_lang.Syntax.create ~name:"coq" ~desc:"the coq extension (experimental)" - [ ((0, 1), `Since (1, 9)) ] + [ ((0, 1), `Since (1, 9)) + ; ((0, 2), `Since (2, 5)) ] let coq_public_decode = map_validate @@ -2043,11 +2044,15 @@ module Coq = struct and+ synopsis = field_o "synopsis" string and+ flags = Ordered_set_lang.Unexpanded.field "flags" and+ boot = - field_b "boot" ~check:(Dune_lang.Syntax.since Stanza.syntax (2, 3)) + field_b "boot" ~check:(Dune_lang.Syntax.since syntax (0, 2)) 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 syntax (0, 2) + >>> repeat Coq_lib_name.decode ) + ~default:[] and+ enabled_if = enabled_if ~since:None in let package = select_deprecation ~package ~public in { name diff --git a/test/blackbox-tests/test-cases/coq/compose_boot/dune-project b/test/blackbox-tests/test-cases/coq/compose_boot/dune-project index c1fd9ec6785..9ef6b81a34a 100644 --- a/test/blackbox-tests/test-cases/coq/compose_boot/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose_boot/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.4) +(lang dune 2.5) -(using coq 0.1) +(using coq 0.2) diff --git a/test/blackbox-tests/test-cases/coq/compose_cycle/dune-project b/test/blackbox-tests/test-cases/coq/compose_cycle/dune-project index c1fd9ec6785..9ef6b81a34a 100644 --- a/test/blackbox-tests/test-cases/coq/compose_cycle/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose_cycle/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.4) +(lang dune 2.5) -(using coq 0.1) +(using coq 0.2) diff --git a/test/blackbox-tests/test-cases/coq/compose_plugin/dune-project b/test/blackbox-tests/test-cases/coq/compose_plugin/dune-project index c1fd9ec6785..9ef6b81a34a 100644 --- a/test/blackbox-tests/test-cases/coq/compose_plugin/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose_plugin/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.4) +(lang dune 2.5) -(using coq 0.1) +(using coq 0.2) diff --git a/test/blackbox-tests/test-cases/coq/compose_simple/dune-project b/test/blackbox-tests/test-cases/coq/compose_simple/dune-project index c1fd9ec6785..9ef6b81a34a 100644 --- a/test/blackbox-tests/test-cases/coq/compose_simple/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose_simple/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.4) +(lang dune 2.5) -(using coq 0.1) +(using coq 0.2) diff --git a/test/blackbox-tests/test-cases/coq/compose_two_scopes/dune-project b/test/blackbox-tests/test-cases/coq/compose_two_scopes/dune-project index c1fd9ec6785..9ef6b81a34a 100644 --- a/test/blackbox-tests/test-cases/coq/compose_two_scopes/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose_two_scopes/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.4) +(lang dune 2.5) -(using coq 0.1) +(using coq 0.2) diff --git a/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/dune-project b/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/dune-project index c1fd9ec6785..9ef6b81a34a 100644 --- a/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose_two_scopes/vendor/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.4) +(lang dune 2.5) -(using coq 0.1) +(using coq 0.2) diff --git a/test/blackbox-tests/test-cases/coq/public_dep_on_private/dune-project b/test/blackbox-tests/test-cases/coq/public_dep_on_private/dune-project index c1fd9ec6785..9ef6b81a34a 100644 --- a/test/blackbox-tests/test-cases/coq/public_dep_on_private/dune-project +++ b/test/blackbox-tests/test-cases/coq/public_dep_on_private/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.4) +(lang dune 2.5) -(using coq 0.1) +(using coq 0.2)