Add "coqdoc_header" and "coqdoc_footer" fields.

Signed-off-by: Rodolphe Lepigre <[email protected]>
ocaml · Nov 22, 2024 · dc1181b · dc1181b
1 parent a50384a
commit dc1181b
Show file tree

Hide file tree

Showing 13 changed files with 222 additions and 8 deletions.
diff --git a/bin/printenv.ml b/bin/printenv.ml
@@ -26,7 +26,9 @@ let dump sctx ~dir =
     Dune_rules.Menhir_rules.menhir_env ~dir
     |> Action_builder.of_memo
     >>= Dune_rules.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_rules.Js_of_ocaml in
     let* jsoo = Action_builder.of_memo (Dune_rules.Jsoo_rules.jsoo_env ~dir ~mode:JS) in

diff --git a/doc/changes/11131.md b/doc/changes/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)
diff --git a/doc/coq.rst b/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,7 +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.10``: Support for the ``(coqdep_flags ...)`` field.
+- ``0.10``: Support for the ``(coqdep_flags ...)``, ``(coqdoc_header ...)``,
+  and ``(coqdoc_footer ...)`` fields.
 - ``0.9``: Support for per-module flags with the ``(module_flags ...)``` field.
 - ``0.8``: Support for composition with installed Coq theories;
   support for ``vos`` builds.
@@ -849,3 +864,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.
diff --git a/src/dune_rules/coq/coq_env.ml b/src/dune_rules/coq/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:(Dune_lang.Syntax.since Stanza.syntax (3, 13))
+        and+ coqdoc_header =
+          field_o
+            "coqdoc_header"
+            (Dune_lang.Syntax.since Stanza.syntax (3, 17) >>> String_with_vars.decode)
+        and+ coqdoc_footer =
+          field_o
+            "coqdoc_footer"
+            (Dune_lang.Syntax.since Stanza.syntax (3, 17) >>> 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
 ;;
diff --git a/src/dune_rules/coq/coq_env.mli b/src/dune_rules/coq/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 Dune_lang.Decoder.fields_parser
diff --git a/src/dune_rules/coq/coq_flags.ml b/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 ]
 ;;
diff --git a/src/dune_rules/coq/coq_flags.mli b/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
diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml
@@ -159,8 +159,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
@@ -205,6 +221,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
@@ -852,8 +886,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)

diff --git a/src/dune_rules/coq/coq_stanza.ml b/src/dune_rules/coq/coq_stanza.ml
@@ -172,6 +172,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 =
@@ -259,6 +261,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, 10) >>> String_with_vars.decode)
+       and+ coqdoc_footer =
+         field_o
+           "coqdoc_footer"
+           (Dune_lang.Syntax.since coq_syntax (0, 10) >>> String_with_vars.decode)
        in
        (* boot libraries cannot depend on other theories *)
        check_boot_has_no_deps boot buildable;
@@ -274,6 +284,8 @@ module Theory = struct
        ; enabled_if
        ; coqdep_flags
        ; coqdoc_flags
+       ; coqdoc_header
+       ; coqdoc_footer
        })
   ;;
 

diff --git a/src/dune_rules/coq/coq_stanza.mli b/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

diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-flags-header-footer-gen.t b/test/blackbox-tests/test-cases/coq/coqdoc-flags-header-footer-gen.t
@@ -0,0 +1,31 @@
+Testing the coqdoc_header and coqdoc_footer field of the env stanza.
+
+  $ cat > dune-project <<EOF
+  > (lang dune 3.17)
+  > (using coq 0.10)
+  > EOF
+
+  $ cat > dune <<EOF
+  > (rule (with-stdout-to header.%{coq:version}.html (echo "HEADER")))
+  > (rule (with-stdout-to footer.html (echo "FOOTER")))
+  > (env
+  >  (_
+  >   (coq
+  >    (coqdoc_header header.%{coq:version}.html)
+  >    (coqdoc_footer footer.html))))
+  > (coq.theory
+  >  (name a))
+  > EOF
+  $ cat > foo.v <<EOF
+  > Definition a := 42.
+  > EOF
+
+  $ dune build @doc
+  $ find _build/default/a.html -type f -name '*.html' | sort | xargs grep HEADER
+  _build/default/a.html/a.foo.html:HEADER
+  _build/default/a.html/index.html:HEADER
+  _build/default/a.html/toc.html:HEADER
+  $ find _build/default/a.html -type f -name '*.html' | sort | xargs grep FOOTER
+  _build/default/a.html/a.foo.html:FOOTER
+  _build/default/a.html/index.html:FOOTER
+  _build/default/a.html/toc.html:FOOTER
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-flags-header-footer.t b/test/blackbox-tests/test-cases/coq/coqdoc-flags-header-footer.t
@@ -0,0 +1,41 @@
+Testing the coqdoc_header and coqdoc_footer field of the env stanza.
+
+  $ cat > dune-project <<EOF
+  > (lang dune 3.17)
+  > (using coq 0.10)
+  > EOF
+
+  $ cat > dune <<EOF
+  > (env
+  >  (_
+  >   (coq
+  >    (coqdoc_header header.html)
+  >    (coqdoc_footer footer.html))))
+  > (coq.theory
+  >  (name a))
+  > EOF
+  $ cat > foo.v <<EOF
+  > Definition a := 42.
+  > EOF
+  $ cat > header.html <<EOF
+  > header
+  > EOF
+  $ cat > footer.html <<EOF
+  > footer
+  > EOF
+
+  $ dune build @doc
+
+  $ tail _build/log -n 1 | ./scrub_coq_args.sh | sed 's/.*coq/coq/'
+  coqdoc
+  coq/theories Coq
+  -R . a --toc --with-header header.html --with-footer footer.html --html -d a.html
+  foo.v
+
+  $ dune build @doc-latex
+
+  $ tail _build/log -n 1 | ./scrub_coq_args.sh | sed 's/.*coq/coq/'
+  coqdoc
+  coq/theories Coq
+  -R . a --toc --latex -d a.tex
+  foo.v
diff --git a/test/blackbox-tests/test-cases/workspaces/workspace-env.t/run.t b/test/blackbox-tests/test-cases/workspaces/workspace-env.t/run.t
@@ -15,6 +15,8 @@ Workspaces also allow you to set the env for a context:
   (coq_flags (-q))
   (coqdep_flags ())
   (coqdoc_flags (--toc))
+  (coqdoc_header ())
+  (coqdoc_footer ())
   (js_of_ocaml_flags ())
   (js_of_ocaml_build_runtime_flags ())
   (js_of_ocaml_link_flags ())