Skip to content

Commit

Permalink
Add reproduction test case for #10149.
Browse files Browse the repository at this point in the history
Signed-off-by: Rodolphe Lepigre <rodolphe@bedrocksystems.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
  • Loading branch information
Rodolphe Lepigre authored and Alizter committed Apr 20, 2024
1 parent 1d5f97c commit 3bf70e1
Showing 1 changed file with 18 additions and 0 deletions.
18 changes: 18 additions & 0 deletions test/blackbox-tests/test-cases/coq/no-rebuild-on-dep-change.t
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
$ echo "(coq.theory (name bug) (mode vo))" > dune
$ echo "(lang dune 3.12)" > dune-project
$ echo "(using coq 0.8)" >> dune-project
$ touch root.v leaf.v
$ dune build
$ find _build -name "*.vo" | sort
_build/default/leaf.vo
_build/default/root.vo
$ echo "Require Import bug.root." >> leaf.v

This test makes sure that a full rebuild is not triggered when the output of
coqdep is changed.

Currently this is the case and a bug:
$ dune build --display=short
coqdep .bug.theory.d
coqc root.{glob,vo}
coqc leaf.{glob,vo}

0 comments on commit 3bf70e1

Please sign in to comment.