Merge pull request #9280 from Alizter/ps/branch/feature_coq___coqdoc_…

…flags_in_env_stanza

feature(coq): coqdoc_flags in env stanza

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 in
+  let coq_flags = node >>= Env_node.coq_flags in
   let js_of_ocaml = node >>= Env_node.js_of_ocaml in
   let open Action_builder.O in
   let+ o_dump =
@@ -32,9 +32,7 @@ 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 =
-    let+ flags = Action_builder.of_memo_join coq_flags in
-    [ "coq_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+ jsoo_dump =
     let* jsoo = Action_builder.of_memo js_of_ocaml in
     Js_of_ocaml.Flags.dump jsoo.flags

doc/changes/9280_coq_env.md

@@ -0,0 +1,2 @@
+- Add `coqdoc_flags` field to `coq` field of `env` stanza allowing the setting of
+  workspace-wide defaults for `coqdoc_flags`. (#9280, fixes #9139, @Alizter)

doc/coq.rst

@@ -788,3 +788,19 @@ 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 (flags <flags>))`` allows passing options to Coq. See :ref:`coq-theory`
+- ``(coq <coq_fields>)`` allow passing options to Coq. See :ref:`coq-env`
   for more details.
 
 - ``(formatting <settings>)`` allows the user to set auto-formatting in the

src/dune_rules/coq/coq_env.ml

@@ -0,0 +1,38 @@
+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
+;;

src/dune_rules/coq/coq_env.mli

@@ -0,0 +1,18 @@
+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

src/dune_rules/coq/coq_flags.ml

@@ -0,0 +1,14 @@
+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 ]
+;;

src/dune_rules/coq/coq_flags.mli

@@ -0,0 +1,7 @@
+type t =
+  { coq_flags : string list
+  ; coqdoc_flags : string list
+  }
+
+val default : t
+val dump : t -> Dune_lang.t list

src/dune_rules/coq/coq_rules.ml

@@ -126,12 +126,27 @@ let select_native_mode ~sctx ~dir (buildable : Coq_stanza.Buildable.t) =
 ;;
 
 let coq_flags ~dir ~stanza_flags ~expander ~sctx =
-  let open Action_builder.O in
-  let* standard =
-    Action_builder.of_memo
-    @@ (Super_context.env_node ~dir sctx |> Memo.bind ~f:Env_node.coq)
+  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
   in
-  Expander.expand_and_eval_set expander stanza_flags ~standard
+  Expander.expand_and_eval_set
+    expander
+    stanza_coqdoc_flags
+    ~standard:
+      (Action_builder.map ~f:(fun { Coq_flags.coqdoc_flags; _ } -> coqdoc_flags) standard)
 ;;
 
 let theory_coqc_flag lib =
@@ -697,9 +712,11 @@ 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 : Ordered_set_lang.Unexpanded.t
+    ; coq : Coq_env.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
-    && Ordered_set_lang.Unexpanded.equal coq t.coq
+    && Coq_env.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 = Ordered_set_lang.Unexpanded.standard
+    ; coq = Coq_env.default
     ; format_config = None
     ; error_on_use = None
     ; warn_on_load = None
@@ -220,15 +220,6 @@ 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)
   ;;
@@ -248,7 +239,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_field
+    and+ coq = Coq_env.decode
     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 : Ordered_set_lang.Unexpanded.t
+    ; coq : Coq_env.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,6 +52,7 @@ 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,10 +8,6 @@ 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
@@ -24,7 +20,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 : Coq.t Action_builder.t Memo.Lazy.t
+  ; coq_flags : Coq_flags.t Action_builder.t Memo.Lazy.t
   ; format_config : Format_config.t Memo.Lazy.t
   ; bin_annot : bool Memo.Lazy.t
   }
@@ -46,7 +42,7 @@ let set_format_config t format_config =
 ;;
 
 let odoc t = Memo.Lazy.force t.odoc |> Action_builder.of_memo_join
-let coq t = Memo.Lazy.force t.coq
+let coq_flags t = Memo.Lazy.force t.coq_flags
 let bin_annot t = Memo.Lazy.force t.bin_annot
 
 let expand_str_lazy expander sw =
@@ -214,12 +210,25 @@ let make
         let+ { warnings } = warnings in
         { warnings = Option.value config.odoc.warnings ~default:warnings })
   in
-  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)
+  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 })
   in
   let format_config =
     inherited_if_absent
@@ -247,7 +256,7 @@ let make
   ; js_of_ocaml
   ; menhir_flags
   ; odoc
-  ; coq
+  ; coq_flags
   ; format_config
   ; bin_annot
   }

src/dune_rules/env_node.mli

@@ -10,10 +10,6 @@ module Odoc : sig
   type t = { warnings : warnings }
 end
 
-module Coq : sig
-  type t = string list
-end
-
 type t
 
 val make
@@ -45,7 +41,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 : t -> Coq.t Action_builder.t Memo.t
+val coq_flags : t -> Coq_flags.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/coq/coqdoc-flags.t

@@ -0,0 +1,23 @@
+Testing the coqdoc flags field of the env stanza.
+
+  $ cat > dune-project <<EOF
+  > (lang dune 3.13)
+  > (using coq 0.8)
+  > EOF
+
+  $ cat > dune <<EOF
+  > (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

test/blackbox-tests/test-cases/workspaces/workspace-env.t/run.t

@@ -12,6 +12,7 @@ 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 ())