feature(coq): call coqdep once per theory

CHANGES.md

@@ -1,6 +1,8 @@
 Unreleased
 ----------
 
+- coqdep is now called once per theory (#7048, @Alizter)
+
 - Add map_workspace_root dune-project stanza to allow disabling of
   mapping of workspace root to /workspace_root. (#6988, fixes #6929,
   @richardlford)

bin/coq/coqtop.ml

@@ -114,11 +114,23 @@ let term =
               , "DuneExtraction" )
           in
           let* (_ : unit * Dep.Fact.t Dep.Map.t) =
-            let deps =
-              Dune_rules.Coq_rules.deps_of ~dir ~use_stdlib ~wrapper_name
+            let dep_map =
+              Dune_rules.Coq_rules.get_dep_map ~dir ~use_stdlib ~wrapper_name
                 coq_module
             in
-            Action_builder.run deps Eager
+            let vo_target =
+              Path.Build.set_extension ~ext:".vo"
+                (Dune_rules.Coq_module.source coq_module)
+            in
+            Action_builder.(
+              run
+                (bind dep_map ~f:(fun dep_map ->
+                     let vo_deps =
+                       Dune_rules.Coq_rules.Dep_map.find_exn dep_map
+                         (Path.build vo_target)
+                     in
+                     paths vo_deps)))
+              Eager
           in
           let* (args, _) : string list * Dep.Fact.t Dep.Map.t =
             let* args =

src/dune_rules/coq/coq_rules.ml

@@ -249,45 +249,6 @@ let ml_flags_and_ml_pack_rule ~context ~lib_db ~theories_deps
   in
   (ml_flags, mlpack_rule)
 
-let parse_coqdep ~dir ~boot_type ~coq_module (lines : string list) =
-  let source = Coq_module.source coq_module in
-  let invalid phase =
-    User_error.raise
-      [ Pp.textf "coqdep returned invalid output for %s / [phase: %s]"
-          (Path.Build.to_string_maybe_quoted source)
-          phase
-      ; Pp.verbatim (String.concat ~sep:"\n" lines)
-      ]
-  in
-  let line =
-    match lines with
-    | [] | _ :: _ :: _ :: _ -> invalid "line"
-    | [ line ] -> line
-    | [ l1; _l2 ] ->
-      (* .vo is produced before .vio, this is fragile tho *)
-      l1
-  in
-  match String.lsplit2 line ~on:':' with
-  | None -> invalid "split"
-  | Some (basename, deps) -> (
-    let ff = List.hd @@ String.extract_blank_separated_words basename in
-    let depname, _ = Filename.split_extension ff in
-    let modname =
-      String.concat ~sep:"/"
-        Coq_module.(
-          prefix coq_module @ [ Coq_module.Name.to_string (name coq_module) ])
-    in
-    if depname <> modname then invalid "basename";
-    let deps = String.extract_blank_separated_words deps in
-    (* Add prelude deps for when stdlib is in scope and we are not actually
-       compiling the prelude *)
-    let deps = List.map ~f:(Path.relative (Path.build dir)) deps in
-    match boot_type with
-    | `No_boot | `Bootstrap_prelude -> deps
-    | `Bootstrap lib ->
-      Path.relative (Path.build (Coq_lib.src_root lib)) "Init/Prelude.vo"
-      :: deps)
-
 let boot_type ~dir ~use_stdlib ~wrapper_name coq_module =
   let* scope = Scope.DB.find_by_dir dir in
   let+ boot_lib =
@@ -307,19 +268,30 @@ let boot_type ~dir ~use_stdlib ~wrapper_name coq_module =
       if init then `Bootstrap_prelude else `Bootstrap lib
   else `Bootstrap_prelude
 
-let setup_coqdep_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name ~use_stdlib
-    ~source_rule ~ml_flags ~mlpack_rule coq_module =
-  let* boot_type = boot_type ~dir ~use_stdlib ~wrapper_name coq_module in
+let dep_theory_file ~dir ~wrapper_name =
+  Path.Build.relative dir wrapper_name
+  |> Path.Build.set_extension ~ext:".theory.d"
+
+let setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name
+    ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule coq_modules =
+  let* boot_type =
+    (* TODO find the boot type a better way *)
+    boot_type ~dir ~use_stdlib ~wrapper_name (List.hd coq_modules)
+  in
   (* coqdep needs the full source + plugin's mlpack to be present :( *)
-  let source = Coq_module.source coq_module in
+  let sources =
+    List.rev_map
+      ~f:(fun module_ -> Coq_module.source module_ |> Path.build)
+      coq_modules
+  in
   let file_flags =
     [ Command.Args.S
         (coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags)
     ; As [ "-dyndep"; "opt" ]
-    ; Dep (Path.build source)
+    ; Deps sources
     ]
   in
-  let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in
+  let stdout_to = dep_theory_file ~dir ~wrapper_name in
   let* coqdep =
     Super_context.resolve_program sctx "coqdep" ~dir ~loc:(Some loc)
       ~hint:"opam install coq"
@@ -331,17 +303,50 @@ let setup_coqdep_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name ~use_stdlib
     >>> Action_builder.(with_no_targets (goal source_rule))
     >>> Command.run ~dir:(Path.build dir) ~stdout_to coqdep file_flags)
 
-let deps_of ~dir ~use_stdlib ~wrapper_name coq_module =
-  let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in
+module Dep_map = Stdune.Map.Make (Path)
+
+let coqdep_invalid phase line =
+  User_error.raise
+    [ Pp.textf "coqdep returned invalid output [phase: %s]" phase
+    ; Pp.verbatim line
+    ]
+
+let parse_line ~dir ~boot_type line =
+  match String.lsplit2 line ~on:':' with
+  | None -> coqdep_invalid "split" line
+  | Some (basename, deps) ->
+    let target = List.hd @@ String.extract_blank_separated_words basename in
+    (* let depname, ext = Filename.split_extension ff in *)
+    let target = Path.relative (Path.build dir) target in
+    let deps = String.extract_blank_separated_words deps in
+    (* Add prelude deps for when stdlib is in scope and we are not actually
+       compiling the prelude *)
+    let deps = List.map ~f:(Path.relative (Path.build dir)) deps in
+    let deps =
+      match boot_type with
+      | `No_boot | `Bootstrap_prelude -> deps
+      | `Bootstrap lib ->
+        Path.relative (Path.build (Coq_lib.src_root lib)) "Init/Prelude.vo"
+        :: deps
+    in
+    (target, deps)
+
+let get_dep_map ~dir ~boot_type ~wrapper_name :
+    Path.t list Dep_map.t Action_builder.t =
+  let file = dep_theory_file ~dir ~wrapper_name in
   let open Action_builder.O in
-  let* boot_type =
-    Action_builder.of_memo
-    @@ boot_type ~dir ~use_stdlib ~wrapper_name coq_module
-  in
-  Action_builder.dyn_paths_unit
-    (Action_builder.map
-       (Action_builder.lines_of (Path.build stdout_to))
-       ~f:(parse_coqdep ~dir ~boot_type ~coq_module))
+  let f = parse_line ~dir ~boot_type in
+  Action_builder.lines_of (Path.build file) >>| fun lines ->
+  List.map ~f lines |> Dep_map.of_list |> function
+  | Ok map -> map
+  | Error (k, r1, r2) ->
+    User_error.raise
+      [ Pp.textf "problem with dup keys"
+      ; Pp.text (String.concat ~sep:"\n>> " lines)
+      ; Dyn.pp (Path.to_dyn k)
+      ; Dyn.pp (Dyn.list Path.to_dyn r1)
+      ; Dyn.pp (Dyn.list Path.to_dyn r2)
+      ]
 
 let generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog
     ~stanza_flags ~ml_flags ~theories_deps ~theory_dirs coq_module =
@@ -386,21 +391,37 @@ let setup_coqc_rule ~loc ~dir ~sctx ~coqc_dir ~file_targets ~stanza_flags
     coq_module =
   (* Process coqdep and generate rules *)
   let* boot_type = boot_type ~dir ~use_stdlib ~wrapper_name coq_module in
-  let deps_of = deps_of ~dir ~use_stdlib ~wrapper_name coq_module in
+  (* let deps_of = deps_of ~dir ~use_stdlib ~wrapper_name coq_module in *)
   let* coqc = coqc ~loc ~dir ~sctx in
-  let target_obj_files =
-    Command.Args.Hidden_targets
-      (Coq_module.obj_files ~wrapper_name ~mode ~obj_files_mode:Coq_module.Build
-         ~obj_dir:dir coq_module
-      |> List.map ~f:fst)
+  let obj_files =
+    Coq_module.obj_files ~wrapper_name ~mode ~obj_files_mode:Coq_module.Build
+      ~obj_dir:dir coq_module
+    |> List.map ~f:fst
   in
+  let target_obj_files = Command.Args.Hidden_targets obj_files in
   let* args =
     generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~stanza_flags ~ml_flags
       ~theories_deps ~theory_dirs ~mode ~coq_prog:`Coqc coq_module
   in
+  let open Action_builder.O in
+  let vo_target =
+    Path.Build.set_extension ~ext:".vo" (Coq_module.source coq_module)
+  in
+  let deps_of =
+    get_dep_map ~dir ~boot_type ~wrapper_name >>| fun dep_map ->
+    match Dep_map.find dep_map (Path.build vo_target) with
+    | None ->
+      User_error.raise
+        [ Pp.textf "Dep_map.find failed for"
+        ; Dyn.pp (Coq_module.to_dyn coq_module)
+        ; Dyn.pp (Dep_map.to_dyn (Dyn.list Path.to_dyn) dep_map)
+        ]
+    | Some deps -> deps
+  in
+
   let open Action_builder.With_targets.O in
   Super_context.add_rule ~loc ~dir sctx
-    (Action_builder.with_no_targets deps_of
+    (Action_builder.(with_no_targets (Action_builder.bind ~f:paths deps_of))
     >>> Action_builder.With_targets.add ~file_targets
         @@ Command.run ~dir:(Path.build coqc_dir) coqc (target_obj_files :: args)
     (* The way we handle the transitive dependencies of .vo files is not safe for
@@ -558,17 +579,16 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) =
     source_rule ~sctx theories
   in
   let coqc_dir = (Super_context.context sctx).build_dir in
-
   let* mode = select_native_mode ~sctx ~dir s.buildable in
-  Memo.parallel_iter coq_modules
-    ~f:
-      (setup_coqdep_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name
-         ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule)
+  (* First we setup the rule calling coqdep *)
+  setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name
+    ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule coq_modules
   >>> Memo.parallel_iter coq_modules
         ~f:
           (setup_coqc_rule ~loc ~dir ~sctx ~file_targets:[] ~stanza_flags
              ~coqc_dir ~theories_deps ~mode ~wrapper_name ~use_stdlib ~ml_flags
              ~theory_dirs)
+  (* And finally the coqdoc rules *)
   >>> setup_coqdoc_rules ~sctx ~dir ~theories_deps s coq_modules
 
 let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t)
@@ -727,10 +747,11 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents
     let lib_db = Scope.libs scope in
     ml_flags_and_ml_pack_rule ~context ~theories_deps ~lib_db s.buildable
   in
+  let loc = s.buildable.loc in
+  let use_stdlib = s.buildable.use_stdlib in
   let* mode = select_native_mode ~sctx ~dir s.buildable in
-  setup_coqdep_rule ~sctx ~loc:s.buildable.loc ~source_rule ~dir ~theories_deps
-    ~wrapper_name ~use_stdlib:s.buildable.use_stdlib ~ml_flags ~mlpack_rule
-    coq_module
+  setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name
+    ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule [ coq_module ]
   >>> setup_coqc_rule ~file_targets ~stanza_flags:s.buildable.flags ~sctx
         ~loc:s.buildable.loc ~coqc_dir:dir coq_module ~dir ~theories_deps ~mode
         ~wrapper_name ~use_stdlib:s.buildable.use_stdlib ~ml_flags
@@ -754,3 +775,11 @@ let coqtop_args_extraction ~sctx ~dir (s : Coq_stanza.Extraction.t) coq_module =
   generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog:`Coqtop
     ~stanza_flags:s.buildable.flags ~ml_flags ~theories_deps
     ~theory_dirs:Path.Build.Set.empty coq_module
+
+(* Version for export *)
+let get_dep_map ~dir ~use_stdlib ~wrapper_name coq_module =
+  let open Action_builder.O in
+  let* boot_type =
+    Action_builder.of_memo (boot_type ~dir ~use_stdlib ~wrapper_name coq_module)
+  in
+  get_dep_map ~dir ~boot_type ~wrapper_name

src/dune_rules/coq/coq_rules.mli

@@ -5,14 +5,15 @@ open Import
 (* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
-(** [deps_of ~dir ~use_stdlib ~wrapper_name m] produces an action builder that
-    can be run to build all dependencies of the Coq module [m]. *)
-val deps_of :
+module Dep_map : Map.S with type key := Path.t
+
+(** [get_dep_map] produces a dep map for a theory *)
+val get_dep_map :
      dir:Path.Build.t
   -> use_stdlib:bool
   -> wrapper_name:string
   -> Coq_module.t
-  -> unit Dune_engine.Action_builder.t
+  -> Path.t list Dep_map.t Dune_engine.Action_builder.t
 
 val coqdoc_directory_targets :
   dir:Path.Build.t -> Coq_stanza.Theory.t -> Loc.t Path.Build.Map.t

test/blackbox-tests/test-cases/coq/base-unsound.t/run.t

@@ -1,5 +1,4 @@
   $ dune build --display short --profile unsound --debug-dependency-path @all
-        coqdep bar.v.d
-        coqdep foo.v.d
+        coqdep basic.theory.d
           coqc foo.{glob,vo}
           coqc bar.{glob,vo}

test/blackbox-tests/test-cases/coq/base.t/run.t

@@ -1,6 +1,5 @@
   $ dune build --display short --debug-dependency-path @all
-        coqdep bar.v.d
-        coqdep foo.v.d
+        coqdep basic.theory.d
           coqc foo.{glob,vo}
           coqc bar.{glob,vo}
 

test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t

@@ -4,8 +4,7 @@ We check cycles are detected
      theory A in A
   -> theory B in B
   -> theory A in A
-  -> required by _build/default/A/a.v.d
-  -> required by _build/default/A/a.glob
+  -> required by _build/default/A/A.theory.d
   -> required by alias A/all
   -> required by alias default
   [1]

test/blackbox-tests/test-cases/coq/compose-installed.t/run.t

@@ -12,8 +12,7 @@ TODO: Currently this is not supported so the output is garbage
                  ^
   Theory B not found
   -> required by theory A in .
-  -> required by _build/default/a.v.d
-  -> required by _build/default/a.glob
+  -> required by _build/default/A.theory.d
   -> required by alias all
   -> required by alias default
   [1]

test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t

@@ -1,11 +1,11 @@
   $ dune build --display short --debug-dependency-path @all
-        coqdep thy1/a.v.d
+        coqdep thy1/thy1.theory.d
         ocamlc src_b/.ml_plugin_b.objs/byte/ml_plugin_b.{cmi,cmo,cmt}
       ocamldep src_b/.ml_plugin_b.objs/ml_plugin_b__Simple_b.impl.d
         ocamlc src_a/.ml_plugin_a.objs/byte/ml_plugin_a.{cmi,cmo,cmt}
       ocamldep src_a/.ml_plugin_a.objs/ml_plugin_a__Gram.intf.d
       ocamldep src_a/.ml_plugin_a.objs/ml_plugin_a__Simple.impl.d
-        coqdep thy2/a.v.d
+        coqdep thy2/thy2.theory.d
          coqpp src_a/gram.ml
       ocamlopt src_b/.ml_plugin_b.objs/native/ml_plugin_b.{cmx,o}
       ocamlopt src_a/.ml_plugin_a.objs/native/ml_plugin_a.{cmx,o}

test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t

@@ -7,7 +7,7 @@ dependencies.
   -> theory B in B
   -> theory C in C
   -> theory A in A
-  -> required by _build/default/A/a.v.d
+  -> required by _build/default/A/A.theory.d
   -> required by _build/default/A/a.vo
   -> required by _build/install/default/lib/coq/user-contrib/A/a.vo
   -> required by _build/default/A/A.install
@@ -21,7 +21,7 @@ dependencies.
   -> theory C in C
   -> theory A in A
   -> theory B in B
-  -> required by _build/default/B/b.v.d
+  -> required by _build/default/B/B.theory.d
   -> required by _build/default/B/b.vo
   -> required by _build/install/default/lib/coq/user-contrib/B/b.vo
   -> required by _build/default/B/B.install
@@ -35,7 +35,7 @@ dependencies.
   -> theory A in A
   -> theory B in B
   -> theory C in C
-  -> required by _build/default/C/c.v.d
+  -> required by _build/default/C/C.theory.d
   -> required by _build/default/C/c.vo
   -> required by _build/install/default/lib/coq/user-contrib/C/c.vo
   -> required by _build/default/C/C.install

test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t

@@ -8,7 +8,7 @@ dependency.
   Theory A not found
   -> required by theory B in B
   -> required by theory C in C
-  -> required by _build/default/C/c.v.d
+  -> required by _build/default/C/C.theory.d
   -> required by _build/default/C/c.vo
   -> required by _build/install/default/lib/coq/user-contrib/C/c.vo
   -> required by _build/default/C/C.install

test/blackbox-tests/test-cases/coq/compose-self.t/run.t

@@ -2,8 +2,7 @@ Composing a theory with itself should cause a cycle
   $ dune build
   Error: Dependency cycle between:
      theory A in A
-  -> required by _build/default/A/a.v.d
-  -> required by _build/default/A/a.glob
+  -> required by _build/default/A/A.theory.d
   -> required by alias A/all
   -> required by alias default
   [1]