From 10fb5aef40c49f1e350a034ec71b2aa597fa6fae Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 5 Apr 2022 20:15:57 +0200
Subject: [PATCH] [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                                    |  3 ++
 src/dune_rules/coq_rules.ml                   |  2 +-
 .../test-cases/coq/coqdep-on-rebuild.t/a/a.v  |  1 +
 .../test-cases/coq/coqdep-on-rebuild.t/a/dune |  3 ++
 .../coq/coqdep-on-rebuild.t/csimple.opam      |  0
 .../coq/coqdep-on-rebuild.t/dune-project      |  3 ++
 .../test-cases/coq/coqdep-on-rebuild.t/run.t  | 30 +++++++++++++++++++
 7 files changed, 41 insertions(+), 1 deletion(-)
 create mode 100644 test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/a/a.v
 create mode 100644 test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/a/dune
 create mode 100644 test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/csimple.opam
 create mode 100644 test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/dune-project
 create mode 100644 test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t

diff --git a/CHANGES.md b/CHANGES.md
index 4c3d77713f4..cf5e8342397 100644
--- a/CHANGES.md
+++ b/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)
 ------------------
 
diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml
index 9ba3397496a..5ecfb9ce76c 100644
--- a/src/dune_rules/coq_rules.ml
+++ b/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 =
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/a/a.v b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/a/a.v
new file mode 100644
index 00000000000..d4389c6d37d
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/a/a.v
@@ -0,0 +1 @@
+Definition foo := 3.
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/a/dune b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/a/dune
new file mode 100644
index 00000000000..099b8f56a24
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/a/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name a)
+ (package csimple))
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/csimple.opam b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/csimple.opam
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/dune-project b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/dune-project
new file mode 100644
index 00000000000..9ef6b81a34a
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/dune-project
@@ -0,0 +1,3 @@
+(lang dune 2.5)
+
+(using coq 0.2)
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t
new file mode 100644
index 00000000000..24b83fc9991
--- /dev/null
+++ b/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}