Add "coqdoc_header" and "coqdoc_footer" fields.

Signed-off-by: Rodolphe Lepigre <[email protected]>

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

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)

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
 ;;

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

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

@@ -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)

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
        })
   ;;
 

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

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 <<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