From ae33567d7bec7bbaee0aace069e2abde21742fef Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Wed, 3 May 2023 17:51:06 +0200
Subject: [PATCH] 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                        |  3 +++
 src/dune_rules/coq/coq_rules.ml   | 11 ++++++++++-
 src/dune_rules/coq/coq_stanza.ml  |  8 +++++++-
 src/dune_rules/coq/coq_stanza.mli |  1 +
 4 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 041914215ac..1e2c85ae01c 100644
--- a/CHANGES.md
+++ b/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)
 
diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml
index b5a7b865d6a..d366eeb0e2b 100644
--- a/src/dune_rules/coq/coq_rules.ml
+++ b/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)
diff --git a/src/dune_rules/coq/coq_stanza.ml b/src/dune_rules/coq/coq_stanza.ml
index c3d63a93499..d38702c514f 100644
--- a/src/dune_rules/coq/coq_stanza.ml
+++ b/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
diff --git a/src/dune_rules/coq/coq_stanza.mli b/src/dune_rules/coq/coq_stanza.mli
index 681f6980a69..40b2a51f7f0 100644
--- a/src/dune_rules/coq/coq_stanza.mli
+++ b/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