Using nightly mathlib as a dependency

Stream: mathlib4

[Leo Stefanesco]

We are using nightly versions of mathlib as a dependency, but a recent change to the cache program broke this use case (cf this issue)

What is the best way forward for this use case?

cc @Kim Morrison

[Leo Stefanesco]

I was thinking that one possibility would be to put the new behavior behind an environment variable, since it's only going to be used by advanced users.

What do you think @Kim Morrison?

[Leo Stefanesco]

Ping @Kim Morrison

[Jovan Gerbscheid]

By the way, I have also found that I cannot get cache from adaptation branches in mathlib4-nightly-testing, which is kind of annoying. And !bench also doesn't work there.

[Leo Stefanesco]

I opened this PR which hopefully fixes my issue by only enabling the new behavior when ran from the mathlib repo itself.

[Leo Stefanesco]

I don't know if it also fixes @Jovan Gerbscheid's issue

[Kim Morrison]

Sorry about the very slow response here. I've started another discussion about this issue at #ecosystem infrastructure > `cache get` fails when depending on Mathlib nightly-testing , and proposed a different fix in #30571.