[coq] Add .aux files as targets

Fix #3437 Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
ocaml · Aug 21, 2020 · 8d30a98 · 8d30a98
1 parent e05b428
commit 8d30a98
Show file tree

Hide file tree

Showing 11 changed files with 28 additions and 16 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,3 +1,8 @@
+Unreleased
+----------
+
+- Add missing `.aux` targets to coq rules (3721, fixes #3437, @rgrinberg)
+
 2.7.0 (13/08/2020)
 ------------------
 

diff --git a/src/dune/coq_module.ml b/src/dune/coq_module.ml
@@ -41,6 +41,10 @@ let dep_file x ~obj_dir =
   let vo_dir = build_vo_dir ~obj_dir x in
   Path.Build.relative vo_dir (x.name ^ ".v.d")
 
+let aux_file x ~obj_dir =
+  let vo_dir = build_vo_dir ~obj_dir x in
+  Path.Build.relative vo_dir ("." ^ x.name ^ ".aux")
+
 let obj_file x ~obj_dir =
   let vo_dir = build_vo_dir ~obj_dir x in
   Path.Build.relative vo_dir (x.name ^ ".vo")

diff --git a/src/dune/coq_module.mli b/src/dune/coq_module.mli
@@ -38,6 +38,8 @@ val name : t -> Name.t
 
 val dep_file : t -> obj_dir:Path.Build.t -> Path.Build.t
 
+val aux_file : t -> obj_dir:Path.Build.t -> Path.Build.t
+
 val obj_file : t -> obj_dir:Path.Build.t -> Path.Build.t
 
 val to_dyn : t -> Dyn.t

diff --git a/src/dune/coq_rules.ml b/src/dune/coq_rules.ml
@@ -265,7 +265,8 @@ let coqc_rule (cctx : _ Context.t) ~file_flags coq_module =
   let source = Coq_module.source coq_module in
   let file_flags =
     let object_to = Coq_module.obj_file ~obj_dir:cctx.dir coq_module in
-    [ Command.Args.Hidden_targets [ object_to ]
+    let aux = Coq_module.aux_file ~obj_dir:cctx.dir coq_module in
+    [ Command.Args.Hidden_targets [ object_to; aux ]
     ; S file_flags
     ; Command.Args.Dep (Path.build source)
     ]

diff --git a/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t b/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t
@@ -1,5 +1,5 @@
   $ dune build --display short --profile unsound --debug-dependency-path @all
         coqdep bar.v.d
         coqdep foo.v.d
-          coqc foo.vo
-          coqc bar.vo
+          coqc .foo.aux,foo.vo
+          coqc .bar.aux,bar.vo
diff --git a/test/blackbox-tests/test-cases/coq/base.t/run.t b/test/blackbox-tests/test-cases/coq/base.t/run.t
@@ -1,8 +1,8 @@
   $ dune build --display short --debug-dependency-path @all
         coqdep bar.v.d
         coqdep foo.v.d
-          coqc foo.vo
-          coqc bar.vo
+          coqc .foo.aux,foo.vo
+          coqc .bar.aux,bar.vo
 
   $ dune build --debug-dependency-path @default
   lib: [

diff --git a/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t b/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t
@@ -23,5 +23,5 @@
       ocamlopt src_b/ml_plugin_b.{a,cmxa}
       ocamlopt src_a/ml_plugin_a.cmxs
       ocamlopt src_b/ml_plugin_b.cmxs
-          coqc thy1/a.vo
-          coqc thy2/a.vo
+          coqc thy1/.a.aux,thy1/a.vo
+          coqc thy2/.a.aux,thy2/a.vo
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t b/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t
@@ -1,8 +1,8 @@
   $ dune build --display short --debug-dependency-path
         coqdep a/a.v.d
         coqdep b/b.v.d
-          coqc a/a.vo
-          coqc b/b.vo
+          coqc a/.a.aux,a/a.vo
+          coqc b/.b.aux,b/b.vo
   lib: [
     "_build/install/default/lib/csimple/META"
     "_build/install/default/lib/csimple/dune-package"

diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t
@@ -1,8 +1,8 @@
   $ dune build --display short --debug-dependency-path
         coqdep b/b.v.d
         coqdep a/a.v.d
-          coqc a/a.vo
-          coqc b/b.vo
+          coqc a/.a.aux,a/a.vo
+          coqc b/.b.aux,b/b.vo
   lib: [
     "_build/install/default/lib/subtheory/META"
     "_build/install/default/lib/subtheory/dune-package"

diff --git a/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t b/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t
@@ -22,4 +22,4 @@
       ocamlopt src_b/ml_plugin_b.{a,cmxa}
       ocamlopt src_a/ml_plugin_a.cmxs
       ocamlopt src_b/ml_plugin_b.cmxs
-          coqc theories/a.vo
+          coqc theories/.a.aux,theories/a.vo
diff --git a/test/blackbox-tests/test-cases/coq/rec-module.t/run.t b/test/blackbox-tests/test-cases/coq/rec-module.t/run.t
@@ -3,10 +3,10 @@
         coqdep b/foo.v.d
         coqdep c/d/bar.v.d
         coqdep c/ooo.v.d
-          coqc b/foo.vo
-          coqc c/d/bar.vo
-          coqc c/ooo.vo
-          coqc a/bar.vo
+          coqc b/.foo.aux,b/foo.vo
+          coqc c/d/.bar.aux,c/d/bar.vo
+          coqc c/.ooo.aux,c/ooo.vo
+          coqc a/.bar.aux,a/bar.vo
 
   $ dune build --debug-dependency-path @default
   lib: [