chore(Cache): Add support for $MATHLIB_CACHE_DIR

[Julian]

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.

---

[github-actions]

PR summary c89a9635c1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[adomani]

What happens if, by mistake, XDG_CACHE_HOME and MATHLIB_CACHE_DIR are set to the same value? Should this be noticed and possibly "remedied"? E.g., the fall-back happens if the variable is unset or set to the same value as XDG_CACHE_HOME? It seems like it would be a little more lenient!

[Julian]

What happens if, by mistake, XDG_CACHE_HOME and MATHLIB_CACHE_DIR are set to the same value? Should this be noticed and possibly "remedied"? E.g., the fall-back happens if the variable is unset or set to the same value as XDG_CACHE_HOME? It seems like it would be a little more lenient!

My immediate reaction is that while I think it is very common for programs to have both a program-specific envvar and also to then fallback to XDG (see my giant list here of just programs I use...), I don't know of any which have that which perform the check you mention. I'm not saying it's not possible someone doing it is making a mistake, but I guess it feels weird to check for to me for reasons I can't quite articulate -- usually for this sort of thing I think you "trust" that someone setting an envvar has double checked and really means to do what they're trying to do (and so it'd be odd to prevent them from doing it in the program if in theory it's possible they mean what they say).

I'm happy to add it though if you'd like, I don't think anyone really will ever be negatively affected by it in practice.

[adomani]

I had no idea that there even was a notion of an XDG variable! I'm happy to follow the standard practice. Besides, I will certainly not be setting these variables on my computer, so for me it is fall-back anyway!

[Julian]

Yeah, XDG is a (Linux) specification for directory hierarchies which lives here: https://specifications.freedesktop.org/basedir-spec/latest/ and which is followed by lots of programs on your computer.