Merge pull request #12733 from rlepigre/fix-12638

Coq/Rocq: fix handling of (modules_flags ...).

Author: Alizter

doc/changes/fixed/12733.md

@@ -0,0 +1 @@
+- Allow multiple modules in `(modules_flags ...)`, in `coq.theory` (#12733, @rlepigre)

doc/coq.rst

@@ -378,9 +378,11 @@ The Coq lang can be modified by adding the following to a
 The supported Coq language versions (not the version of Coq) are:
 
 - ``0.11``: Support for the ``(coqdoc_header ...)`` and ``(coqdoc_footer ...)``
-  fields, and for ``_CoqProject`` file generation.
+  fields, for ``_CoqProject`` file generation, and multiple modules in
+  ``(modules_flags ...)``.
 - ``0.10``: Support for the ``(coqdep_flags ...)`` field.
-- ``0.9``: Support for per-module flags with the ``(modules_flags ...)``` field.
+- ``0.9``: Support for per-module flags with the ``(modules_flags ...)`` field,
+  limited to a single module due to a bug.
 - ``0.8``: Support for composition with installed Coq theories;
   support for ``vos`` builds.
 

src/dune_rules/coq/coq_stanza.ml

@@ -250,7 +250,8 @@ module Theory = struct
       mod_, flags
     ;;
 
-    let decode = enter (repeat decode_pair)
+    let decode = repeat (enter decode_pair)
+    let broken_decode = enter (repeat decode_pair)
   end
 
   let decode =
@@ -268,9 +269,13 @@ module Theory = struct
               ~check:(Dune_lang.Syntax.since coq_syntax (0, 11))
        and+ modules = Ordered_set_lang.field "modules"
        and+ modules_flags =
-         field_o
-           "modules_flags"
-           (Dune_lang.Syntax.since coq_syntax (0, 9) >>> Per_file.decode)
+         let* version = Dune_lang.Syntax.get_exn coq_syntax in
+         if version >= (0, 11)
+         then field_o "modules_flags" Per_file.decode
+         else
+           field_o
+             "modules_flags"
+             (Dune_lang.Syntax.since coq_syntax (0, 9) >>> Per_file.broken_decode)
        and+ enabled_if = Enabled_if.decode ~allowed_vars:Any ~since:None ()
        and+ buildable = Buildable.decode
        and+ coqdep_flags =

test/blackbox-tests/test-cases/coq/modules_flags.t

@@ -0,0 +1,46 @@
+Reproducing test case for https://github.com/ocaml/dune/issues/12638.
+
+  $ cat > dune-project <<EOF
+  > (lang dune 3.21)
+  > (using coq 0.11)
+  > EOF
+
+  $ touch foo.v bar.v
+
+  $ cat > dune <<EOF
+  > (coq.theory
+  >  (name a)
+  >  (modules_flags
+  >   (foo (-w -deprecated-since-8.15))
+  >   (bar (-w -deprecated-since-8.16))))
+  > EOF
+
+  $ dune build foo.vo && tail -n 1 _build/log | ./scrub_coq_args.sh | grep deprecated-since
+  -w -deprecated-since-8.15
+  $ dune build bar.vo && tail -n 1 _build/log | ./scrub_coq_args.sh | grep deprecated-since
+  -w -deprecated-since-8.16
+  $ dune clean
+
+  $ cat > dune-project <<EOF
+  > (lang dune 3.21)
+  > (using coq 0.10)
+  > EOF
+  $ dune build
+  File "dune", line 5, characters 2-35:
+  5 |   (bar (-w -deprecated-since-8.16))))
+        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  Error: Too many arguments for "modules_flags"
+  [1]
+  $ dune clean
+
+  $ cat > dune <<EOF
+  > (coq.theory
+  >  (name a)
+  >  (modules_flags
+  >   (bar (-w -deprecated-since-8.16))))
+  > EOF
+
+  $ dune build foo.vo && tail -n 1 _build/log | ./scrub_coq_args.sh | grep deprecated-since
+  [1]
+  $ dune build bar.vo && tail -n 1 _build/log | ./scrub_coq_args.sh | grep deprecated-since
+  -w -deprecated-since-8.16