Store LeanCopilot cache elsewhere

Stream: Machine Learning for Theorem Proving

[Jason Rute]

LeanCopilot stores a lot of stuff in ~/.cache/lean_copilot. Is there a way I can change the that location? I'm working in a system where the home directory is tiny. Is this location hard coded in LeanCopilot, hard coded in Lean, or is it configurable? @Kaiyu Yang

[Kaiyu Yang]

It should be configurable via the LEAN_COPILOT_CACHE_DIR environment variable (details in https://github.com/lean-dojo/LeanCopilot/blob/4bc4e6c09689472e5523b0acc724c666baf51e6e/ModelCheckpointManager/Download.lean#L26). I've never tested this functionality. Please let me know if you encounter any issues.

A simpler solution could be just to create a symbolic link at ~/.cache/lean_copilot that points to somewhere else.

[Jason Rute]

A simpler solution could be just to create a symbolic link at ~/.cache/lean_copilot that points to somewhere else.

That is what I've been doing. I'll let you know if I try out the env variable.

[Jason Rute]

Thanks!

[Kaiyu Yang]

You may need to modify the environment variable in both bash and VSCode (settings of Lean 4 extension).