initial coqdoc support

CHANGES.md

@@ -9,6 +9,12 @@ Unreleased
 
 - Support new locations of unix, str, dynlink in OCaml >= 5.0 (#5582, @dra27)
 
+- The ``coq.theory`` stanza now produces rules for running ``coqdoc``. Given a
+  theory named ``mytheory``, the directory targets ``mytheory.html/`` and
+  ``mytheory.tex/`` or additionally the aliases `@doc` and `@doc-latex` will
+  build the HTML and LaTeX documentation repsectively. (#5695, fixes #3760,
+  @Alizter)
+
 3.2.0 (17-05-2022)
 ------------------
 

src/dune_engine/action_builder.ml

@@ -151,6 +151,15 @@ module With_targets = struct
           (Targets.Files.create (Path.Build.Set.of_list file_targets))
     }
 
+  let add_directories t ~directory_targets =
+    { build = t.build
+    ; targets =
+        Targets.combine t.targets
+          (Targets.create
+             ~dirs:(Path.Build.Set.of_list directory_targets)
+             ~files:Path.Build.Set.empty)
+    }
+
   let map { build; targets } ~f = { build = map build ~f; targets }
 
   let map2 x y ~f =

src/dune_engine/action_builder.mli

@@ -18,6 +18,8 @@ module With_targets : sig
 
   val add : 'a t -> file_targets:Path.Build.t list -> 'a t
 
+  val add_directories : 'a t -> directory_targets:Path.Build.t list -> 'a t
+
   val map : 'a t -> f:('a -> 'b) -> 'b t
 
   val map2 : 'a t -> 'b t -> f:('a -> 'b -> 'c) -> 'c t

src/dune_rules/command.ml

@@ -97,7 +97,7 @@ let dep_prog = function
   | Ok p -> Action_builder.path p
   | Error _ -> Action_builder.return ()
 
-let run ~dir ?stdout_to prog args =
+let run ~dir ?sandbox ?stdout_to prog args =
   Action_builder.With_targets.add ~file_targets:(Option.to_list stdout_to)
     (let open Action_builder.With_targets.O in
     let+ () = Action_builder.with_no_targets (dep_prog prog)
@@ -108,7 +108,7 @@ let run ~dir ?stdout_to prog args =
       | None -> action
       | Some path -> Action.with_stdout_to path action
     in
-    Action.Full.make (Action.chdir dir action))
+    Action.Full.make ?sandbox (Action.chdir dir action))
 
 let run' ~dir prog args =
   let open Action_builder.O in

src/dune_rules/command.mli

@@ -79,6 +79,7 @@ end
    we can use the constructor [S] to concatenate lists instead. *)
 val run :
      dir:Path.t
+  -> ?sandbox:Sandbox_config.t
   -> ?stdout_to:Path.Build.t
   -> Action.Prog.t
   -> Args.any Args.t list

src/dune_rules/coq_module.ml

@@ -70,6 +70,10 @@ type obj_files_mode =
   | Build
   | Install
 
+let glob_file x ~obj_dir =
+  let vo_dir = build_vo_dir ~obj_dir x in
+  Path.Build.relative vo_dir (x.name ^ ".glob")
+
 (* XXX: Remove the install .coq-native hack once rules can output targets in
    multiple subdirs *)
 let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode =

src/dune_rules/coq_module.mli

@@ -40,6 +40,8 @@ val name : t -> Name.t
 
 val dep_file : t -> obj_dir:Path.Build.t -> Path.Build.t
 
+val glob_file : t -> obj_dir:Path.Build.t -> Path.Build.t
+
 (** Some of the object files should not be installed, we control this with the
     following parameter *)
 type obj_files_mode =

src/dune_rules/coq_rules.ml

@@ -106,6 +106,7 @@ module Context = struct
   type 'a t =
     { coqdep : Action.Prog.t
     ; coqc : Action.Prog.t * Path.Build.t
+    ; coqdoc : Action.Prog.t
     ; wrapper_name : string
     ; dir : Path.Build.t
     ; expander : Expander.t
@@ -190,6 +191,16 @@ module Context = struct
       in
       Resolve.args args
 
+  let coqdoc_file_flags cctx =
+    let file_flags =
+      [ theories_flags cctx
+      ; Command.Args.A "-R"
+      ; Path (Path.build cctx.dir)
+      ; A cctx.wrapper_name
+      ]
+    in
+    [ Command.Args.S (Bootstrap.flags cctx.boot_type); S file_flags ]
+
   (* compute include flags and mlpack rules *)
   let setup_ml_deps ~lib_db libs theories =
     (* Pair of include flags and paths to mlpack *)
@@ -250,9 +261,11 @@ module Context = struct
       setup_native_theory_includes ~sctx ~mode ~theories_deps ~theory_dirs
     and+ coqdep = rr "coqdep"
     and+ coqc = rr "coqc"
+    and+ coqdoc = rr "coqdoc"
     and+ profile_flags = Super_context.coq sctx ~dir in
     { coqdep
     ; coqc = (coqc, coqc_dir)
+    ; coqdoc
     ; wrapper_name
     ; dir
     ; expander
@@ -372,6 +385,79 @@ let coqc_rule (cctx : _ Context.t) ~file_flags coq_module =
   Context.coqc cctx (Command.Args.dyn coq_flags :: file_flags)
   >>| Action.Full.add_sandbox sandbox
 
+module Coqdoc_mode = struct
+  type t =
+    | Html
+    | Latex
+
+  let flag = function
+    | Html -> "--html"
+    | Latex -> "--latex"
+
+  let directory t obj_dir (theory : Coq_lib_name.t) =
+    Path.Build.relative obj_dir
+      (Coq_lib_name.to_string theory
+      ^
+      match t with
+      | Html -> ".html"
+      | Latex -> ".tex")
+
+  let alias t ~dir =
+    match t with
+    | Html -> Alias.doc ~dir
+    | Latex -> Alias.make (Alias.Name.of_string "doc-latex") ~dir
+end
+
+let coqdoc_directory_targets ~dir:obj_dir (theory : Coq_stanza.Theory.t) =
+  let loc, name = theory.name in
+  Path.Build.Map.of_list_exn
+    [ (Coqdoc_mode.directory Html obj_dir name, loc)
+    ; (Coqdoc_mode.directory Latex obj_dir name, loc)
+    ]
+
+let coqdoc_rule (cctx : _ Context.t) ~sctx ~name:(_, name) ~file_flags ~mode
+    ~theories_deps coq_modules =
+  let obj_dir = cctx.dir in
+  let doc_dir = Coqdoc_mode.directory mode obj_dir name in
+  let file_flags =
+    let globs =
+      let open Action_builder.O in
+      let* theories_deps = Resolve.read theories_deps in
+      Action_builder.of_memo
+      @@
+      let open Memo.O in
+      let+ deps =
+        Memo.parallel_map theories_deps ~f:(fun theory ->
+            let+ theory_dirs = Context.directories_of_lib ~sctx theory in
+            Dep.Set.of_list_map theory_dirs ~f:(fun dir ->
+                (* TODO *)
+                Glob.of_string_exn Loc.none "*.{glob}"
+                |> Glob.to_pred
+                |> File_selector.create ~dir:(Path.build dir)
+                |> Dep.file_selector))
+      in
+      Command.Args.Hidden_deps (Dep.Set.union_all deps)
+    in
+    [ Command.Args.S file_flags
+    ; A "--toc"
+    ; A Coqdoc_mode.(flag mode)
+    ; A "-d"
+    ; Path (Path.build doc_dir)
+    ; Deps (List.map ~f:Path.build @@ List.map ~f:Coq_module.source coq_modules)
+    ; Dyn globs
+    ; Hidden_deps
+        (Dep.Set.of_files @@ List.map ~f:Path.build
+        @@ List.map ~f:(Coq_module.glob_file ~obj_dir) coq_modules)
+    ]
+  in
+  Command.run ~sandbox:Sandbox_config.needs_sandboxing
+    ~dir:(Path.build cctx.dir) cctx.coqdoc file_flags
+  |> Action_builder.With_targets.map
+       ~f:
+         (Action.Full.map ~f:(fun coqdoc ->
+              Action.Progn [ Action.mkdir (Path.build doc_dir); coqdoc ]))
+  |> Action_builder.With_targets.add_directories ~directory_targets:[ doc_dir ]
+
 module Module_rule = struct
   type t =
     { coqdep : Action.Full.t Action_builder.With_targets.t
@@ -425,8 +511,9 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
     let theories_deps =
       Coq_lib.DB.requires coq_lib_db theory |> Resolve.of_result
     in
-    let theory_dirs = Coq_sources.directories coq_dir_contents ~name in
-    let theory_dirs = Path.Build.Set.of_list theory_dirs in
+    let theory_dirs =
+      Coq_sources.directories coq_dir_contents ~name |> Path.Build.Set.of_list
+    in
     let coqc_dir = (Super_context.context sctx).build_dir in
     Context.create sctx ~coqc_dir ~dir ~wrapper_name ~theories_deps ~theory_dirs
       s.buildable
@@ -441,11 +528,28 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
     in
     source_rule ~sctx theories
   in
+  let loc = s.buildable.loc in
+  let* () =
+    let rule =
+      let file_flags = Context.coqdoc_file_flags cctx in
+      fun mode ->
+        let* () =
+          coqdoc_rule cctx ~sctx ~mode ~theories_deps:cctx.theories_deps
+            ~name:s.name ~file_flags coq_modules
+          |> Super_context.add_rule ~loc ~dir sctx
+        in
+        Coqdoc_mode.directory mode cctx.dir name
+        |> Path.build |> Action_builder.path
+        |> Rules.Produce.Alias.add_deps (Coqdoc_mode.alias mode ~dir) ~loc
+    in
+    let* () = rule Html in
+    rule Latex
+  in
   List.concat_map coq_modules ~f:(fun m ->
       let cctx = Context.for_module cctx m in
       let { Module_rule.coqc; coqdep } = setup_rule cctx ~source_rule m in
       [ coqc; coqdep ])
-  |> Super_context.add_rules ~loc:s.buildable.loc ~dir sctx
+  |> Super_context.add_rules ~loc ~dir sctx
 
 let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Theory.t) coq_module =
   let name = snd s.name in

src/dune_rules/coq_rules.mli

@@ -17,6 +17,9 @@ module Bootstrap : sig
     | Bootstrap_prelude  (** We are compiling the prelude itself *)
 end
 
+val coqdoc_directory_targets :
+  dir:Path.Build.t -> Coq_stanza.Theory.t -> Loc.t Path.Build.Map.t
+
 val setup_rules :
      sctx:Super_context.t
   -> dir:Path.Build.t

src/dune_rules/gen_rules.ml

@@ -277,6 +277,24 @@ let gen_rules sctx dir_contents cctxs expander
   let+ () = define_all_alias ~dir:ctx_dir ~scope ~js_targets in
   cctxs
 
+let collect_directory_targets sctx ~init ~dir =
+  match Super_context.stanzas_in sctx ~dir with
+  | None -> init
+  | Some { Dir_with_dune.data = stanzas; ctx_dir = dir; _ } ->
+    List.fold_left stanzas ~init ~f:(fun acc stanza ->
+        match stanza with
+        | Coq_stanza.Theory.T m ->
+          Coq_rules.coqdoc_directory_targets ~dir m
+          |> Path.Build.Map.union acc ~f:(fun path loc1 loc2 ->
+                 User_error.raise
+                   [ Pp.textf
+                       "the following both define the directory target: %s"
+                       (Path.Build.to_string path)
+                   ; Pp.textf "- %s" (Loc.to_file_colon_line loc1)
+                   ; Pp.textf "- %s" (Loc.to_file_colon_line loc2)
+                   ])
+        | _ -> acc)
+
 let gen_rules sctx dir_contents cctxs ~source_dir ~dir :
     (Loc.t * Compilation_context.t) list Memo.t =
   let* expander =
@@ -429,7 +447,8 @@ let gen_rules ~sctx ~dir components : Build_config.gen_rules_result Memo.t =
         Memo.return
           (Build_config.Rules
              { build_dir_only_sub_dirs = S.These subdirs
-             ; directory_targets
+             ; directory_targets =
+                 collect_directory_targets sctx ~dir ~init:directory_targets
              ; rules
              })))
 

test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/base.v

@@ -0,0 +1,5 @@
+
+Variant Or (A B : Set) : Set :=
+| inl : A -> Or A B
+| inr : B -> Or A B
+.

test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/dune

@@ -0,0 +1,21 @@
+(rule
+ (targets
+  (dir base.html))
+ (action
+  (progn
+   (run mkdir base.html)
+   (run touch base.html/base.base.html))))
+
+(rule
+ (targets
+  (dir base.tex))
+ (action
+  (progn
+   (run mkdir base.tex)
+   (run touch base.tex/base.base.tex))))
+
+(coq.theory
+ (name base)
+ (package base)
+ (modules base)
+ (synopsis "Base Coq library"))

test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/dune-project

@@ -0,0 +1,6 @@
+(lang dune 3.1)
+(using directory-targets 0.1)
+(using coq 0.3)
+
+(package
+ (name base))

test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/run.t

@@ -0,0 +1,8 @@
+We try to build the documentation but there will be a clash between the
+directory targets. Notice how the tex one fails before html one.
+  $ dune build @check
+  Error: the following both define the directory target:
+  _build/default/base.tex
+  - dune:9
+  - dune:18
+  [1]

test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/A/AB/ab.v

@@ -0,0 +1 @@
+Require Import AA.aa.

test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/A/dune

@@ -0,0 +1,3 @@
+(include_subdirs qualified)
+(coq.theory
+ (name A))

test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/B/b.v

@@ -0,0 +1 @@
+From A Require Import AB.ab.

test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/B/dune

@@ -0,0 +1,5 @@
+(include_subdirs qualified)
+
+(coq.theory
+ (name B)
+ (theories A))

test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/dune-project

@@ -0,0 +1,3 @@
+(lang dune 3.0)
+(using coq 0.3)
+(name CoqTest)