[coq] Ignore contents in coqdep rule

This should help reduce the coqdep calls drastically.

Improves ocaml#5100 .

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

CHANGES.md

@@ -19,6 +19,9 @@
 - Fix operations that remove folders with absolute path. This happens when
   using esy (#5507, @EduardoRFS)
 
+- `coqdep` now depends only on the filesystem layout of the .v files,
+  and not on their contents (#5547 , helps with #5100 , @ejgallego)
+
 3.0.3 (Unreleased)
 ------------------
 

src/dune_rules/coq_rules.ml

@@ -346,7 +346,7 @@ let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module =
   (* Coqdep has to be called in the stanza's directory *)
   let open Action_builder.With_targets.O in
   Action_builder.with_no_targets cctx.mlpack_rule
-  >>> Action_builder.with_no_targets source_rule
+  >>> Action_builder.(with_no_targets (goal source_rule))
   >>> Command.run ~dir:(Path.build cctx.dir) ~stdout_to cctx.coqdep file_flags
 
 let coqc_rule (cctx : _ Context.t) ~file_flags coq_module =
@@ -566,7 +566,7 @@ let extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) =
   let source_rule =
     let theories = source_rule ~sctx cctx.theories_deps in
     let open Action_builder.O in
-    theories >>> Action_builder.path (Path.build (Coq_module.source coq_module))
+    theories >>> Action_builder.(path (Path.build (Coq_module.source coq_module)))
   in
   let { Module_rule.coqc; coqdep } = setup_rule cctx ~source_rule coq_module in
   let coqc = Action_builder.With_targets.add coqc ~file_targets:ml_targets in

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

@@ -0,0 +1 @@
+Definition foo := 3.

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

@@ -0,0 +1,3 @@
+(coq.theory
+ (name a)
+ (package csimple))

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

@@ -0,0 +1,3 @@
+(lang dune 2.5)
+
+(using coq 0.2)

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

@@ -0,0 +1,30 @@
+  $ mkdir b
+  $ cat > b/dune <<EOF
+  > (coq.theory
+  >  (name b)
+  >  (theories a)
+  >  (package csimple))
+  > EOF
+  $ cat > b/b.v <<EOF
+  > From a Require Import a.
+  > Definition bar := a.foo.
+  > EOF
+  $ cat > b/d.v <<EOF
+  > From a Require Import a.
+  > 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
+          coqc a/.a.aux,a/a.{glob,vo}
+          coqc b/.b.aux,b/b.{glob,vo}
+          coqc b/.d.aux,b/d.{glob,vo}
+  $ cat > b/b.v <<EOF
+  > From a Require Import a.
+  > Definition bar := a.foo.
+  > Definition zoo := 4.
+  > EOF
+  $ dune build --display short --debug-dependency-path
+        coqdep b/b.v.d
+          coqc b/.b.aux,b/b.{glob,vo}