[3.12] Revert #9280

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

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

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 <coq_fields>)`` field with the following
-values for ``<coq_fields>``:
-
-- ``(flags <flags>)``: The default flags passed to ``coqc``. The default value
-  is ``-q``. Values set here become the ``:standard`` value in the
-  ``(coq.theory (flags <flags>))`` field. 
-- ``(coqdoc_flags <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 <flags>))`` field.

doc/stanzas/env.rst

@@ -62,7 +62,7 @@ Fields supported in ``<settings>`` are:
 - ``(odoc <fields>)`` allows passing options to ``odoc``. See
   :ref:`odoc-options` for more details.
 
-- ``(coq <coq_fields>)`` allow passing options to Coq. See :ref:`coq-env`
+- ``(coq (flags <flags>))`` allows passing options to Coq. See :ref:`coq-theory`
   for more details.
 
 - ``(formatting <settings>)`` allows the user to set auto-formatting in the

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

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

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

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

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
   }

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

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 ())