Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

remove .aux targets from coqc rule #6024

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,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)

- Cinaps actions are now sandboxed by default (#6062, @rgrinberg)

- Allow rules producing directory targets to be not sandboxed (#6056,
Expand Down
2 changes: 1 addition & 1 deletion src/dune_rules/coq_module.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down
4 changes: 2 additions & 2 deletions test/blackbox-tests/test-cases/coq/base-unsound.t/run.t
Original file line number Diff line number Diff line change
@@ -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}
4 changes: 2 additions & 2 deletions test/blackbox-tests/test-cases/coq/base.t/run.t
Original file line number Diff line number Diff line change
@@ -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: [
Expand Down
2 changes: 1 addition & 1 deletion test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
4 changes: 2 additions & 2 deletions test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand All @@ -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]
Expand All @@ -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]
Original file line number Diff line number Diff line change
Expand Up @@ -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]
2 changes: 1 addition & 1 deletion test/blackbox-tests/test-cases/coq/compose-self.t/run.t
Original file line number Diff line number Diff line change
Expand Up @@ -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]
8 changes: 4 additions & 4 deletions test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t
Original file line number Diff line number Diff line change
Expand Up @@ -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}
4 changes: 2 additions & 2 deletions test/blackbox-tests/test-cases/coq/coqtop-recomp.t
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 '..'
Expand Down
2 changes: 1 addition & 1 deletion test/blackbox-tests/test-cases/coq/ml-lib.t/run.t
Original file line number Diff line number Diff line change
Expand Up @@ -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}
6 changes: 3 additions & 3 deletions test/blackbox-tests/test-cases/coq/native-compose.t/run.t
Original file line number Diff line number Diff line change
Expand Up @@ -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: [
Expand Down
4 changes: 2 additions & 2 deletions test/blackbox-tests/test-cases/coq/native-single.t/run.t
Original file line number Diff line number Diff line change
@@ -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: [
Expand Down
8 changes: 4 additions & 4 deletions test/blackbox-tests/test-cases/coq/rec-module.t/run.t
Original file line number Diff line number Diff line change
Expand Up @@ -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: [
Expand Down