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

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.
 
@@ -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
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1696,7 +1697,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 +1709,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

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)

src/dune/dune_file.ml

@@ -1992,7 +1992,7 @@ module Coq = struct
 
   let syntax =
     Dune_lang.Syntax.create ~name:"coq" ~desc:"the coq extension (experimental)"
-      [ (0, 1) ]
+      [ (0, 2) ]
 
   let coq_public_decode =
     map_validate
@@ -2041,11 +2041,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

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"

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)

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)

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)

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)

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)

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)

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)