From 2ad2a504c4895833cdfe0990f01982d944595e91 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Mon, 4 Nov 2024 13:31:38 +0100 Subject: [PATCH 1/2] Add support for coqdep flags. This includes the following: - A [coqdep_flags] field in the [env] stanza (under [coq]). - A [coqdep_flags] field in the [coq.theory] stanza. Signed-off-by: Rodolphe Lepigre --- doc/changes/11094.md | 2 ++ doc/coq.rst | 10 ++++++ src/dune_rules/coq/coq_env.ml | 12 +++++-- src/dune_rules/coq/coq_env.mli | 3 ++ src/dune_rules/coq/coq_flags.ml | 7 ++-- src/dune_rules/coq/coq_flags.mli | 1 + src/dune_rules/coq/coq_rules.ml | 34 +++++++++++++++++-- src/dune_rules/coq/coq_stanza.ml | 7 ++++ src/dune_rules/coq/coq_stanza.mli | 1 + .../coq/coqdep-flags.t/dune-project | 2 ++ .../coq/coqdep-flags.t/dune.disabled | 4 +++ .../test-cases/coq/coqdep-flags.t/run.t | 29 ++++++++++++++++ .../coq/coqdep-flags.t/theories/bar.v | 3 ++ .../coq/coqdep-flags.t/theories/dune.flags | 3 ++ .../coq/coqdep-flags.t/theories/dune.noflags | 2 ++ .../coq/coqdep-flags.t/theories/foo.v | 1 + .../test-cases/coq/coqtop/coqtop-root.t/run.t | 2 +- .../test-cases/coq/github3624.t | 2 +- .../workspaces/workspace-env.t/run.t | 1 + 19 files changed, 117 insertions(+), 9 deletions(-) create mode 100644 doc/changes/11094.md create mode 100644 test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune.disabled create mode 100644 test/blackbox-tests/test-cases/coq/coqdep-flags.t/run.t create mode 100644 test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/bar.v create mode 100644 test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.flags create mode 100644 test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.noflags create mode 100644 test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/foo.v diff --git a/doc/changes/11094.md b/doc/changes/11094.md new file mode 100644 index 00000000000..99101b3b07e --- /dev/null +++ b/doc/changes/11094.md @@ -0,0 +1,2 @@ +- Add a `coqdep_flags` field to the `coq` field of the `env` stanza, and to the `coq.theory` stanza, allowing to configure `coqdep` flags. + (#11094, @rlepigre) diff --git a/doc/coq.rst b/doc/coq.rst index 7088a827917..ea16f585a26 100644 --- a/doc/coq.rst +++ b/doc/coq.rst @@ -67,6 +67,7 @@ The Coq theory stanza is very similar in form to the OCaml (plugins ) (flags ) (modules_flags ) + (coqdep_flags ) (coqdoc_flags ) (stdlib ) (mode ) @@ -134,6 +135,11 @@ The semantics of the fields are: ...)`` as to propagate the default flags. (Appeared in :ref:`Coq lang 0.9`) +- ```` are extra user-configurable flags passed to ``coqdep``. The + default value for ``:standard`` is empty. (Appeared in :ref:`Coq + lang 0.10`) + + - ```` are extra user-configurable flags passed to ``coqdoc``. The default value for ``:standard`` is ``--toc``. The ``--html`` or ``--latex`` flags are passed separately depending on which mode is target. See the section @@ -347,6 +353,7 @@ The Coq lang can be modified by adding the following to a The supported Coq language versions (not the version of Coq) are: +- ``0.10``: Support for the ``(coqdep_flags ...)`` field. - ``0.9``: Support for per-module flags with the ``(module_flags ...)``` field. - ``0.8``: Support for composition with installed Coq theories; support for ``vos`` builds. @@ -833,6 +840,9 @@ with the following values for ````: - ``(flags )``: The default flags passed to ``coqc``. The default value is ``-q``. Values set here become the ``:standard`` value in the ``(coq.theory (flags ))`` field. +- ``(coqdep_flags )``: The default flags passed to ``coqdep``. The default + value is empty. Values set here become the ``:standard`` value in the + ``(coq.theory (coqdep_flags ))`` field. - ``(coqdoc_flags )``: The default flags passed to ``coqdoc``. The default value is ``--toc``. Values set here become the ``:standard`` value in the ``(coq.theory (coqdoc_flags ))`` field. diff --git a/src/dune_rules/coq/coq_env.ml b/src/dune_rules/coq/coq_env.ml index 28bf530870a..8afa7d2bbf5 100644 --- a/src/dune_rules/coq/coq_env.ml +++ b/src/dune_rules/coq/coq_env.ml @@ -3,16 +3,19 @@ open Dune_lang.Decoder type t = { flags : Ordered_set_lang.Unexpanded.t + ; coqdep_flags : Ordered_set_lang.Unexpanded.t ; coqdoc_flags : Ordered_set_lang.Unexpanded.t } let default = { flags = Ordered_set_lang.Unexpanded.standard + ; coqdep_flags = Ordered_set_lang.Unexpanded.standard ; coqdoc_flags = Ordered_set_lang.Unexpanded.standard } ;; let flags t = t.flags +let coqdep_flags t = t.coqdep_flags let coqdoc_flags t = t.coqdoc_flags let decode = @@ -24,15 +27,20 @@ let decode = Ordered_set_lang.Unexpanded.field "flags" ~check:(Dune_lang.Syntax.since Stanza.syntax (2, 7)) + and+ coqdep_flags = + Ordered_set_lang.Unexpanded.field + "coqdep_flags" + ~check:(Dune_lang.Syntax.since Stanza.syntax (3, 17)) and+ coqdoc_flags = Ordered_set_lang.Unexpanded.field "coqdoc_flags" ~check:(Dune_lang.Syntax.since Stanza.syntax (3, 13)) in - { flags; coqdoc_flags })) + { flags; coqdep_flags; coqdoc_flags })) ;; -let equal { flags; coqdoc_flags } t = +let equal { flags; coqdep_flags; coqdoc_flags } t = Ordered_set_lang.Unexpanded.equal flags t.flags + && Ordered_set_lang.Unexpanded.equal coqdep_flags t.coqdep_flags && Ordered_set_lang.Unexpanded.equal coqdoc_flags t.coqdoc_flags ;; diff --git a/src/dune_rules/coq/coq_env.mli b/src/dune_rules/coq/coq_env.mli index 9a371099e2d..e5ce999bb48 100644 --- a/src/dune_rules/coq/coq_env.mli +++ b/src/dune_rules/coq/coq_env.mli @@ -11,6 +11,9 @@ val default : t (** Flags for Coq binaries. *) val flags : t -> Ordered_set_lang.Unexpanded.t +(** Flags for coqdep *) +val coqdep_flags : t -> Ordered_set_lang.Unexpanded.t + (** Flags for coqdoc *) val coqdoc_flags : t -> Ordered_set_lang.Unexpanded.t diff --git a/src/dune_rules/coq/coq_flags.ml b/src/dune_rules/coq/coq_flags.ml index d7e5c412024..16ce8972582 100644 --- a/src/dune_rules/coq/coq_flags.ml +++ b/src/dune_rules/coq/coq_flags.ml @@ -2,13 +2,14 @@ open Import type t = { coq_flags : string list + ; coqdep_flags : string list ; coqdoc_flags : string list } -let default = { coq_flags = [ "-q" ]; coqdoc_flags = [ "--toc" ] } +let default = { coq_flags = [ "-q" ]; coqdep_flags = []; coqdoc_flags = [ "--toc" ] } -let dump { coq_flags; coqdoc_flags } = +let dump { coq_flags; coqdep_flags; coqdoc_flags } = List.map ~f:Dune_lang.Encoder.(pair string (list string)) - [ "coq_flags", coq_flags; "coqdoc_flags", coqdoc_flags ] + [ "coq_flags", coq_flags; "coqdep_flags", coqdep_flags; "coqdoc_flags", coqdoc_flags ] ;; diff --git a/src/dune_rules/coq/coq_flags.mli b/src/dune_rules/coq/coq_flags.mli index 37deba94b92..7f249549b44 100644 --- a/src/dune_rules/coq/coq_flags.mli +++ b/src/dune_rules/coq/coq_flags.mli @@ -1,5 +1,6 @@ type t = { coq_flags : string list + ; coqdep_flags : string list ; coqdoc_flags : string list } diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml index f1fdf923b60..6b4db3b1bb9 100644 --- a/src/dune_rules/coq/coq_rules.ml +++ b/src/dune_rules/coq/coq_rules.ml @@ -141,6 +141,15 @@ let coq_env = x.coq_flags in Expander.expand_and_eval_set expander (Coq_env.flags config.coq) ~standard + and+ coqdep_flags = + let standard = + let+ x = Action_builder.of_memo_join parent in + x.coqdep_flags + in + Expander.expand_and_eval_set + expander + (Coq_env.coqdep_flags config.coq) + ~standard and+ coqdoc_flags = let standard = let+ x = Action_builder.of_memo_join parent in @@ -151,7 +160,7 @@ let coq_env = (Coq_env.coqdoc_flags config.coq) ~standard in - { Coq_flags.coq_flags; coqdoc_flags }) + { Coq_flags.coq_flags; coqdep_flags; coqdoc_flags }) in fun ~dir -> (let* () = Memo.return () in @@ -176,6 +185,16 @@ let coq_flags ~dir ~stanza_flags ~per_file_flags ~expander = Expander.expand_and_eval_set expander flags_to_expand ~standard ;; +let coqdep_flags ~dir ~stanza_coqdep_flags ~expander = + Expander.expand_and_eval_set + expander + stanza_coqdep_flags + ~standard: + (Action_builder.map + ~f:(fun { Coq_flags.coqdep_flags; _ } -> coqdep_flags) + (coq_env ~dir)) +;; + let coqdoc_flags ~dir ~stanza_coqdoc_flags ~expander = Expander.expand_and_eval_set expander @@ -474,6 +493,7 @@ let setup_coqdep_for_theory_rule ~ml_flags ~mlpack_rule ~boot_flags + ~stanza_coqdep_flags coq_modules = (* coqdep needs the full source + plugin's mlpack to be present :( *) @@ -484,7 +504,15 @@ let setup_coqdep_for_theory_rule ; Deps sources ] in - let coqdep_flags = Command.Args.Dyn boot_flags :: file_flags in + let extra_coqdep_flags = + (* Standard flags for coqdep *) + let open Action_builder.O in + let* expander = Action_builder.of_memo @@ Super_context.expander sctx ~dir in + coqdep_flags ~dir ~stanza_coqdep_flags ~expander + in + let coqdep_flags = + Command.Args.Dyn boot_flags :: Command.Args.dyn extra_coqdep_flags :: file_flags + in let stdout_to = dep_theory_file ~dir ~wrapper_name in let* coqdep = Super_context.resolve_program_memo @@ -968,6 +996,7 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) = ~ml_flags ~mlpack_rule ~boot_flags + ~stanza_coqdep_flags:s.coqdep_flags coq_modules >>> Memo.parallel_iter coq_modules @@ -1189,6 +1218,7 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Extraction.t ~ml_flags ~mlpack_rule ~boot_flags + ~stanza_coqdep_flags:Ordered_set_lang.Unexpanded.standard [ coq_module ] >>> setup_coqc_rule ~scope diff --git a/src/dune_rules/coq/coq_stanza.ml b/src/dune_rules/coq/coq_stanza.ml index cd0bcc6ffae..3bc1f06d066 100644 --- a/src/dune_rules/coq/coq_stanza.ml +++ b/src/dune_rules/coq/coq_stanza.ml @@ -14,6 +14,7 @@ let coq_syntax = ; (0, 7), `Since (3, 7) ; (0, 8), `Since (3, 8) ; (0, 9), `Since (3, 16) + ; (0, 10), `Since (3, 17) ] ;; @@ -169,6 +170,7 @@ module Theory = struct ; boot : bool ; enabled_if : Blang.t ; buildable : Buildable.t + ; coqdep_flags : Ordered_set_lang.Unexpanded.t ; coqdoc_flags : Ordered_set_lang.Unexpanded.t } @@ -249,6 +251,10 @@ module Theory = struct (Dune_lang.Syntax.since coq_syntax (0, 9) >>> Per_file.decode) and+ enabled_if = Enabled_if.decode ~allowed_vars:Any ~since:None () and+ buildable = Buildable.decode + and+ coqdep_flags = + Ordered_set_lang.Unexpanded.field + "coqdep_flags" + ~check:(Dune_lang.Syntax.since coq_syntax (0, 10)) and+ coqdoc_flags = Ordered_set_lang.Unexpanded.field "coqdoc_flags" @@ -266,6 +272,7 @@ module Theory = struct ; boot ; buildable ; enabled_if + ; coqdep_flags ; coqdoc_flags }) ;; diff --git a/src/dune_rules/coq/coq_stanza.mli b/src/dune_rules/coq/coq_stanza.mli index 744a28ac34c..bc243b3e77b 100644 --- a/src/dune_rules/coq/coq_stanza.mli +++ b/src/dune_rules/coq/coq_stanza.mli @@ -35,6 +35,7 @@ module Theory : sig ; boot : bool ; enabled_if : Blang.t ; buildable : Buildable.t + ; coqdep_flags : Ordered_set_lang.Unexpanded.t ; coqdoc_flags : Ordered_set_lang.Unexpanded.t } diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune-project b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune-project new file mode 100644 index 00000000000..a7bab4a1ced --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.17) +(using coq 0.10) diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune.disabled b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune.disabled new file mode 100644 index 00000000000..5334a5e7660 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/dune.disabled @@ -0,0 +1,4 @@ +(env + (_ + (coq + (coqdep_flags (:standard --global-flag1 --global-flag2))))) diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/run.t b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/run.t new file mode 100644 index 00000000000..218bb9f6ad1 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/run.t @@ -0,0 +1,29 @@ +By default the coqdep flags are empty. + + $ cp theories/dune.noflags theories/dune + $ dune build theories/.basic.theory.d + +We use non-exising coqdep flags, so compilation fails. + + $ mv dune.disabled dune + $ dune build theories/.basic.theory.d + *** Warning: unknown option --global-flag1 + *** Warning: unknown option --global-flag2 + +We then add more flags locally to the theory. + + $ rm -f theories/dune + $ cp theories/dune.flags theories/dune + $ dune build theories/.basic.theory.d + *** Warning: unknown option --global-flag1 + *** Warning: unknown option --global-flag2 + *** Warning: unknown option --local-flag1 + *** Warning: unknown option --local-flag2 + +Finally we remove the toplevel dune file which sets some flags, but keep the +theory-local flags only. + + $ rm -f dune + $ dune build theories/.basic.theory.d + *** Warning: unknown option --local-flag1 + *** Warning: unknown option --local-flag2 diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/bar.v b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/bar.v new file mode 100644 index 00000000000..4627b76131c --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/bar.v @@ -0,0 +1,3 @@ +From basic Require Import foo. + +Definition mynum (i : mynat) := 3. diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.flags b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.flags new file mode 100644 index 00000000000..ad1476c36f5 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.flags @@ -0,0 +1,3 @@ +(coq.theory + (name basic) + (coqdep_flags (:standard --local-flag1 --local-flag2))) diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.noflags b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.noflags new file mode 100644 index 00000000000..e442495a247 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/dune.noflags @@ -0,0 +1,2 @@ +(coq.theory + (name basic)) diff --git a/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/foo.v b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/foo.v new file mode 100644 index 00000000000..53e0ce1b152 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/coqdep-flags.t/theories/foo.v @@ -0,0 +1 @@ +Definition mynat := nat. diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t index 9f4313633ad..4927115eeb6 100644 --- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t @@ -45,5 +45,5 @@ This test is currently broken due to the workspace resolution being faulty #5899 1 | (coq.theory 2 | (name foo)) Error: 'coq.theory' is available only when coq is enabled in the dune-project - file. You must enable it using (using coq 0.9) in your dune-project file. + file. You must enable it using (using coq 0.10) in your dune-project file. [1] diff --git a/test/blackbox-tests/test-cases/coq/github3624.t b/test/blackbox-tests/test-cases/coq/github3624.t index 874ae07cfe0..02fd701f04b 100644 --- a/test/blackbox-tests/test-cases/coq/github3624.t +++ b/test/blackbox-tests/test-cases/coq/github3624.t @@ -17,5 +17,5 @@ good when the coq extension is not enabled. 1 | (coq.theory 2 | (name foo)) Error: 'coq.theory' is available only when coq is enabled in the dune-project - file. You must enable it using (using coq 0.9) in your dune-project file. + file. You must enable it using (using coq 0.10) in your dune-project file. [1] diff --git a/test/blackbox-tests/test-cases/workspaces/workspace-env.t/run.t b/test/blackbox-tests/test-cases/workspaces/workspace-env.t/run.t index 094d6d20d76..313c25faf49 100644 --- a/test/blackbox-tests/test-cases/workspaces/workspace-env.t/run.t +++ b/test/blackbox-tests/test-cases/workspaces/workspace-env.t/run.t @@ -13,6 +13,7 @@ Workspaces also allow you to set the env for a context: (menhir_flags ()) (menhir_explain ()) (coq_flags (-q)) + (coqdep_flags ()) (coqdoc_flags (--toc)) (js_of_ocaml_flags ()) (js_of_ocaml_build_runtime_flags ()) From b2c3d9326d94b0841fbdf363c63410ea3bb2e415 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Wed, 13 Nov 2024 10:12:35 +0100 Subject: [PATCH 2/2] Warn about coqdep_flags in the documentation. Signed-off-by: Rodolphe Lepigre --- doc/coq.rst | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/doc/coq.rst b/doc/coq.rst index ea16f585a26..6ddb391358d 100644 --- a/doc/coq.rst +++ b/doc/coq.rst @@ -136,8 +136,9 @@ The semantics of the fields are: lang 0.9`) - ```` are extra user-configurable flags passed to ``coqdep``. The - default value for ``:standard`` is empty. (Appeared in :ref:`Coq - lang 0.10`) + default value for ``:standard`` is empty. This field exists for transient + use-cases, in particular disabling ``coqdep`` warnings, but it should not be + used in normal operations. (Appeared in :ref:`Coq lang 0.10`) - ```` are extra user-configurable flags passed to ``coqdoc``. The @@ -842,7 +843,9 @@ with the following values for ````: ``(coq.theory (flags ))`` field. - ``(coqdep_flags )``: The default flags passed to ``coqdep``. The default value is empty. Values set here become the ``:standard`` value in the - ``(coq.theory (coqdep_flags ))`` field. + ``(coq.theory (coqdep_flags ))`` field. As noted in the documentation + of the ``(coq.theory (coqdep_flags ))`` field, changing the ``coqdep`` + flags is discouraged. - ``(coqdoc_flags )``: The default flags passed to ``coqdoc``. The default value is ``--toc``. Values set here become the ``:standard`` value in the ``(coq.theory (coqdoc_flags ))`` field.