From 7a428ab898bce33bbe30965062130054d736a2e7 Mon Sep 17 00:00:00 2001 From: Etienne Millon Date: Wed, 29 Nov 2023 12:01:09 +0100 Subject: [PATCH 1/3] Revert "doc(coq): document coqdoc_flags in env stanza" This reverts commit b3d2bf1cb3fc46ae9eaa975cc0e01c2ee9d7ed82. Signed-off-by: Etienne Millon --- doc/coq.rst | 16 ---------------- doc/stanzas/env.rst | 2 +- 2 files changed, 1 insertion(+), 17 deletions(-) diff --git a/doc/coq.rst b/doc/coq.rst index e322f20cfda..0c52c6ea77b 100644 --- a/doc/coq.rst +++ b/doc/coq.rst @@ -788,19 +788,3 @@ configuration. These are: See :doc:`concepts/variables` for more information on variables supported by Dune. - - -.. _coq-env: - -Coq Environment Fields ----------------------- - -The :ref:`dune-env` stanza has a ``(coq )`` field 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. -- ``(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. \ No newline at end of file diff --git a/doc/stanzas/env.rst b/doc/stanzas/env.rst index 370ce3adbbb..7c45e7e0e50 100644 --- a/doc/stanzas/env.rst +++ b/doc/stanzas/env.rst @@ -62,7 +62,7 @@ Fields supported in ```` are: - ``(odoc )`` allows passing options to ``odoc``. See :ref:`odoc-options` for more details. -- ``(coq )`` allow passing options to Coq. See :ref:`coq-env` +- ``(coq (flags ))`` allows passing options to Coq. See :ref:`coq-theory` for more details. - ``(formatting )`` allows the user to set auto-formatting in the From 2a501c2f7e83f5994a29f71eeed08e8b8b3801ef Mon Sep 17 00:00:00 2001 From: Etienne Millon Date: Wed, 29 Nov 2023 12:01:13 +0100 Subject: [PATCH 2/3] Revert "feature(coq): coqdoc_flags in env stanza" This reverts commit b545564dc45366901f337deb08686f6746a22f2e. Signed-off-by: Etienne Millon --- bin/printenv.ml | 6 ++- src/dune_rules/coq/coq_env.ml | 38 ------------------- src/dune_rules/coq/coq_env.mli | 18 --------- src/dune_rules/coq/coq_flags.ml | 14 ------- src/dune_rules/coq/coq_flags.mli | 7 ---- src/dune_rules/coq/coq_rules.ml | 29 +++----------- src/dune_rules/dune_env.ml | 17 +++++++-- src/dune_rules/dune_env.mli | 2 +- src/dune_rules/dune_rules.ml | 1 - src/dune_rules/env_node.ml | 35 +++++++---------- src/dune_rules/env_node.mli | 6 ++- .../test-cases/coq/coqdoc-flags.t | 23 ----------- .../workspaces/workspace-env.t/run.t | 1 - 13 files changed, 42 insertions(+), 155 deletions(-) delete mode 100644 src/dune_rules/coq/coq_env.ml delete mode 100644 src/dune_rules/coq/coq_env.mli delete mode 100644 src/dune_rules/coq/coq_flags.ml delete mode 100644 src/dune_rules/coq/coq_flags.mli delete mode 100644 test/blackbox-tests/test-cases/coq/coqdoc-flags.t diff --git a/bin/printenv.ml b/bin/printenv.ml index 9c55d80e38a..cd1dda86c75 100644 --- a/bin/printenv.ml +++ b/bin/printenv.ml @@ -13,7 +13,7 @@ let dump sctx ~dir = let foreign_flags = node >>| Env_node.foreign_flags in let link_flags = node >>= Env_node.link_flags in let menhir_flags = node >>| Env_node.menhir_flags in - let coq_flags = node >>= Env_node.coq_flags in + let coq_flags = node >>= Env_node.coq in let js_of_ocaml = node >>= Env_node.js_of_ocaml in let open Action_builder.O in let+ o_dump = @@ -32,7 +32,9 @@ let dump sctx ~dir = and+ menhir_dump = let+ flags = Action_builder.of_memo_join menhir_flags in [ "menhir_flags", flags ] |> List.map ~f:Dune_lang.Encoder.(pair string (list string)) - and+ coq_dump = Action_builder.of_memo_join coq_flags >>| Dune_rules.Coq_flags.dump + and+ coq_dump = + let+ flags = Action_builder.of_memo_join coq_flags in + [ "coq_flags", flags ] |> List.map ~f:Dune_lang.Encoder.(pair string (list string)) and+ jsoo_dump = let* jsoo = Action_builder.of_memo js_of_ocaml in Js_of_ocaml.Flags.dump jsoo.flags diff --git a/src/dune_rules/coq/coq_env.ml b/src/dune_rules/coq/coq_env.ml deleted file mode 100644 index 28bf530870a..00000000000 --- a/src/dune_rules/coq/coq_env.ml +++ /dev/null @@ -1,38 +0,0 @@ -open Import -open Dune_lang.Decoder - -type t = - { flags : Ordered_set_lang.Unexpanded.t - ; coqdoc_flags : Ordered_set_lang.Unexpanded.t - } - -let default = - { flags = Ordered_set_lang.Unexpanded.standard - ; coqdoc_flags = Ordered_set_lang.Unexpanded.standard - } -;; - -let flags t = t.flags -let coqdoc_flags t = t.coqdoc_flags - -let decode = - field - "coq" - ~default - (fields - (let+ flags = - Ordered_set_lang.Unexpanded.field - "flags" - ~check:(Dune_lang.Syntax.since Stanza.syntax (2, 7)) - and+ coqdoc_flags = - Ordered_set_lang.Unexpanded.field - "coqdoc_flags" - ~check:(Dune_lang.Syntax.since Stanza.syntax (3, 13)) - in - { flags; coqdoc_flags })) -;; - -let equal { flags; coqdoc_flags } t = - Ordered_set_lang.Unexpanded.equal flags t.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 deleted file mode 100644 index 9a371099e2d..00000000000 --- a/src/dune_rules/coq/coq_env.mli +++ /dev/null @@ -1,18 +0,0 @@ -open Import - -(** Environment for Coq. *) -type t - -val equal : t -> t -> bool - -(** Default environment for Coq. *) -val default : t - -(** Flags for Coq binaries. *) -val flags : t -> Ordered_set_lang.Unexpanded.t - -(** Flags for coqdoc *) -val coqdoc_flags : t -> Ordered_set_lang.Unexpanded.t - -(** Parser for env stanza. *) -val decode : t Dune_lang.Decoder.fields_parser diff --git a/src/dune_rules/coq/coq_flags.ml b/src/dune_rules/coq/coq_flags.ml deleted file mode 100644 index d7e5c412024..00000000000 --- a/src/dune_rules/coq/coq_flags.ml +++ /dev/null @@ -1,14 +0,0 @@ -open Import - -type t = - { coq_flags : string list - ; coqdoc_flags : string list - } - -let default = { coq_flags = [ "-q" ]; coqdoc_flags = [ "--toc" ] } - -let dump { coq_flags; coqdoc_flags } = - List.map - ~f:Dune_lang.Encoder.(pair string (list string)) - [ "coq_flags", coq_flags; "coqdoc_flags", coqdoc_flags ] -;; diff --git a/src/dune_rules/coq/coq_flags.mli b/src/dune_rules/coq/coq_flags.mli deleted file mode 100644 index 37deba94b92..00000000000 --- a/src/dune_rules/coq/coq_flags.mli +++ /dev/null @@ -1,7 +0,0 @@ -type t = - { coq_flags : string list - ; coqdoc_flags : string list - } - -val default : t -val dump : t -> Dune_lang.t list diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml index 6461e0d9c46..2bb912bed52 100644 --- a/src/dune_rules/coq/coq_rules.ml +++ b/src/dune_rules/coq/coq_rules.ml @@ -126,27 +126,12 @@ let select_native_mode ~sctx ~dir (buildable : Coq_stanza.Buildable.t) = ;; let coq_flags ~dir ~stanza_flags ~expander ~sctx = - let standard = - let open Memo.O in - Super_context.env_node ~dir sctx >>= Env_node.coq_flags |> Action_builder.of_memo_join - in - Expander.expand_and_eval_set - expander - stanza_flags - ~standard: - (Action_builder.map ~f:(fun { Coq_flags.coq_flags; _ } -> coq_flags) standard) -;; - -let coqdoc_flags ~dir ~stanza_coqdoc_flags ~expander ~sctx = - let standard = - let open Memo.O in - Super_context.env_node ~dir sctx >>= Env_node.coq_flags |> Action_builder.of_memo_join + let open Action_builder.O in + let* standard = + Action_builder.of_memo + @@ (Super_context.env_node ~dir sctx |> Memo.bind ~f:Env_node.coq) in - Expander.expand_and_eval_set - expander - stanza_coqdoc_flags - ~standard: - (Action_builder.map ~f:(fun { Coq_flags.coqdoc_flags; _ } -> coqdoc_flags) standard) + Expander.expand_and_eval_set expander stanza_flags ~standard ;; let theory_coqc_flag lib = @@ -712,11 +697,9 @@ let setup_coqdoc_rules ~sctx ~dir ~theories_deps (s : Coq_stanza.Theory.t) coq_m in let extra_coqdoc_flags = (* Standard flags for coqdoc *) + let standard = Action_builder.return [ "--toc" ] in let open Action_builder.O in let* expander = Action_builder.of_memo @@ Super_context.expander sctx ~dir in - let standard = - coqdoc_flags ~dir ~stanza_coqdoc_flags:s.coqdoc_flags ~expander ~sctx - in Expander.expand_and_eval_set expander s.coqdoc_flags ~standard in [ Command.Args.S file_flags diff --git a/src/dune_rules/dune_env.ml b/src/dune_rules/dune_env.ml index ba6e8c5c7e5..f6858599fda 100644 --- a/src/dune_rules/dune_env.ml +++ b/src/dune_rules/dune_env.ml @@ -82,7 +82,7 @@ module Stanza = struct ; menhir_flags : Ordered_set_lang.Unexpanded.t option ; odoc : Odoc.t ; js_of_ocaml : Ordered_set_lang.Unexpanded.t Js_of_ocaml.Env.t - ; coq : Coq_env.t + ; coq : Ordered_set_lang.Unexpanded.t ; format_config : Format_config.t option ; error_on_use : User_message.t option ; warn_on_load : User_message.t option @@ -123,7 +123,7 @@ module Stanza = struct && Option.equal Inline_tests.equal inline_tests t.inline_tests && Option.equal Ordered_set_lang.Unexpanded.equal menhir_flags t.menhir_flags && Odoc.equal odoc t.odoc - && Coq_env.equal coq t.coq + && Ordered_set_lang.Unexpanded.equal coq t.coq && Option.equal Format_config.equal format_config t.format_config && Js_of_ocaml.Env.equal js_of_ocaml t.js_of_ocaml && Option.equal User_message.equal error_on_use t.error_on_use @@ -143,7 +143,7 @@ module Stanza = struct ; menhir_flags = None ; odoc = Odoc.empty ; js_of_ocaml = Js_of_ocaml.Env.empty - ; coq = Coq_env.default + ; coq = Ordered_set_lang.Unexpanded.standard ; format_config = None ; error_on_use = None ; warn_on_load = None @@ -220,6 +220,15 @@ module Stanza = struct (Dune_lang.Syntax.since Stanza.syntax (3, 0) >>> Js_of_ocaml.Env.decode) ;; + let coq_flags = Ordered_set_lang.Unexpanded.field "flags" + + let coq_field = + field + "coq" + ~default:Ordered_set_lang.Unexpanded.standard + (Dune_lang.Syntax.since Stanza.syntax (2, 7) >>> fields coq_flags) + ;; + let bin_annot = field_o "bin_annot" (Dune_lang.Syntax.since Stanza.syntax (3, 8) >>> bool) ;; @@ -239,7 +248,7 @@ module Stanza = struct and+ menhir_flags = menhir_flags ~since:(Some (2, 1)) and+ odoc = odoc_field and+ js_of_ocaml = js_of_ocaml_field - and+ coq = Coq_env.decode + and+ coq = coq_field and+ format_config = Format_config.field ~since:(2, 8) and+ bin_annot = bin_annot in { flags diff --git a/src/dune_rules/dune_env.mli b/src/dune_rules/dune_env.mli index d6785d97820..1272313022d 100644 --- a/src/dune_rules/dune_env.mli +++ b/src/dune_rules/dune_env.mli @@ -33,7 +33,7 @@ module Stanza : sig ; menhir_flags : Ordered_set_lang.Unexpanded.t option ; odoc : Odoc.t ; js_of_ocaml : Ordered_set_lang.Unexpanded.t Js_of_ocaml.Env.t - ; coq : Coq_env.t + ; coq : Ordered_set_lang.Unexpanded.t ; format_config : Format_config.t option ; error_on_use : User_message.t option ; warn_on_load : User_message.t option diff --git a/src/dune_rules/dune_rules.ml b/src/dune_rules/dune_rules.ml index fea6d9edaee..29ef9698ce1 100644 --- a/src/dune_rules/dune_rules.ml +++ b/src/dune_rules/dune_rules.ml @@ -52,7 +52,6 @@ module Coq_module = Coq_module module Coq_sources = Coq_sources module Coq_lib_name = Coq_lib_name module Coq_lib = Coq_lib -module Coq_flags = Coq_flags module Command = Command module Clflags = Clflags module Dune_project = Dune_project diff --git a/src/dune_rules/env_node.ml b/src/dune_rules/env_node.ml index b44fb207163..8027d0551c0 100644 --- a/src/dune_rules/env_node.ml +++ b/src/dune_rules/env_node.ml @@ -8,6 +8,10 @@ module Odoc = struct type t = { warnings : warnings } end +module Coq = struct + type t = string list +end + type t = { scope : Scope.t ; local_binaries : File_binding.Expanded.t list Memo.Lazy.t @@ -20,7 +24,7 @@ type t = ; menhir_flags : string list Action_builder.t Memo.Lazy.t ; odoc : Odoc.t Action_builder.t Memo.Lazy.t ; js_of_ocaml : string list Action_builder.t Js_of_ocaml.Env.t Memo.Lazy.t - ; coq_flags : Coq_flags.t Action_builder.t Memo.Lazy.t + ; coq : Coq.t Action_builder.t Memo.Lazy.t ; format_config : Format_config.t Memo.Lazy.t ; bin_annot : bool Memo.Lazy.t } @@ -42,7 +46,7 @@ let set_format_config t format_config = ;; let odoc t = Memo.Lazy.force t.odoc |> Action_builder.of_memo_join -let coq_flags t = Memo.Lazy.force t.coq_flags +let coq t = Memo.Lazy.force t.coq let bin_annot t = Memo.Lazy.force t.bin_annot let expand_str_lazy expander sw = @@ -210,25 +214,12 @@ let make let+ { warnings } = warnings in { warnings = Option.value config.odoc.warnings ~default:warnings }) in - let coq_flags : Coq_flags.t Action_builder.t Memo.Lazy.t = - inherited - ~field:coq_flags - ~root:(Action_builder.return Coq_flags.default) - (fun coq_flags -> - let+ expander = Memo.Lazy.force expander in - let open Action_builder.O in - let* { coq_flags; coqdoc_flags } = coq_flags in - let+ coq_flags = - let standard = Action_builder.return coq_flags in - Expander.expand_and_eval_set expander (Coq_env.flags config.coq) ~standard - and+ coqdoc_flags = - let standard = Action_builder.return coqdoc_flags in - Expander.expand_and_eval_set - expander - (Coq_env.coqdoc_flags config.coq) - ~standard - in - { Coq_flags.coq_flags; coqdoc_flags }) + let default_coq_flags = Action_builder.return [ "-q" ] in + let coq : Coq.t Action_builder.t Memo.Lazy.t = + inherited ~field:coq ~root:default_coq_flags (fun flags -> + let+ expander = Memo.Lazy.force expander in + let standard = flags in + Expander.expand_and_eval_set expander config.coq ~standard) in let format_config = inherited_if_absent @@ -256,7 +247,7 @@ let make ; js_of_ocaml ; menhir_flags ; odoc - ; coq_flags + ; coq ; format_config ; bin_annot } diff --git a/src/dune_rules/env_node.mli b/src/dune_rules/env_node.mli index b736c092741..0b756a21d93 100644 --- a/src/dune_rules/env_node.mli +++ b/src/dune_rules/env_node.mli @@ -10,6 +10,10 @@ module Odoc : sig type t = { warnings : warnings } end +module Coq : sig + type t = string list +end + type t val make @@ -41,7 +45,7 @@ val local_binaries : t -> File_binding.Expanded.t list Memo.t val artifacts : t -> Artifacts.t Memo.t val odoc : t -> Odoc.t Action_builder.t -val coq_flags : t -> Coq_flags.t Action_builder.t Memo.t +val coq : t -> Coq.t Action_builder.t Memo.t val menhir_flags : t -> string list Action_builder.t val format_config : t -> Format_config.t Memo.t val set_format_config : t -> Format_config.t -> t diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-flags.t b/test/blackbox-tests/test-cases/coq/coqdoc-flags.t deleted file mode 100644 index 19822fc4099..00000000000 --- a/test/blackbox-tests/test-cases/coq/coqdoc-flags.t +++ /dev/null @@ -1,23 +0,0 @@ -Testing the coqdoc flags field of the env stanza. - - $ cat > dune-project < (lang dune 3.13) - > (using coq 0.8) - > EOF - - $ cat > dune < (env - > (_ - > (coq - > (coqdoc_flags :standard -toc-depth 2)))) - > (coq.theory - > (name a)) - > EOF - - $ dune build @doc - - $ tail _build/log -n 1 | ./scrub_coq_args.sh | sed 's/.*coq/coq/' - coqdoc - coq/theories Coq - -R . a --toc -toc-depth 2 --html -d - a.html 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 44443030bdd..0454369f1d9 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 @@ -12,7 +12,6 @@ Workspaces also allow you to set the env for a context: (link_flags ()) (menhir_flags ()) (coq_flags (-q)) - (coqdoc_flags (--toc)) (js_of_ocaml_flags ()) (js_of_ocaml_build_runtime_flags ()) (js_of_ocaml_link_flags ()) From de83f6681d14b31782304cb4e0ec61cb3c6240b1 Mon Sep 17 00:00:00 2001 From: Etienne Millon Date: Wed, 29 Nov 2023 12:04:46 +0100 Subject: [PATCH 3/3] Add changelog Signed-off-by: Etienne Millon --- CHANGES.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index d19cb6c64e4..8690d2228e6 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,8 @@ +3.12.1 (unreleased) +------------------- + +- Revert unintended inclusion of #9280 (@emillon) + 3.12.0 (2023-11-28) ------------------- @@ -40,9 +45,6 @@ - Add `test_` prefix to default test name in `dune init project` (#9257, fixes #9131, @9sako6) -- Add `coqdoc_flags` field to `coq` field of `env` stanza allowing the setting - of workspace-wide defaults for `coqdoc_flags`. (#9280, fixes #9139, @Alizter) - - [coq rules] Be more tolerant when coqc --print-version / --config don't work properly, and fallback to a reasonable default. This fixes problems when building Coq projects with `(stdlib no)` and likely other cases. (#8966, fix