[Merged by Bors] - chore(Cache): Add support for $MATHLIB_CACHE_DIR#21480
[Merged by Bors] - chore(Cache): Add support for $MATHLIB_CACHE_DIR#21480
Conversation
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.
2016bb3 to
c89a963
Compare
PR summary c89a9635c1Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo 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 No changes to technical debt.You can run this locally as
|
|
What happens if, by mistake, |
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. |
|
I had no idea that there even was a notion of an |
|
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. |
|
bors merge |
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.
|
Pull request successfully merged into master. Build succeeded: |
* origin/master: chore: update Mathlib dependencies 2025-02-06 (#21523) fix(MathlibTest/TransImports): stop inspecting the `Lean` package (#21492) style(Mathlib/Computability/Halting): `RePred` to `REPred` (#21216) feat(Data/Set/Card): add `ncard_le_encard` (#21467) feat(Order): lemmas for `Order.succ` and `Order.pred` in `Fin` (#21437) feat(LinearAlgebra/LinearIndependent): linear independence + subsingletons (#21511) feat: for continuous linear maps in a normed ring, `flip mul = mul` (#21507) chore(GroupTheory/Commutator): don't import `Ring` (#21296) chore(Data/Complex/Abs): add `protected` to results that already exists in root namespace (#21454) chore(*): `erw`s that can now become `rw`s (#21510) chore: allow create-adaptation-pr.sh to continue when bump branch already exists (#21486) feat(CategoryTheory): equivalence between `Ind C` and left exact functors from `C` to `Type` (#21430) chore: add test to TCSynth.lean (#21499) feat: the category of ind-objects satisfies the AB5 axiom (#21350) refactor(RepresentationTheory): `ConcreteCategory` instances for `Rep` (#21465) chore: split Mathlib.Order.Filter.Basic (#21403) chore: update Mathlib dependencies 2025-02-06 (#21487) chore(Cache): Add support for $MATHLIB_CACHE_DIR (#21480) feat(CategoryTheory): a closed monoidal category is an ordinary enriched category over itself (#21436) feat(AlgebraicTopology): notation X ^[n] for cosimplicial objects (#21485) chore: upgrade dependencies manually (#21484) refactor(Analysis/Normed): `ConcreteCategory` refactor for `SemiNormedGrp` (#21477) refactor(LinearAlgebra): `ConcreteCategory` instance for `QuadraticModuleCat` (#21471) refactor(MeasureTheory): `ConcreteCategory` instance for `MeasCat` (#21468) refactor(Topology/Category): clean up remaining uses of `HasForget` (#21458) refactor(CategoryTheory): `ConcreteCategory` instances for pointed types (#21470) feat(CategoryTheory/Action): `ConcreteCategory` instances for `Action` (#21462) feat(CategoryTheory): `ConcreteCategory` instance for `DifferentialObject` (#21464) feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and `mk` (#18178) chore: rename `encard_le_card` to `encard_le_encard` (#21426) feat: add theorem about the norm of cross products (#20920) feat(Data/Matroid/Circuit): circuit elimination and finitary matroids (#21172) feat(LinearAlgebra/ExteriorPower): add iMulti_family definition for product of a family of vectors (#21397)
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.
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.