From 7b75def0f2ddc26705b8b91e540a552f90d3b3e3 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Tue, 19 Nov 2024 00:44:45 +0100 Subject: [PATCH] Add "coqdoc_header" and "coqdoc_footer" fields. Signed-off-by: Rodolphe Lepigre --- bin/printenv.ml | 4 +- doc/changes/11131.md | 2 + doc/coq.rst | 23 +++++++- src/dune_rules/coq/coq_env.ml | 20 ++++++- src/dune_rules/coq/coq_env.mli | 6 ++ src/dune_rules/coq/coq_flags.ml | 16 ++++- src/dune_rules/coq/coq_flags.mli | 6 +- src/dune_rules/coq/coq_rules.ml | 58 ++++++++++++++++++- src/dune_rules/coq/coq_stanza.ml | 12 ++++ src/dune_rules/coq/coq_stanza.mli | 2 + .../coq/coqdoc-flags-header-footer-gen.t | 31 ++++++++++ .../coq/coqdoc-flags-header-footer.t | 33 +++++++++++ .../workspaces/workspace-env.t/run.t | 2 + 13 files changed, 207 insertions(+), 8 deletions(-) create mode 100644 doc/changes/11131.md create mode 100644 test/blackbox-tests/test-cases/coq/coqdoc-flags-header-footer-gen.t create mode 100644 test/blackbox-tests/test-cases/coq/coqdoc-flags-header-footer.t diff --git a/bin/printenv.ml b/bin/printenv.ml index 709bf53c9b2..a4f1eb3256a 100644 --- 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 new file mode 100644 index 00000000000..ca2e868bc3f --- /dev/null +++ b/doc/changes/11131.md @@ -0,0 +1,2 @@ +- 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 index 6ddb391358d..7f8181d8350 100644 --- 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 ) (coqdep_flags ) (coqdoc_flags ) + (coqdoc_header ) + (coqdoc_footer ) (stdlib ) (mode ) (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` for more information. +- ```` 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`) + +- ```` 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`) + - ```` 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 ````: - ``(coqdoc_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 ))`` field. +- ``(coqdoc_header )``: 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 ))`` field. +- ``(coqdoc_footer )``: 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 ))`` field. diff --git a/src/dune_rules/coq/coq_env.ml b/src/dune_rules/coq/coq_env.ml index 8afa7d2bbf5..a2dabd8c6a7 100644 --- 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 index e5ce999bb48..3acb78372e2 100644 --- 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 index 16ce8972582..87948e22eb4 100644 --- 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 index 7f249549b44..570b79a53b1 100644 --- 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 index 6b4db3b1bb9..d5c7edb9d17 100644 --- 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,30 @@ 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 [ Command.Args.S file_flags ; Command.Args.dyn extra_coqdoc_flags + ; Command.Args.Dyn header + ; Command.Args.Dyn 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 index 3bc1f06d066..0389784f157 100644 --- 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 index bc243b3e77b..eb211babb4a 100644 --- 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 new file mode 100644 index 00000000000..9c321e45d54 --- /dev/null +++ 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 < (lang dune 3.17) + > (using coq 0.10) + > EOF + + $ cat > dune < (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 < 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 new file mode 100644 index 00000000000..10a283eeb91 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/coqdoc-flags-header-footer.t @@ -0,0 +1,33 @@ +Testing the coqdoc_header and coqdoc_footer field of the env stanza. + + $ cat > dune-project < (lang dune 3.17) + > (using coq 0.10) + > EOF + + $ cat > dune < (env + > (_ + > (coq + > (coqdoc_header header.html) + > (coqdoc_footer footer.html)))) + > (coq.theory + > (name a)) + > EOF + $ cat > foo.v < Definition a := 42. + > EOF + $ cat > header.html < header + > EOF + $ cat > footer.html < 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 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 index 313c25faf49..5b1efc00b21 100644 --- 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 ())