Merge pull request #3283 from ejgallego/coq+version_theory_field

[coq] Check version for Coq's `(theories ...)` field.
ocaml · Mar 24, 2020 · 574c1e2 · 574c1e2
2 parents ca54525 + 8dababa
commit 574c1e2
Show file tree

Hide file tree

Showing 10 changed files with 34 additions and 25 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1,3 +1,3 @@
-(lang dune 2.4)
+(lang dune 2.5)
 
-(using coq 0.1)
+(using coq 0.2)