[coq] Check version for Coq's (theories ...) field.

Users willing to use this indeed need to bump their `dune-project` version. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
ocaml · Mar 20, 2020 · a9800dd · a9800dd
1 parent b332148
commit a9800dd
Show file tree

Hide file tree

Showing 11 changed files with 17 additions and 13 deletions.
diff --git a/doc/dune-files.rst b/doc/dune-files.rst
@@ -12,7 +12,7 @@ like:
 
 .. code:: scheme
 
-          (lang dune 2.4)
+          (lang dune 2.5)
 
 Additionally, they can contains the following stanzas.
 
@@ -1696,7 +1696,7 @@ a typical ``dune-workspace`` file looks like:
 
 .. code:: scheme
 
-    (lang dune 2.4)
+    (lang dune 2.5)
     (context (opam (switch 4.02.3)))
     (context (opam (switch 4.03.0)))
     (context (opam (switch 4.04.0)))
@@ -1708,7 +1708,7 @@ containing exactly:
 
 .. code:: scheme
 
-    (lang dune 2.4)
+    (lang dune 2.5)
     (context default)
 
 This allows you to use an empty ``dune-workspace`` file to mark the root of your

diff --git a/doc/opam.rst b/doc/opam.rst
@@ -94,7 +94,7 @@ configuration will tell ``dune`` to generate two opam files: ``cohttp.opam`` and
 
 .. code:: scheme
 
-   (lang dune 2.4)
+   (lang dune 2.5)
    (name cohttp)
 
    (generate_opam_files true)

diff --git a/src/dune/dune_file.ml b/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)
+           >>> 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/src/dune/stanza.ml b/src/dune/stanza.ml
@@ -6,7 +6,7 @@ module Parser = struct
   type nonrec t = string * t list Dune_lang.Decoder.t
 end
 
-let latest_version = (2, 4)
+let latest_version = (2, 5)
 
 let syntax =
   Dune_lang.Syntax.create ~name:"dune" ~desc:"the dune language"

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)
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)
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)
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)
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)
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)
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)