Merge pull request #11131 from rlepigre/coqdoc-header-footer

Add "coqdoc_header" and "coqdoc_footer" fields.

Author: Alizter

bin/printenv.ml

@@ -26,7 +26,9 @@ let dump sctx ~dir =
     Dune_rules.Menhir_rules.menhir_env ~dir
     |> Action_builder.of_memo
     >>= Dune_lang.Menhir_env.dump
-  and+ coq_dump = Dune_rules.Coq.Coq_rules.coq_env ~dir >>| Dune_rules.Coq.Coq_flags.dump
+  and+ coq_dump =
+    Dune_rules.Coq.Coq_rules.coq_env ~dir
+    >>| Dune_rules.Coq.Coq_flags.dump ~dir:(Path.build dir)
   and+ jsoo_js_dump =
     let module Js_of_ocaml = Dune_lang.Js_of_ocaml in
     let* jsoo = Action_builder.of_memo (Dune_rules.Jsoo_rules.jsoo_env ~dir ~mode:JS) in

doc/changes/added/11131.md

@@ -0,0 +1,4 @@
+- Add `coqdoc_header` and `coqdoc_footer` fields to the `coq` field of the
+  `env` stanza, and to the `coq.theory` stanza, allowing to configure a
+  custom header or footer respectively in the HTML output of `coqdoc`.
+  (#11131, @rlepigre)

doc/coq.rst

@@ -69,6 +69,8 @@ The Coq theory stanza is very similar in form to the OCaml
      (modules_flags <flags_map>)
      (coqdep_flags <coqdep_flags>)
      (coqdoc_flags <coqdoc_flags>)
+     (coqdoc_header <coqdoc_header>)
+     (coqdoc_footer <coqdoc_footer>)
      (stdlib <stdlib_included>)
      (mode <coq_native_mode>)
      (theories <coq_theories>))
@@ -146,6 +148,14 @@ The semantics of the fields are:
   flags are passed separately depending on which mode is target. See the section
   on :ref:`documentation using coqdoc<coqdoc>` for more information.
 
+- ``<coqdoc_header>`` is a file passed to ``coqdoc`` using the ``--with-header``
+  option, to configure a custom HTML header for the generated HTML pages.
+  (Appeared in :ref:`Coq lang 0.10<coq-lang>`)
+
+- ``<coqdoc_footer>`` is a file passed to ``coqdoc`` using the ``--with-footer``
+  option, to configure a custom HTML footer for the generated HTML pages.
+  (Appeared in :ref:`Coq lang 0.10<coq-lang>`)
+
 - ``<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
@@ -212,6 +222,10 @@ Further flags can also be configured using the ``(coqdoc_flags)`` field in the
 is ``:standard`` which is ``--toc``. Extra flags can therefore be passed by
 writing ``(coqdoc_flags :standard --body-only)`` for example.
 
+When building the HTML documentation, flags ``(coqdoc_header)`` and
+``(coqdoc_footer)`` can also be used to configure a custom HTML header or
+footer respectively.
+
 .. _include-subdirs-coq:
 
 Recursive Qualification of Modules
@@ -354,6 +368,8 @@ The Coq lang can be modified by adding the following to a
 
 The supported Coq language versions (not the version of Coq) are:
 
+- ``0.11``: Support for the ``(coqdoc_header ...)`` and ``(coqdoc_footer ...)``
+  fields.
 - ``0.10``: Support for the ``(coqdep_flags ...)`` field.
 - ``0.9``: Support for per-module flags with the ``(module_flags ...)``` field.
 - ``0.8``: Support for composition with installed Coq theories;
@@ -849,3 +865,9 @@ with the following values for ``<coq_fields>``:
 - ``(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.
+- ``(coqdoc_header <file>)``: The default HTML header passed to ``coqdoc`` via
+  the ``--with-header`` flag. Values set here become the ``:standard`` value in the
+  ``(coq.theory (coqdoc_header <file>))`` field.
+- ``(coqdoc_footer <file>)``: The default HTML footer passed to ``coqdoc`` via
+  the ``--with-footer`` flag. Values set here become the ``:standard`` value in the
+  ``(coq.theory (coqdoc_footer <file>))`` field.

src/dune_lang/coq_env.ml

@@ -5,18 +5,24 @@ type t =
   { flags : Ordered_set_lang.Unexpanded.t
   ; coqdep_flags : Ordered_set_lang.Unexpanded.t
   ; coqdoc_flags : Ordered_set_lang.Unexpanded.t
+  ; coqdoc_header : String_with_vars.t option
+  ; coqdoc_footer : String_with_vars.t option
   }
 
 let default =
   { flags = Ordered_set_lang.Unexpanded.standard
   ; coqdep_flags = Ordered_set_lang.Unexpanded.standard
   ; coqdoc_flags = Ordered_set_lang.Unexpanded.standard
+  ; coqdoc_header = None
+  ; coqdoc_footer = None
   }
 ;;
 
 let flags t = t.flags
 let coqdep_flags t = t.coqdep_flags
 let coqdoc_flags t = t.coqdoc_flags
+let coqdoc_header t = t.coqdoc_header
+let coqdoc_footer t = t.coqdoc_footer
 
 let decode =
   field
@@ -35,12 +41,22 @@ let decode =
           Ordered_set_lang.Unexpanded.field
             "coqdoc_flags"
             ~check:(Syntax.since Stanza.syntax (3, 13))
+        and+ coqdoc_header =
+          field_o
+            "coqdoc_header"
+            (Syntax.since Stanza.syntax (3, 21) >>> String_with_vars.decode)
+        and+ coqdoc_footer =
+          field_o
+            "coqdoc_footer"
+            (Syntax.since Stanza.syntax (3, 21) >>> String_with_vars.decode)
         in
-        { flags; coqdep_flags; coqdoc_flags }))
+        { flags; coqdep_flags; coqdoc_flags; coqdoc_header; coqdoc_footer }))
 ;;
 
-let equal { flags; coqdep_flags; coqdoc_flags } t =
+let equal { flags; coqdep_flags; coqdoc_flags; coqdoc_header; coqdoc_footer } t =
   Ordered_set_lang.Unexpanded.equal flags t.flags
   && Ordered_set_lang.Unexpanded.equal coqdep_flags t.coqdep_flags
   && Ordered_set_lang.Unexpanded.equal coqdoc_flags t.coqdoc_flags
+  && Option.equal String_with_vars.equal coqdoc_header t.coqdoc_header
+  && Option.equal String_with_vars.equal coqdoc_footer t.coqdoc_footer
 ;;

src/dune_lang/coq_env.mli

@@ -17,5 +17,11 @@ val coqdep_flags : t -> Ordered_set_lang.Unexpanded.t
 (** Flags for coqdoc *)
 val coqdoc_flags : t -> Ordered_set_lang.Unexpanded.t
 
+(** Coqdoc header config. *)
+val coqdoc_header : t -> String_with_vars.t option
+
+(** Coqdoc footer config. *)
+val coqdoc_footer : t -> String_with_vars.t option
+
 (** Parser for env stanza. *)
 val decode : t Decoder.fields_parser

src/dune_rules/coq/coq_flags.ml

@@ -4,12 +4,24 @@ type t =
   { coq_flags : string list
   ; coqdep_flags : string list
   ; coqdoc_flags : string list
+  ; coqdoc_header : Path.t option
+  ; coqdoc_footer : Path.t option
   }
 
-let default = { coq_flags = [ "-q" ]; coqdep_flags = []; coqdoc_flags = [ "--toc" ] }
+let default =
+  { coq_flags = [ "-q" ]
+  ; coqdep_flags = []
+  ; coqdoc_flags = [ "--toc" ]
+  ; coqdoc_header = None
+  ; coqdoc_footer = None
+  }
+;;
 
-let dump { coq_flags; coqdep_flags; coqdoc_flags } =
+let dump ~dir { coq_flags; coqdep_flags; coqdoc_flags; coqdoc_header; coqdoc_footer } =
   List.map
     ~f:Dune_lang.Encoder.(pair string (list string))
     [ "coq_flags", coq_flags; "coqdep_flags", coqdep_flags; "coqdoc_flags", coqdoc_flags ]
+  @ List.map
+      ~f:Dune_lang.Encoder.(pair string (option (Dune_lang.Path.Local.encode ~dir)))
+      [ "coqdoc_header", coqdoc_header; "coqdoc_footer", coqdoc_footer ]
 ;;

src/dune_rules/coq/coq_flags.mli

@@ -1,8 +1,12 @@
+open Import
+
 type t =
   { coq_flags : string list
   ; coqdep_flags : string list
   ; coqdoc_flags : string list
+  ; coqdoc_header : Path.t option
+  ; coqdoc_footer : Path.t option
   }
 
 val default : t
-val dump : t -> Dune_lang.t list
+val dump : dir:Path.t -> t -> Dune_lang.t list

src/dune_rules/coq/coq_rules.ml

@@ -160,8 +160,24 @@ let coq_env =
             expander
             (Coq_env.coqdoc_flags config.coq)
             ~standard
+        and+ coqdoc_header =
+          match Coq_env.coqdoc_header config.coq with
+          | None ->
+            let+ x = Action_builder.of_memo_join parent in
+            x.coqdoc_header
+          | Some s ->
+            let+ path = Expander.expand_path expander s in
+            Some path
+        and+ coqdoc_footer =
+          match Coq_env.coqdoc_footer config.coq with
+          | None ->
+            let+ x = Action_builder.of_memo_join parent in
+            x.coqdoc_footer
+          | Some s ->
+            let+ path = Expander.expand_path expander s in
+            Some path
         in
-        { Coq_flags.coq_flags; coqdep_flags; coqdoc_flags })
+        { Coq_flags.coq_flags; coqdep_flags; coqdoc_flags; coqdoc_header; coqdoc_footer })
   in
   fun ~dir ->
     (let* () = Memo.return () in
@@ -206,6 +222,24 @@ let coqdoc_flags ~dir ~stanza_coqdoc_flags ~expander =
          (coq_env ~dir))
 ;;
 
+let coqdoc_header ~dir ~stanza_coqdoc_header ~expander =
+  match stanza_coqdoc_header with
+  | None ->
+    Action_builder.map
+      ~f:(fun { Coq_flags.coqdoc_header; _ } -> coqdoc_header)
+      (coq_env ~dir)
+  | Some s -> Action_builder.map ~f:Option.some (Expander.expand_path expander s)
+;;
+
+let coqdoc_footer ~dir ~stanza_coqdoc_footer ~expander =
+  match stanza_coqdoc_footer with
+  | None ->
+    Action_builder.map
+      ~f:(fun { Coq_flags.coqdoc_footer; _ } -> coqdoc_footer)
+      (coq_env ~dir)
+  | Some s -> Action_builder.map ~f:Option.some (Expander.expand_path expander s)
+;;
+
 let theory_coqc_flag lib =
   let name = Coq_lib_name.wrapper (Coq_lib.name lib) in
   let dir = Coq_lib.obj_root lib in
@@ -855,8 +889,35 @@ let setup_coqdoc_rules ~sctx ~dir ~theories_deps (s : Coq_stanza.Theory.t) coq_m
              in
              Expander.expand_and_eval_set expander s.coqdoc_flags ~standard
            in
+           let header =
+             let open Action_builder.O in
+             let* expander = Action_builder.of_memo @@ Super_context.expander sctx ~dir in
+             let+ header =
+               coqdoc_header ~dir ~stanza_coqdoc_header:s.coqdoc_header ~expander
+             in
+             match header with
+             | None -> Command.Args.empty
+             | Some path -> Command.Args.S [ A "--with-header"; Dep path ]
+           in
+           let footer =
+             let open Action_builder.O in
+             let* expander = Action_builder.of_memo @@ Super_context.expander sctx ~dir in
+             let+ footer =
+               coqdoc_footer ~dir ~stanza_coqdoc_footer:s.coqdoc_footer ~expander
+             in
+             match footer with
+             | None -> Command.Args.empty
+             | Some path -> Command.Args.S [ A "--with-footer"; Dep path ]
+           in
+           let when_html dyn =
+             match mode with
+             | `Html -> Command.Args.Dyn dyn
+             | `Latex -> Command.Args.empty
+           in
            [ Command.Args.S file_flags
            ; Command.Args.dyn extra_coqdoc_flags
+           ; when_html header
+           ; when_html footer
            ; A mode_flag
            ; A "-d"
            ; Path (Path.build doc_dir)

src/dune_rules/coq/coq_stanza.ml

@@ -15,6 +15,7 @@ let coq_syntax =
     ; (0, 8), `Since (3, 8)
     ; (0, 9), `Since (3, 16)
     ; (0, 10), `Since (3, 17)
+    ; (0, 11), `Since (3, 21)
     ]
 ;;
 
@@ -172,6 +173,8 @@ module Theory = struct
     ; buildable : Buildable.t
     ; coqdep_flags : Ordered_set_lang.Unexpanded.t
     ; coqdoc_flags : Ordered_set_lang.Unexpanded.t
+    ; coqdoc_header : String_with_vars.t option
+    ; coqdoc_footer : String_with_vars.t option
     }
 
   let coq_public_decode =
@@ -260,6 +263,14 @@ module Theory = struct
          Ordered_set_lang.Unexpanded.field
            "coqdoc_flags"
            ~check:(Dune_lang.Syntax.since coq_syntax (0, 8))
+       and+ coqdoc_header =
+         field_o
+           "coqdoc_header"
+           (Dune_lang.Syntax.since coq_syntax (0, 11) >>> String_with_vars.decode)
+       and+ coqdoc_footer =
+         field_o
+           "coqdoc_footer"
+           (Dune_lang.Syntax.since coq_syntax (0, 11) >>> String_with_vars.decode)
        in
        (* boot libraries cannot depend on other theories *)
        check_boot_has_no_deps boot buildable;
@@ -275,6 +286,8 @@ module Theory = struct
        ; enabled_if
        ; coqdep_flags
        ; coqdoc_flags
+       ; coqdoc_header
+       ; coqdoc_footer
        })
   ;;
 

src/dune_rules/coq/coq_stanza.mli

@@ -37,6 +37,8 @@ module Theory : sig
     ; buildable : Buildable.t
     ; coqdep_flags : Ordered_set_lang.Unexpanded.t
     ; coqdoc_flags : Ordered_set_lang.Unexpanded.t
+    ; coqdoc_header : String_with_vars.t option
+    ; coqdoc_footer : String_with_vars.t option
     }
 
   include Stanza.S with type t := t