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

Changelog entry for the change of dune cache default (#10710) #10913

Closed
wants to merge 4 commits into from

Conversation

ElectreAAS
Copy link
Collaborator

No description provided.

doc/changes/10710.md Outdated Show resolved Hide resolved
@ejgallego
Copy link
Collaborator

A couple of comments:

  • should doc be updated in this PR, or in a separate one?
  • IMHO the most important bit is to explain how uses can re-enable old behavior, I am aware of users in the wild relying heavily on cache + safe user-side rules. I guess they all need to do is to update the ./config/dune as to enable the cache for the user rules, right?

@ejgallego
Copy link
Collaborator

Thanks for the update @ElectreAAS !

I have a last question, is it possible with the new code to recover the old behavior when the user had used (cache enabled) in the config file, without using any env variables?

Comment on lines +35 to +38
Not all rules are cached by default: user-created ``(rule _)`` actions are not to prevent mistakes.
You can enable the caching of these rules by setting the environment variable ``DUNE_CACHE_RULES`` to ``enabled``.

Copy link
Contributor

Choose a reason for hiding this comment

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

to be clear, this is about caching the output of such rules right? Not the rules themselves

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I don't really know what caching a rule without caching its result would even mean. So yes I believe this is about caching outputs.

doc/caching.rst Outdated Show resolved Hide resolved
@Leonidas-from-XIV
Copy link
Collaborator

I have a last question, is it possible with the new code to recover the old behavior when the user had used (cache enabled) in the config file, without using any env variables?

No, not with the current code, you need to explicitly opt-in to caching the user rules.

@rgrinberg
Copy link
Member

is it possible with the new code to recover the old behavior when the user had used (cache enabled) in the config file, without using any env variables?

As Marek mentioned, it's not possible at the moment. If you'd like to add a config option for this in addition to the env var, you are welcome to.

@ejgallego
Copy link
Collaborator

As Marek mentioned, it's not possible at the moment. If you'd like to add a config option for this in addition to the env var, you are welcome to.

Thanks folks for the confirmation.

I think indeed an option to enable this in ./config/dune should be added, otherwise quite a few users I know (virtually all Coq devs + many users) will regress as they have a setup where they enable the cache in the config file (their rules are safe), however it is far from trivial for them to switch to using environment variables.

I guess that would be a regression, but likely this setup did fall under the "experimental" category, right?

Signed-off-by: Ambre Austen Suhamy <[email protected]>
Signed-off-by: Ambre Austen Suhamy <[email protected]>
Signed-off-by: Ambre Austen Suhamy <[email protected]>
Copy link
Collaborator

@Leonidas-from-XIV Leonidas-from-XIV left a comment

Choose a reason for hiding this comment

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

I am aware of the discussion happening in #10710 but I think this PR accurately describes the current state of main. If any changes will be done that will happen in a separate PR so I think merging this one in the meantime is sensible.

Signed-off-by: Christine Rose <[email protected]>
@nojb
Copy link
Collaborator

nojb commented Sep 21, 2024

I am aware of the discussion happening in #10710 but I think this PR accurately describes the current state of main. If any changes will be done that will happen in a separate PR so I think merging this one in the meantime is sensible.

The discussion in #10710 is converging, so you may want to hold off before merging this one. See #10944.

@ElectreAAS
Copy link
Collaborator Author

#10944 has been merged, and it includes a correct changelog.
Closing this one.

@ElectreAAS ElectreAAS closed this Sep 23, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants