[coq] Ignore contents in coqdep rule

This should help reduce the coqdep calls drastically.

Improves #5100 .

In particular, while a build from scratch has still one coqdep call
per file overhead, incremental builds don't anymore. This makes one
coqdep call per theory (or `-modules`) much less critical.

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

CHANGES.md

@@ -24,6 +24,9 @@
 - Dune will not fail if some directories are non-empty when uninstalling.
   (#5543, fixes #5542, @nojb)
 
+- `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 =

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}