[coq] Add .aux files as targets

Fix #3437 Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
ocaml · Aug 18, 2020 · fa68c82 · fa68c82
1 parent 48a5db7
commit fa68c82
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 16 deletions.
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/main.t/run.t b/test/blackbox-tests/test-cases/coq/main.t/run.t
@@ -2,26 +2,26 @@
   Entering directory 'base'
         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 --root base_unsound --display short --profile unsound --debug-dependency-path @all
   Entering directory 'base_unsound'
         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 --root rec_module --display short --debug-dependency-path @all
   Entering directory 'rec_module'
         coqdep a/bar.v.d
         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 --root ml_lib --display short --debug-dependency-path @all
   Entering directory 'ml_lib'
@@ -48,7 +48,7 @@
       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
 
   $ dune build --root base --debug-dependency-path @default
   Entering directory 'base'
@@ -86,8 +86,8 @@
   Entering directory 'compose_simple'
         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"
@@ -126,8 +126,8 @@
       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
 
 # Test only works on Coq 8.12 due to boot constraints
 # $ dune build --root compose_boot/ --display short --debug-dependency-path
@@ -181,8 +181,8 @@
   Entering directory 'compose_sub_theory'
         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"