You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Firstly thank you @Kha for setting up Lean so it uses CCache, even with Nix. I'm currently cribbing some of it to try to speed up the CUDA work I'm doing.
They have CCACHE_BASEDIR instead of CCACHE_BASE_DIR. Looking at the docs, it looks like most of the environment variables are CCACHE_* where * doesn't have any underscores or hyphens. There are a few exceptions, but I don't know if there's a general rule.
Any ideas if this breaks caching, or if the docs are wrong?
The text was updated successfully, but these errors were encountered:
Firstly thank you @Kha for setting up Lean so it uses CCache, even with Nix. I'm currently cribbing some of it to try to speed up the CUDA work I'm doing.
In looking at
https://github.com/leanprover/lean4/blob/869d64e97ac5acf557c949c2af917db633999f8d/nix/packages.nix#L14C26-L14C26
I noticed that the environment variable being set isn't in the current docs:
https://ccache.dev/manual/4.8.2.html#_configuration_options
They have
CCACHE_BASEDIR
instead ofCCACHE_BASE_DIR
. Looking at the docs, it looks like most of the environment variables areCCACHE_*
where*
doesn't have any underscores or hyphens. There are a few exceptions, but I don't know if there's a general rule.Any ideas if this breaks caching, or if the docs are wrong?
The text was updated successfully, but these errors were encountered: