Get cache for a specific file

Stream: general

[Yaël Dillies]

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 is also quite unergonomic. Would it be possible for the extension to provide a button (or a command in the forall menu) to download cache for the file currently in focus?

[Eric Rodriguez]

fzf is nice for situations like this

[Junyan Xu]

Getting the file path seems to be an easier problem than getting the module name (at least for me) because VSCode allows you to "Copy Relative Path"
image.png

[Kim Morrison]

Please open a feature request at https://github.com/leanprover/vscode-lean4.

[Yaël Dillies]

vscode-lean4#416