feature(coq): call coqdep once per theory

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: caa26aa8-d2fa-4df5-8f47-58eb642c07d5 -->

src/dune_rules/coq/coq_module.ml

@@ -66,6 +66,10 @@ let dep_file x ~obj_dir =
   let vo_dir = build_vo_dir ~obj_dir x in
   Path.Build.relative vo_dir (x.name ^ ".v.d")
 
+let vo_file x ~obj_dir =
+  let vo_dir = build_vo_dir ~obj_dir x in
+  Path.Build.relative vo_dir (x.name ^ ".vo")
+
 type obj_files_mode =
   | Build
   | Install

src/dune_rules/coq/coq_module.mli

@@ -42,6 +42,8 @@ val dep_file : t -> obj_dir:Path.Build.t -> Path.Build.t
 
 val glob_file : t -> obj_dir:Path.Build.t -> Path.Build.t
 
+val vo_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/coq_rules.ml

@@ -307,6 +307,73 @@ let boot_type ~dir ~use_stdlib ~wrapper_name coq_module =
       if init then `Bootstrap_prelude else `Bootstrap lib
   else `Bootstrap_prelude
 
+let setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name
+    ~use_stdlib ~source_rule ~ml_flags ~mlpack_rule ~theory_name 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 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" ]
+    ; Deps sources
+    ]
+  in
+  let stdout_to =
+    Path.Build.relative dir (Coq_lib_name.to_string theory_name)
+    |> Path.Build.set_extension ~ext:".theory.d"
+  in
+  let* coqdep =
+    Super_context.resolve_program sctx "coqdep" ~dir ~loc:(Some loc)
+      ~hint:"opam install coq"
+  in
+  (* Coqdep has to be called in the stanza's directory *)
+  Super_context.add_rule ~loc sctx ~dir
+    (let open Action_builder.With_targets.O in
+    Action_builder.with_no_targets mlpack_rule
+    >>> Action_builder.(with_no_targets (goal source_rule))
+    >>> Command.run ~dir:(Path.build dir) ~stdout_to coqdep file_flags)
+
+let setup_coqdep_for_mod_rule ~loc ~sctx ~dir ~wrapper_name coq_module =
+  let theory_deps_file =
+    Path.Build.relative dir wrapper_name
+    |> Path.Build.set_extension ~ext:".theory.d"
+    |> Path.build
+  in
+  let deps_file = Coq_module.dep_file ~obj_dir:dir coq_module in
+  let vo_file =
+    String.concat ~sep:"/"
+      (Coq_module.prefix coq_module
+      @ [ Coq_module.Name.to_string (Coq_module.name coq_module) ])
+    ^ ".vo"
+  in
+  let action =
+    let line =
+      let open Action_builder.O in
+      let+ lines = Action_builder.lines_of theory_deps_file in
+      List.find ~f:(String.is_prefix ~prefix:vo_file) lines |> function
+      | None ->
+        Code_error.raise "coqdep output doesn't match theory modules"
+          [ ("theory_deps_file", Path.to_dyn theory_deps_file)
+          ; ("vo_file", Dyn.string vo_file)
+          ; ("lines", Dyn.list Dyn.string lines)
+          ; ("coq_module", Coq_module.to_dyn coq_module)
+          ; ("dir", Path.to_dyn (Path.build dir))
+          ; ("wrapper_name", Dyn.string wrapper_name)
+          ]
+      | Some line -> line
+    in
+    Action_builder.write_file_dyn deps_file line
+  in
+  Super_context.add_rule ~loc sctx ~dir action
+
 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
@@ -558,17 +625,21 @@ 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)
+  let theory_name = snd s.name in
+  (* 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 ~theory_name coq_modules
+  (* Next the rules filtering that file per module *)
+  >>> Memo.parallel_iter coq_modules
+        ~f:(setup_coqdep_for_mod_rule ~sctx ~dir ~loc ~wrapper_name)
+  (* Then we setup the coqc rules *)
   >>> 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)

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,6 +7,7 @@ dependencies.
   -> theory B in B
   -> theory C in C
   -> theory A in A
+  -> required by _build/default/A/A.theory.d
   -> required by _build/default/A/a.v.d
   -> required by _build/default/A/a.vo
   -> required by _build/install/default/lib/coq/user-contrib/A/a.vo
@@ -21,6 +22,7 @@ dependencies.
   -> theory C in C
   -> theory A in A
   -> theory B in B
+  -> required by _build/default/B/B.theory.d
   -> required by _build/default/B/b.v.d
   -> required by _build/default/B/b.vo
   -> required by _build/install/default/lib/coq/user-contrib/B/b.vo
@@ -35,6 +37,7 @@ dependencies.
   -> theory A in A
   -> theory B in B
   -> theory C in C
+  -> required by _build/default/C/C.theory.d
   -> required by _build/default/C/c.v.d
   -> required by _build/default/C/c.vo
   -> required by _build/install/default/lib/coq/user-contrib/C/c.vo

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

@@ -8,6 +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.theory.d
   -> required by _build/default/C/c.v.d
   -> required by _build/default/C/c.vo
   -> required by _build/install/default/lib/coq/user-contrib/C/c.vo

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]

test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t

@@ -14,9 +14,8 @@
   > Definition doo := a.foo.
   > EOF
   $ dune build --display short --debug-dependency-path
-        coqdep a/a.v.d
-        coqdep b/b.v.d
-        coqdep b/d.v.d
+        coqdep a/a.theory.d
+        coqdep b/b.theory.d
           coqc a/Na_a.{cmi,cmxs},a/a.{glob,vo}
           coqc b/Nb_b.{cmi,cmxs},b/b.{glob,vo}
           coqc b/Nb_d.{cmi,cmxs},b/d.{glob,vo}
@@ -26,5 +25,5 @@
   > Definition zoo := 4.
   > EOF
   $ dune build --display short --debug-dependency-path
-        coqdep b/b.v.d
+        coqdep b/b.theory.d
           coqc b/Nb_b.{cmi,cmxs},b/b.{glob,vo}

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

@@ -20,6 +20,7 @@ Next we build the doc for the second theory
   $ dune build @B/doc
 Check that the first theory doc is not built
   $ ls _build/default/A/
+  A.theory.d
   AA
   AB
 Check that the second theory doc is built
@@ -52,6 +53,7 @@ Next we build the doc for the second theory
   $ dune build @B/doc-latex
 Check that the first theory doc is not built
   $ ls _build/default/A
+  A.theory.d
   AA
   AB
 Check that the second theory doc is built

test/blackbox-tests/test-cases/coq/coqdoc-with-boot.t/run.t

@@ -4,6 +4,7 @@ Testing coqdoc when composed with a boot library
 
   $ ls _build/default/A
   A.html
+  A.theory.d
   a.glob
   a.v
   a.v.d

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

@@ -32,6 +32,7 @@ Note that this currently works due to a bug in @all detecting directory targets.
   bar.vos
   base.dune-package
   base.install
+  basic.theory.d
   foo.glob
   foo.v
   foo.v.d

test/blackbox-tests/test-cases/coq/coqtop/coqtop-recomp.t

@@ -19,17 +19,15 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   > (using coq 0.3)
   > EOF
   $ dune coq top --display short --toplevel echo dir/bar.v
-        coqdep dir/bar.v.d
-        coqdep dir/foo.v.d
+        coqdep dir/basic.theory.d
           coqc dir/foo.{glob,vo}
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/dir basic
   $ dune coq top --display short --toplevel echo dir/bar.v
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/dir basic
   $ dune clean
   $ (cd dir && dune coq top --root .. --display short --toplevel echo dir/bar.v)
   Entering directory '..'
-        coqdep dir/bar.v.d
-        coqdep dir/foo.v.d
+        coqdep dir/basic.theory.d
           coqc dir/foo.{glob,vo}
   Leaving directory '..'
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R $TESTCASE_ROOT/_build/default/dir basic

test/blackbox-tests/test-cases/coq/ml-lib.t/run.t

@@ -1,5 +1,5 @@
   $ dune build --display short --debug-dependency-path @all
-        coqdep theories/a.v.d
+        coqdep theories/Plugin.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}

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

@@ -1,7 +1,6 @@
   $ dune build --profile=release --display short --debug-dependency-path @all
-        coqdep bar/bar.v.d
-        coqdep foo/foo.v.d
-        coqdep foo/a/a.v.d
+        coqdep bar/bar.theory.d
+        coqdep foo/foo.theory.d
           coqc foo/Nfoo_foo.{cmi,cmxs},foo/foo.{glob,vo}
           coqc foo/a/Nfoo_a_a.{cmi,cmxs},foo/a/a.{glob,vo}
           coqc bar/Nbar_baz_bar.{cmi,cmxs},bar/bar.{glob,vo}

test/blackbox-tests/test-cases/coq/native-single.t/run.t

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

test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t

@@ -2,7 +2,7 @@ Test that when `(stdlib no)` is provided, the standard library is not bound to `
 and the prelude is not imported
 
   $ dune build --display=short foo.vo
-        coqdep foo.v.d
+        coqdep basic.theory.d
   *** Warning: in file foo.v, library Prelude is required from root Coq and has not been found in the loadpath!
           coqc foo.{glob,vo} (exit 1)
   File "./foo.v", line 1, characters 0-32:
@@ -12,7 +12,6 @@ and the prelude is not imported
   [1]
 
   $ dune build --display=short bar.vo
-        coqdep bar.v.d
           coqc bar.{glob,vo} (exit 1)
   File "./bar.v", line 1, characters 20-23:
   Error: The reference nat was not found in the current environment.

test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t

@@ -5,6 +5,7 @@
   Theory "private" is private, it cannot be a dependency of a public theory.
   You need to associate "private" to a package.
   -> required by theory public in public
+  -> required by _build/default/public/public.theory.d
   -> required by _build/default/public/b.v.d
   -> required by _build/default/public/b.vo
   -> required by _build/install/default/lib/coq/user-contrib/public/b.vo

test/blackbox-tests/test-cases/coq/rec-module.t/run.t

@@ -1,8 +1,5 @@
   $ dune build --display short --debug-dependency-path @all
-        coqdep a/bar.v.d
-        coqdep b/foo.v.d
-        coqdep c/d/bar.v.d
-        coqdep c/ooo.v.d
+        coqdep rec_module.theory.d
           coqc b/foo.{glob,vo}
           coqc c/d/bar.{glob,vo}
           coqc c/ooo.{glob,vo}