remove .aux targets from coqc rule

ps-id: 2b8b57f9-f39d-4162-a2aa-31505e430304 Signed-off-by: Ali Caglayan <[email protected]>
ocaml · Aug 7, 2022 · 83252ff · 83252ff
1 parent cda8801
commit 83252ff
Show file tree

Hide file tree

Showing 16 changed files with 41 additions and 30 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -4,6 +4,9 @@
 - Do not ignore rules marked `(promote (until-clean))` when
   `--ignore-promoted-rules` (or `-p`) is passed. (#6010, fixes #4401, @emillon)
 
+- Dune no longer considers .aux files as targets during Coq compilation. This
+  means that .aux files are no longer cached. (#6024, fixes #6004, @alizter)
+
 3.4.1 (26-07-2022)
 ------------------
 

diff --git a/src/dune_rules/coq_module.ml b/src/dune_rules/coq_module.ml
@@ -92,7 +92,7 @@ let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode =
   in
   let obj_files =
     match obj_files_mode with
-    | Build -> [ x.name ^ ".vo"; "." ^ x.name ^ ".aux"; x.name ^ ".glob" ]
+    | Build -> [ x.name ^ ".vo"; x.name ^ ".glob" ]
     | Install -> [ x.name ^ ".vo" ]
   in
   List.map obj_files ~f:(fun fname ->

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.aux,foo.{glob,vo}
-          coqc .bar.aux,bar.{glob,vo}
+          coqc foo.{glob,vo}
+          coqc bar.{glob,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.aux,foo.{glob,vo}
-          coqc .bar.aux,bar.{glob,vo}
+          coqc foo.{glob,vo}
+          coqc bar.{glob,vo}
 
   $ dune build --debug-dependency-path @default
   lib: [

diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t
@@ -5,7 +5,7 @@ We check cycles are detected
   -> theory B in B
   -> theory A in A
   -> required by _build/default/A/a.v.d
-  -> required by _build/default/A/.a.aux
+  -> required by _build/default/A/a.glob
   -> required by alias A/all
   -> required by alias default
   [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t
@@ -13,7 +13,7 @@ TODO: Currently this is not supported so the output is garbage
   Theory B not found
   -> required by theory A in .
   -> required by _build/default/a.v.d
-  -> required by _build/default/.a.aux
+  -> required by _build/default/a.glob
   -> required by alias all
   -> required by alias default
   [1]

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.aux,thy1/a.{glob,vo}
-          coqc thy2/.a.aux,thy2/a.{glob,vo}
+          coqc thy1/a.{glob,vo}
+          coqc thy2/a.{glob,vo}
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t
@@ -8,7 +8,9 @@ dependencies.
   -> theory C in C
   -> theory A in A
   -> required by _build/default/A/a.v.d
-  -> required by _build/default/A/.a.aux
+  -> required by _build/default/A/a.vo
+  -> required by _build/install/default/lib/coq/user-contrib/A/a.vo
+  -> required by _build/default/A/A.install
   -> required by alias A/all
   -> required by alias A/default
   [1]
@@ -20,7 +22,9 @@ dependencies.
   -> theory A in A
   -> theory B in B
   -> required by _build/default/B/b.v.d
-  -> required by _build/default/B/.b.aux
+  -> required by _build/default/B/b.vo
+  -> required by _build/install/default/lib/coq/user-contrib/B/b.vo
+  -> required by _build/default/B/B.install
   -> required by alias B/all
   -> required by alias B/default
   [1]
@@ -32,7 +36,9 @@ dependencies.
   -> theory B in B
   -> theory C in C
   -> required by _build/default/C/c.v.d
-  -> required by _build/default/C/.c.aux
+  -> required by _build/default/C/c.vo
+  -> required by _build/install/default/lib/coq/user-contrib/C/c.vo
+  -> required by _build/default/C/C.install
   -> required by alias C/all
   -> required by alias C/default
   [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t
@@ -9,7 +9,9 @@ dependency.
   -> required by theory B in B
   -> required by theory C in C
   -> required by _build/default/C/c.v.d
-  -> required by _build/default/C/.c.aux
+  -> required by _build/default/C/c.vo
+  -> required by _build/install/default/lib/coq/user-contrib/C/c.vo
+  -> required by _build/default/C/C.install
   -> required by alias C/all
   -> required by alias C/default
   [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-self.t/run.t b/test/blackbox-tests/test-cases/coq/compose-self.t/run.t
@@ -3,7 +3,7 @@ Composing a theory with itself should cause a cycle
   Error: Dependency cycle between:
      theory A in A
   -> required by _build/default/A/a.v.d
-  -> required by _build/default/A/.a.aux
+  -> required by _build/default/A/a.glob
   -> required by alias A/all
   -> required by alias default
   [1]
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
@@ -17,14 +17,14 @@
         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}
+          coqc a/a.{glob,vo}
+          coqc b/b.{glob,vo}
+          coqc 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}
+          coqc b/b.{glob,vo}
diff --git a/test/blackbox-tests/test-cases/coq/coqtop-recomp.t b/test/blackbox-tests/test-cases/coq/coqtop-recomp.t
@@ -21,7 +21,7 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   $ dune coq top --display short --toplevel echo dir/bar.v
         coqdep dir/bar.v.d
         coqdep dir/foo.v.d
-          coqc dir/.foo.aux,dir/foo.{glob,vo}
+          coqc dir/foo.{glob,vo}
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -R $TESTCASE_ROOT/_build/default/dir basic
   $ dune coq top --display short --toplevel echo dir/bar.v
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -R $TESTCASE_ROOT/_build/default/dir basic
@@ -30,7 +30,7 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   Entering directory '..'
         coqdep dir/bar.v.d
         coqdep dir/foo.v.d
-          coqc dir/.foo.aux,dir/foo.{glob,vo}
+          coqc dir/foo.{glob,vo}
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -R $TESTCASE_ROOT/_build/default/dir basic
   $ (cd dir && dune coq top --root .. --display short --toplevel echo dir/bar.v)
   Entering directory '..'

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.aux,theories/a.{glob,vo}
+          coqc theories/a.{glob,vo}
diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/run.t b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t
@@ -2,9 +2,9 @@
         coqdep bar/bar.v.d
         coqdep foo/foo.v.d
         coqdep foo/a/a.v.d
-          coqc foo/.foo.aux,foo/Nfoo_foo.{cmi,cmxs},foo/foo.{glob,vo}
-          coqc foo/a/.a.aux,foo/a/Nfoo_a_a.{cmi,cmxs},foo/a/a.{glob,vo}
-          coqc bar/.bar.aux,bar/Nbar_baz_bar.{cmi,cmxs},bar/bar.{glob,vo}
+          coqc foo/Nfoo_foo.{cmi,cmxs},foo/foo.{glob,vo}
+          coqc foo/a/Nfoo_a_a.{cmi,cmxs},foo/a/a.{glob,vo}
+          coqc bar/Nbar_baz_bar.{cmi,cmxs},bar/bar.{glob,vo}
 
   $ dune build --profile=release --debug-dependency-path @default
   lib: [

diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/run.t b/test/blackbox-tests/test-cases/coq/native-single.t/run.t
@@ -1,8 +1,8 @@
   $ dune build --profile=release --display short --debug-dependency-path @all
         coqdep bar.v.d
         coqdep foo.v.d
-          coqc .foo.aux,Nbasic_foo.{cmi,cmxs},foo.{glob,vo}
-          coqc .bar.aux,Nbasic_bar.{cmi,cmxs},bar.{glob,vo}
+          coqc Nbasic_foo.{cmi,cmxs},foo.{glob,vo}
+          coqc Nbasic_bar.{cmi,cmxs},bar.{glob,vo}
 
   $ dune build --profile=release --debug-dependency-path @default
   lib: [

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.aux,b/foo.{glob,vo}
-          coqc c/d/.bar.aux,c/d/bar.{glob,vo}
-          coqc c/.ooo.aux,c/ooo.{glob,vo}
-          coqc a/.bar.aux,a/bar.{glob,vo}
+          coqc b/foo.{glob,vo}
+          coqc c/d/bar.{glob,vo}
+          coqc c/ooo.{glob,vo}
+          coqc a/bar.{glob,vo}
 
   $ dune build --debug-dependency-path @default
   lib: [