From 6b1f6b82f6dd518cd9adf15e27ed964e6cd72600 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Sun, 16 Nov 2025 15:16:24 +0100 Subject: [PATCH] Fix #12638. Signed-off-by: Rodolphe Lepigre --- doc/changes/fixed/12733.md | 1 + doc/coq.rst | 6 ++- src/dune_rules/coq/coq_stanza.ml | 13 ++++-- .../test-cases/coq/modules_flags.t | 46 +++++++++++++++++++ 4 files changed, 60 insertions(+), 6 deletions(-) create mode 100644 doc/changes/fixed/12733.md create mode 100644 test/blackbox-tests/test-cases/coq/modules_flags.t diff --git a/doc/changes/fixed/12733.md b/doc/changes/fixed/12733.md new file mode 100644 index 00000000000..35d4acadfac --- /dev/null +++ b/doc/changes/fixed/12733.md @@ -0,0 +1 @@ +- Allow multiple modules in `(modules_flags ...)`, in `coq.theory` (#12733, @rlepigre) diff --git a/doc/coq.rst b/doc/coq.rst index f89a70e1931..01cca1a3754 100644 --- a/doc/coq.rst +++ b/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. diff --git a/src/dune_rules/coq/coq_stanza.ml b/src/dune_rules/coq/coq_stanza.ml index 32154a3437f..e5dd8c7e489 100644 --- a/src/dune_rules/coq/coq_stanza.ml +++ b/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 = diff --git a/test/blackbox-tests/test-cases/coq/modules_flags.t b/test/blackbox-tests/test-cases/coq/modules_flags.t new file mode 100644 index 00000000000..4019e3f449f --- /dev/null +++ b/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 < (lang dune 3.21) + > (using coq 0.11) + > EOF + + $ touch foo.v bar.v + + $ cat > dune < (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 < (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 < (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