Skip to content

Commit

Permalink
feature(coq): add coqdoc_flags field to coq.theory
Browse files Browse the repository at this point in the history
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>
Alizter committed May 3, 2023
1 parent 988b0b2 commit 5e367c7
Showing 4 changed files with 21 additions and 2 deletions.
3 changes: 3 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -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)

11 changes: 10 additions & 1 deletion src/dune_rules/coq/coq_rules.ml
Original file line number Diff line number Diff line change
@@ -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)
8 changes: 7 additions & 1 deletion src/dune_rules/coq/coq_stanza.ml
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions src/dune_rules/coq/coq_stanza.mli
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 5e367c7

Please sign in to comment.