[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 19, 2020 · d087d3f · d087d3f
1 parent 839398f
commit d087d3f
Show file tree

Hide file tree

Showing 9 changed files with 13 additions and 9 deletions.
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)