From 2091f8b98ad4492e7b7323581e261a5556162d87 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Mon, 18 Nov 2024 22:31:50 +0100 Subject: [PATCH] Add "coqdoc_header" and "coqdoc_footer" fields. Signed-off-by: Rodolphe Lepigre --- bin/printenv.ml | 4 +- boot/libs.ml | 2 +- src/dune_rules/coq/coq_env.ml | 15 ++++- 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 | 7 ++- src/dune_rules/coq/coq_stanza.mli | 2 + .../coq/coqdoc-flags-header-footer.t | 33 +++++++++++ 10 files changed, 139 insertions(+), 10 deletions(-) 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/boot/libs.ml b/boot/libs.ml index 6faacb217ec..b6aeed5a6d5 100644 --- a/boot/libs.ml +++ b/boot/libs.ml @@ -1,4 +1,4 @@ -let external_libraries = [ "unix"; "threads" ] +let external_libraries = [ "threads.posix" ] let local_libraries = [ ("otherlibs/ordering", Some "Ordering", false, None) diff --git a/src/dune_rules/coq/coq_env.ml b/src/dune_rules/coq/coq_env.ml index 8afa7d2bbf5..c25def67648 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,15 @@ let decode = Ordered_set_lang.Unexpanded.field "coqdoc_flags" ~check:(Dune_lang.Syntax.since Stanza.syntax (3, 13)) - in - { flags; coqdep_flags; coqdoc_flags })) + and+ coqdoc_header = field_o "coqdoc_header" String_with_vars.decode + and+ coqdoc_footer = field_o "coqdoc_footer" String_with_vars.decode in + { 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..63818a55848 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,7 +261,8 @@ module Theory = struct Ordered_set_lang.Unexpanded.field "coqdoc_flags" ~check:(Dune_lang.Syntax.since coq_syntax (0, 8)) - in + and+ coqdoc_header = field_o "coqdoc_header" String_with_vars.decode + and+ coqdoc_footer = field_o "coqdoc_footer" String_with_vars.decode in (* boot libraries cannot depend on other theories *) check_boot_has_no_deps boot buildable; let package = merge_package_public ~package ~public in @@ -274,6 +277,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.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