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

feature: clear dune cache #8971

Closed
emillon opened this issue Oct 19, 2023 · 9 comments · Fixed by #8975
Closed

feature: clear dune cache #8971

emillon opened this issue Oct 19, 2023 · 9 comments · Fixed by #8975
Labels
feature-request User wanted features

Comments

@emillon
Copy link
Collaborator

emillon commented Oct 19, 2023

It is pretty common to use dune cache trim to completely remove the cache. The right invocation is dune cache trim --size 0B but it requires finding about --size vs --trimmed-size, adding a B suffix, etc.

I suggest adding a dedicated way to do that. Either dune cache trim --all, or dune cache clear, to be determined.

@emillon emillon added the feature-request User wanted features label Oct 19, 2023
@nojb
Copy link
Collaborator

nojb commented Oct 19, 2023

+1 for dune cache clear.

Another cache-related "missing" feature: some way to print the cache location (maybe as part of dune --verbose output)

@Alizter
Copy link
Collaborator

Alizter commented Oct 19, 2023

I've had this idea to have a configurable default size for trim for some time now. The idea is that you put some config value in your dune config that gives a default value for size. That way you just have to write dune cache trim on its own with no arguments necessary. This would presumably subsume dune cache clear.

@nojb
Copy link
Collaborator

nojb commented Oct 19, 2023

This would presumably subsume dune cache clear.

Not really. dune cache trim without an argument would be used to trim the cache (to your configured size). But sometimes you want to get rid of the cache, not trim it, which is when you would use dune cache clear.

@Alizter
Copy link
Collaborator

Alizter commented Oct 19, 2023

Right, I was thinking configuring the size to be 0. In which situations would you want to clear the cache rather than trim it?

@nojb
Copy link
Collaborator

nojb commented Oct 19, 2023

Right, I was thinking configuring the size to be 0.

I know, but my sense is that the two operations are independently useful.

In which situations would you want to clear the cache rather than trim it?

Liberating disk space punctually, debugging purposes, ...

@Alizter
Copy link
Collaborator

Alizter commented Oct 19, 2023

I suppose one way dune cache clear would be distinct from dune cache trim is in speed. Trim takes its time calculating sizes, but if you just want to remove all the cache then dune cache clear doesn't need to concern itself with these calculations.

@nojb
Copy link
Collaborator

nojb commented Oct 19, 2023

dune cache clear doesn't need to concern itself with these calculations.

Good point.

@nojb
Copy link
Collaborator

nojb commented Oct 20, 2023

I took a quick stab at this: #8975

@nojb
Copy link
Collaborator

nojb commented Oct 20, 2023

Another cache-related "missing" feature: some way to print the cache location (maybe as part of dune --verbose output)

And also this: #8974

@nojb nojb closed this as completed in #8975 Jan 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature-request User wanted features
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants