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

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Jul 30, 2022

We stop declaring .aux files as targets in the coqc rules. .aux files are simply a "cache" recording a runtime estimation for the STM (the thing that let's Coq process proofs asynchronously) to schedule proofs. It definitely should not be cached (or really known) by Dune.

Fixes #6004

@Alizter Alizter force-pushed the ps/rr/remove__aux_targets_from_coqc_rule branch 2 times, most recently from d7f8a4a to bafb533 Compare July 30, 2022 22:33
@ejgallego
Copy link
Collaborator

Note this would re-open #3437

@Alizter
Copy link
Collaborator Author

Alizter commented Jul 31, 2022

@ejgallego I am unable to reproduce that issue on my machine. Do you have a test demonstrating the behaviour that this PR will introduce. Otherwise, it doesn't seem like something important.

@Alizter Alizter added the coq label Jul 31, 2022
@emillon
Copy link
Collaborator

emillon commented Aug 1, 2022

Just chiming in, but in #3437 you mentioned a possible new flag that could disable the production of aux files @ejgallego. Does this exist? is this useful for dune or are these files used elsewhere?

@Alizter
Copy link
Collaborator Author

Alizter commented Aug 1, 2022

@emillon It was never implemented in Coq AFAIK. .aux files are not used by dune anywhere. The only users are IDEs for Coq and even then it is just a suggestion on how to split concurrent work, rather than some deterministic output.

There are lots of mentions of .aux files being replaced by a better system scattered around, however it will probably just end up with their removal.

@Alizter Alizter force-pushed the ps/rr/remove__aux_targets_from_coqc_rule branch from bafb533 to 008ee3f Compare August 1, 2022 10:11
@ejgallego
Copy link
Collaborator

@Alizter does the test repository in the issue above reproduce the issue?

This may not seem important, but could impact a lot of users if we get this wrong and .aux files are not properly cleaned anymore.

@Alizter
Copy link
Collaborator Author

Alizter commented Aug 6, 2022

@ejgallego I am unable to reproduce the issue in the repository with this patch.

@Alizter Alizter force-pushed the ps/rr/remove__aux_targets_from_coqc_rule branch from 008ee3f to b504e9e Compare August 6, 2022 16:31
@ejgallego
Copy link
Collaborator

Ok, thanks for checking. Somehow this scares me, as testing this stuff is tricky, but if you think it is worth trying we can do, hope we don't break most users.

The PR needs a changelog entry tho (please add what PR reverts and the bug fixed)

@Alizter Alizter force-pushed the ps/rr/remove__aux_targets_from_coqc_rule branch from b504e9e to 83252ff Compare August 7, 2022 19:12
@Alizter Alizter force-pushed the ps/rr/remove__aux_targets_from_coqc_rule branch from 83252ff to f5892b0 Compare September 6, 2022 19:50
@Alizter Alizter requested a review from rgrinberg September 6, 2022 19:54
@rgrinberg rgrinberg requested a review from ejgallego September 6, 2022 23:26
@Alizter
Copy link
Collaborator Author

Alizter commented Sep 6, 2022

Depends on #6130

ps-id: 2b8b57f9-f39d-4162-a2aa-31505e430304
Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter Alizter force-pushed the ps/rr/remove__aux_targets_from_coqc_rule branch from f5892b0 to 44c456e Compare September 7, 2022 16:47
Copy link
Collaborator

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, but I'd be nice if @rgrinberg could have a looks as he introduced these as targets in the first place.

@rgrinberg rgrinberg added this to the 3.5.0 milestone Sep 9, 2022
@rgrinberg rgrinberg merged commit 2949a99 into ocaml:main Sep 9, 2022
@Blaisorblade
Copy link
Contributor

@Alizter AFAICT https://github.com/Mbodin/dune-bug was not a sufficient reproduction, but adding .common.aux next to common.v was needed.

@ejgallego
Copy link
Collaborator

@Alizter AFAICT https://github.com/Mbodin/dune-bug was not a sufficient reproduction, but adding .common.aux next to common.v was needed.

Thanks for the pointer, it seems to work fine here. I'm unsure how that issue happened in the first place.

@Alizter Alizter deleted the ps/rr/remove__aux_targets_from_coqc_rule branch September 9, 2022 15:58
emillon added a commit to emillon/opam-repository that referenced this pull request Oct 11, 2022
…ne-site, dune-rpc, dune-rpc-lwt, dune-private-libs, dune-glob, dune-configurator, dune-build-info, dune-action-plugin and chrome-trace (3.5.0~alpha1)

CHANGES:

- Sandbox running cinaps actions starting from cinaps 1.1 (ocaml/dune#6176, @rgrinberg)

- Add a `runtime_deps` field in the `cinaps` stanza to specify runtime
  dependencies for running the cinaps preprocessing action (ocaml/dune#6175, @rgrinberg)

- Shadow alias module `Foo__` when building a library `Foo` (ocaml/dune#6126, @rgrinberg)

- Extend dune describe to include the root path of the workspace and the
  relative path to the build directory. (ocaml/dune#6136, @reubenrowe)

- Allow dune describe workspace to accept directories as arguments.
  The provided directories restrict the worskpace description to those
  directories. (ocaml/dune#6107, fixes ocaml/dune#3893, @esope)

- Add a terminal persistence mode that attempts to clear the terminal history.
  It is enabled by setting terminal persistence to
  `clear-on-rebuild-and-flush-history` (ocaml/dune#6065, @rgrinberg)

- Disallow generating targets in sub direcories in inferred rules. The check to
  forbid this was accidentally done only for manually specified targets (ocaml/dune#6031,
  @rgrinberg)

- Do not ignore rules marked `(promote (until-clean))` when
  `--ignore-promoted-rules` (or `-p`) is passed. (ocaml/dune#6010, fixes ocaml/dune#4401, @emillon)

- Dune no longer considers .aux files as targets during Coq compilation. This
  means that .aux files are no longer cached. (ocaml/dune#6024, fixes ocaml/dune#6004, @Alizter)

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

- Allow rules producing directory targets to be not sandboxed (ocaml/dune#6056,
  @rgrinberg)

- Introduce a `dirs` field in the `install` stanza to install entire
  directories (ocaml/dune#5097, fixes ocaml/dune#5059, @rgrinberg)

- Menhir rules are now sandboxed by default (ocaml/dune#6076, @rgrinberg)

- Allow rules producing directory targets to create symlinks (ocaml/dune#6077, fixes
  ocaml/dune#5945, @rgrinberg)

- Inline tests are now sandboxed by default (ocaml/dune#6079, @rgrinberg)

- Fix build-info version when used with flambda (ocaml/dune#6089, fixes ocaml/dune#6075, @jberdine)

- Add an `(include <file>)` term to the `include_dirs` field for adding
  directories to the include paths sourced from a file. (ocaml/dune#6058, fixes ocaml/dune#3993,
  @gridbugs)

- Support `(extra_objects ...)` field in `(executable ...)` and `(library
  ...)` stanzas (ocaml/dune#6084, fixes ocaml/dune#4129, @gridbugs)

- Fix compilation of Dune under esy on Windows (ocaml/dune#6109, fixes ocaml/dune#6098, @nojb)

- Improve error message when parsing several licenses in `(license)` (ocaml/dune#6114,
  fixes ocaml/dune#6103, @emillon)

- odoc rules now about `ODOC_SYNTAX` and will rerun accordingly (ocaml/dune#6010, fixes
  ocaml/dune#1117, @emillon)

- dune install: copy files in an atomic way (ocaml/dune#6150, @emillon)

- Add `%{coq:...}` macro for accessing data about the configuration about Coq.
  For instance `%{coq:version}` (ocaml/dune#6049, @Alizter)

- update vendored copy of cmdliner to 1.1.1. This improves the built-in
  documentation for command groups such as `dune ocaml`. (ocaml/dune#6038, @emillon,
  ocaml/dune#6169, @shonfeder)

- The test suite for Coq now requires Coq >= 8.16 due to changes in the
  plugin loading mechanism upstream (which now uses findlib).

- Starting with Coq build language 0.6, theories can be built without importing
  Coq's standard library by including `(stdlib no)`.
  (ocaml/dune#6165 ocaml/dune#6164, fixes ocaml/dune#6163, @ejgallego @Alizter @LasseBlaauwbroek)

- on macOS, sign executables produced by artifact substitution (ocaml/dune#6137, fixes
  ocaml/dune#5650, @emillon)

- Added an (aliases ...) field to the (rules ...) stanza which allows the
  specification of multiple aliases per rule (ocaml/dune#6194, @Alizter)
emillon added a commit to emillon/opam-repository that referenced this pull request Oct 19, 2022
…ne-site, dune-rpc, dune-rpc-lwt, dune-private-libs, dune-glob, dune-configurator, dune-build-info, dune-action-plugin and chrome-trace (3.5.0)

CHANGES:

- macOS: Handle unknown fsevents without crashing (ocaml/dune#6217, @rgrinberg)

- Enable file watching on MacOS SDK < 10.13. (ocaml/dune#6218, @rgrinberg)

- Sandbox running cinaps actions starting from cinaps 1.1 (ocaml/dune#6176, @rgrinberg)

- Add a `runtime_deps` field in the `cinaps` stanza to specify runtime
  dependencies for running the cinaps preprocessing action (ocaml/dune#6175, @rgrinberg)

- Shadow alias module `Foo__` when building a library `Foo` (ocaml/dune#6126, @rgrinberg)

- Extend dune describe to include the root path of the workspace and the
  relative path to the build directory. (ocaml/dune#6136, @reubenrowe)

- Allow dune describe workspace to accept directories as arguments.
  The provided directories restrict the worskpace description to those
  directories. (ocaml/dune#6107, fixes ocaml/dune#3893, @esope)

- Add a terminal persistence mode that attempts to clear the terminal history.
  It is enabled by setting terminal persistence to
  `clear-on-rebuild-and-flush-history` (ocaml/dune#6065, @rgrinberg)

- Disallow generating targets in sub direcories in inferred rules. The check to
  forbid this was accidentally done only for manually specified targets (ocaml/dune#6031,
  @rgrinberg)

- Do not ignore rules marked `(promote (until-clean))` when
  `--ignore-promoted-rules` (or `-p`) is passed. (ocaml/dune#6010, fixes ocaml/dune#4401, @emillon)

- Dune no longer considers .aux files as targets during Coq compilation. This
  means that .aux files are no longer cached. (ocaml/dune#6024, fixes ocaml/dune#6004, @Alizter)

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

- Allow rules producing directory targets to be not sandboxed (ocaml/dune#6056,
  @rgrinberg)

- Introduce a `dirs` field in the `install` stanza to install entire
  directories (ocaml/dune#5097, fixes ocaml/dune#5059, @rgrinberg)

- Menhir rules are now sandboxed by default (ocaml/dune#6076, @rgrinberg)

- Allow rules producing directory targets to create symlinks (ocaml/dune#6077, fixes
  ocaml/dune#5945, @rgrinberg)

- Inline tests are now sandboxed by default (ocaml/dune#6079, @rgrinberg)

- Fix build-info version when used with flambda (ocaml/dune#6089, fixes ocaml/dune#6075, @jberdine)

- Add an `(include <file>)` term to the `include_dirs` field for adding
  directories to the include paths sourced from a file. (ocaml/dune#6058, fixes ocaml/dune#3993,
  @gridbugs)

- Support `(extra_objects ...)` field in `(executable ...)` and `(library
  ...)` stanzas (ocaml/dune#6084, fixes ocaml/dune#4129, @gridbugs)

- Fix compilation of Dune under esy on Windows (ocaml/dune#6109, fixes ocaml/dune#6098, @nojb)

- Improve error message when parsing several licenses in `(license)` (ocaml/dune#6114,
  fixes ocaml/dune#6103, @emillon)

- odoc rules now about `ODOC_SYNTAX` and will rerun accordingly (ocaml/dune#6010, fixes
  ocaml/dune#1117, @emillon)

- dune install: copy files in an atomic way (ocaml/dune#6150, @emillon)

- Add `%{coq:...}` macro for accessing data about the configuration about Coq.
  For instance `%{coq:version}` (ocaml/dune#6049, @Alizter)

- update vendored copy of cmdliner to 1.1.1. This improves the built-in
  documentation for command groups such as `dune ocaml`. (ocaml/dune#6038, @emillon,
  ocaml/dune#6169, @shonfeder)

- The test suite for Coq now requires Coq >= 8.16 due to changes in the
  plugin loading mechanism upstream (which now uses `Findlib`).

- Starting with Coq build language 0.6, theories can be built without importing
  Coq's standard library by including `(stdlib no)`.
  (ocaml/dune#6165 ocaml/dune#6164, fixes ocaml/dune#6163, @ejgallego @Alizter @LasseBlaauwbroek)

- on macOS, sign executables produced by artifact substitution (ocaml/dune#6137, ocaml/dune#6231,
  fixes ocaml/dune#5650, fixes ocaml/dune#6226, @emillon)

- Added an (aliases ...) field to the (rules ...) stanza which allows the
  specification of multiple aliases per rule (ocaml/dune#6194, @Alizter)

- The `(coq.theory ...)` stanza will now ensure that for each declared `(plugin
 ...)`, the `META` file for it is built before calling `coqdep`. This enables
 the use of the new `Findlib`-based loading method in Coq 8.16; however as of
 Coq 8.16.0, Coq itself has some bugs preventing this to work yet. (ocaml/dune#6167 ,
 workarounds ocaml/dune#5767, @ejgallego)

- Allow include statement in install stanza (ocaml/dune#6139, fixes ocaml/dune#256, @gridbugs)

- Handle CSI n K code in ANSI escape codes from commands. (ocaml/dune#6214, fixes ocaml/dune#5528,
  @emillon)

- Add a new experimental feature `mode_specific_stubs` that allows the
  specification of different flags and sources for foreign stubs depending on
  the build mode (ocaml/dune#5649, @voodoos)
SkySkimmer added a commit to SkySkimmer/coq that referenced this pull request Oct 21, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
Archived in project
Development

Successfully merging this pull request may close these issues.

--cache-check-probability gives "false" positives on Coq builds
5 participants