feature(coq): add coqdoc_flags field to coq.theory

This allows users to further configure the flags sent to coqdoc. It is
an ordered set lang with :standard being just `--toc` as is currently
passed today.

Signed-off-by: Ali Caglayan <alizter@gmail.com>

CHANGES.md

@@ -20,6 +20,9 @@ Unreleased
 - Load the host context `findlib.conf` when cross-compiling (#7428, fixes
   #1701, @rgrinberg, @anmonteiro)
 
+- Add a `coqdoc_flags` field to the `coq.theory` stanza allowing the user to
+  pass extra arguments to `coqdoc`. (#17015, @Alizter)
+
 - Resolve `ppx_runtime_libraries` in the target context when cross compiling
   (#7450, fixes #2794, @anmonteiro)
 

src/dune_rules/coq/coq_rules.ml

@@ -602,8 +602,17 @@ let setup_coqdoc_rules ~sctx ~dir ~theories_deps (s : Coq_stanza.Theory.t)
              | `Html -> "--html"
              | `Latex -> "--latex"
            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
+             Expander.expand_and_eval_set expander s.coqdoc_flags ~standard
+           in
            [ Command.Args.S file_flags
-           ; A "--toc"
+           ; Command.Args.dyn extra_coqdoc_flags
            ; A mode_flag
            ; A "-d"
            ; Path (Path.build doc_dir)

src/dune_rules/coq/coq_stanza.ml

@@ -116,6 +116,7 @@ module Theory = struct
     ; boot : bool
     ; enabled_if : Blang.t
     ; buildable : Buildable.t
+    ; coqdoc_flags : Ordered_set_lang.Unexpanded.t
     }
 
   let coq_public_decode =
@@ -173,7 +174,11 @@ module Theory = struct
          field_b "boot" ~check:(Dune_lang.Syntax.since coq_syntax (0, 2))
        and+ modules = Stanza_common.modules_field "modules"
        and+ enabled_if = Enabled_if.decode ~allowed_vars:Any ~since:None ()
-       and+ buildable = Buildable.decode in
+       and+ buildable = Buildable.decode
+       and+ coqdoc_flags =
+         Ordered_set_lang.Unexpanded.field "coqdoc_flags"
+           ~check:(Dune_lang.Syntax.since coq_syntax (0, 8))
+       in
        (* boot libraries cannot depend on other theories *)
        check_boot_has_no_deps boot buildable;
        let package = merge_package_public ~package ~public in
@@ -185,6 +190,7 @@ module Theory = struct
        ; boot
        ; buildable
        ; enabled_if
+       ; coqdoc_flags
        })
 
   type Stanza.t += T of t

src/dune_rules/coq/coq_stanza.mli

@@ -34,6 +34,7 @@ module Theory : sig
     ; boot : bool
     ; enabled_if : Blang.t
     ; buildable : Buildable.t
+    ; coqdoc_flags : Ordered_set_lang.Unexpanded.t
     }
 
   type Stanza.t += T of t