Skip to content

Commit

Permalink
chore(Cache): Add support for $MATHLIB_CACHE_DIR
Browse files Browse the repository at this point in the history
This allows someone to explicitly put just Mathlib's own cache in some
specific location without needing to entirely affect any program using
XDG_CACHE_HOME.

When unset we fallback to the same logic as before.
  • Loading branch information
Julian committed Feb 5, 2025
1 parent 24c5975 commit c89a963
Showing 1 changed file with 13 additions and 10 deletions.
23 changes: 13 additions & 10 deletions Cache/IO.lean
Original file line number Diff line number Diff line change
Expand Up @@ -44,17 +44,20 @@ def IRDIR : FilePath :=

/-- Target directory for caching -/
initialize CACHEDIR : FilePath ← do
match ← IO.getEnv "XDG_CACHE_HOME" with
| some path => return path / "mathlib"
match ← IO.getEnv "MATHLIB_CACHE_DIR" with
| some path => return path
| none =>
let home ← if System.Platform.isWindows then
let drive ← IO.getEnv "HOMEDRIVE"
let path ← IO.getEnv "HOMEPATH"
pure <| return (← drive) ++ (← path)
else IO.getEnv "HOME"
match home with
| some path => return path / ".cache" / "mathlib"
| none => pure ⟨".cache"
match ← IO.getEnv "XDG_CACHE_HOME" with
| some path => return path / "mathlib"
| none =>
let home ← if System.Platform.isWindows then
let drive ← IO.getEnv "HOMEDRIVE"
let path ← IO.getEnv "HOMEPATH"
pure <| return (← drive) ++ (← path)
else IO.getEnv "HOME"
match home with
| some path => return path / ".cache" / "mathlib"
| none => pure ⟨".cache"

/-- Target file path for `curl` configurations -/
def CURLCFG :=
Expand Down

0 comments on commit c89a963

Please sign in to comment.