Skip to content

Commit 79b2042

Browse files
committed
chore: try 'XDG_CACHE_HOME' to download cache files (#1623)
Searches for a `XDG_CACHE_HOME` env variable. If it's defined, use `$XDG_CACHE_HOME/mathlib` as the repository of cache files. Fallback to `.cache`. Zulip thread fro context: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/lake.20get-cache/near/321773418
1 parent aa74e27 commit 79b2042

File tree

1 file changed

+6
-2
lines changed

1 file changed

+6
-2
lines changed

Cache/IO.lean

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,12 @@ def IRDIR : FilePath :=
3232
"build" / "ir"
3333

3434
/-- Target directory for caching -/
35-
def CACHEDIR : FilePath :=
36-
".cache"
35+
initialize CACHEDIR : FilePath ← do
36+
match ← IO.getEnv "XDG_CACHE_HOME" with
37+
| some path => return path / "mathlib"
38+
| none => match ← IO.getEnv "HOME" with
39+
| some path => return path / ".cache" / "mathlib"
40+
| none => pure ⟨".cache"
3741

3842
/-- Target file path for `curl` configurations -/
3943
def CURLCFG :=

0 commit comments

Comments
 (0)