Using nighly mathlib as dependency fails

[ineol]

We have a dependency on nightly mathlib, and since, this commit, getting the cache fails as it is looking for a certain git remote in the checkout of mathlib in .lake/packages/mathlib.

The error when running lake exe cache get is:

Current branch: HEAD
uncaught exception: Failed to run Git to determine Mathlib's repository from nightly-testing remote (exit code: 2).
Branch 'HEAD' should use the nightly-testing remote, but it's not configured.
Please add the nightly-testing remote pointing to the nightly testing repository:
git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
Stdout:

Stderr:
error: No such remote 'nightly-testing'

Should we use another way of depending on mathlib or is it an issue in cache?

cc @kim-em

[kim-em]

Yes, this is a problem! We weren't thinking about the implications for downstream cache users. Can you start a thread on the zulip about this?

[ineol]

sure!

[kim-em]

I've proposed a different fix at #30571.