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

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`. (#7676, fixes #7954 @Alizter)
+
 - Resolve `ppx_runtime_libraries` in the target context when cross compiling
   (#7450, fixes #2794, @anmonteiro)
 

doc/coq.rst

@@ -59,6 +59,7 @@ stanza:
      (modules <ordered_set_lang>)
      (plugins <ocaml_plugins>)
      (flags <coq_flags>)
+     (coqdoc_flags <coqdoc_flags>)
      (stdlib <stdlib_included>)
      (mode <coq_native_mode>)
      (theories <coq_theories>))
@@ -106,6 +107,11 @@ The semantics of the fields are:
   is taken from the value set in the ``(coq (flags <flags>))`` field in ``env``
   profile. See :ref:`dune-env` for more information.
 
+- ``<coqdoc_flags>`` 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 targed. See the section
+  on :ref:`documentation using coqdoc<coqdoc>` for more information.
+
 - ``<stdlib_included>`` can either be ``yes`` or ``no``, currently defaulting to
   ``yes``. When set to ``no``, Coq's standard library won't be visible from this
   theory, which means the ``Coq`` prefix won't be bound, and
@@ -150,6 +156,7 @@ them in the correct order, even if they are in separate theories. Under the
 hood, Dune asks coqdep how to resolve these dependencies, which is why it is
 called once per theory.
 
+.. _coqdoc:
 
 Coq Documentation
 ~~~~~~~~~~~~~~~~~
@@ -161,7 +168,13 @@ A.tex``, respectively (if the :ref:`dune file<dune-files>` for the theory is the
 current directory).
 
 There are also two aliases ``@doc`` and ``@doc-latex`` that will respectively
-build the HTML or LaTeX documentation when called.
+build the HTML or LaTeX documentation when called. These will determine whether
+or not Dune passes a ``--html`` or ``--latex`` flag to ``coqdoc``.
+
+Further flags can also be configured using the ``(coqdoc_flags)`` field in the
+``coq.theory`` stanza. These will be passed to ``coqdoc`` and the default value
+is ``:standard`` which is ``--toc``. Extra flags can therefore be passed by
+writing ``(coqdoc_flags :standard --body-only)`` for example.
 
 .. _include-subdirs-coq:
 

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

@@ -129,6 +129,7 @@ module Theory = struct
     ; boot : bool
     ; enabled_if : Blang.t
     ; buildable : Buildable.t
+    ; coqdoc_flags : Ordered_set_lang.Unexpanded.t
     }
 
   let coq_public_decode =
@@ -186,7 +187,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
@@ -198,6 +203,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