Skip to content

Commit

Permalink
[coq] Ignore contents in coqdep rule
Browse files Browse the repository at this point in the history
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>
  • Loading branch information
ejgallego committed Apr 6, 2022
1 parent 3787d76 commit 10fb5ae
Show file tree
Hide file tree
Showing 7 changed files with 41 additions and 1 deletion.
3 changes: 3 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
------------------

Expand Down
2 changes: 1 addition & 1 deletion src/dune_rules/coq_rules.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Definition foo := 3.
3 changes: 3 additions & 0 deletions test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/a/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
(coq.theory
(name a)
(package csimple))
Empty file.
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
(lang dune 2.5)

(using coq 0.2)
30 changes: 30 additions & 0 deletions test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t
Original file line number Diff line number Diff line change
@@ -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}

0 comments on commit 10fb5ae

Please sign in to comment.