RFC: GUI button to download cache for a specific file

[YaelDillies]

Proposal

Oftentimes I want to work on a rather low-level file X. lake exe cache get would download me way too many files and take too long, but typing lake exe cache get Mathlib/X.lean (where X is a long file path) is also quite unergonomic.

I suggest we add a pretty visible button on the file window to download cache for the file currently in focus.

Community Feedback

Zulip

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[arthurpaulino]

If there's a file in focus that doesn't have its current olean up to date, I assume there will be work happening in the background. Won't the background job conflict with what the user tries to do when summoning cache? Or was this issue resolved?

[YaelDillies]

oleans now get rebuilt only if the user explicitly asks for it. Does this answer your question?

[arthurpaulino]

Yeap, thanks!

[YaelDillies]

🏓 This feature would save me 10-15min a day, so I really want it.