cache warning

Stream: mathlib4

[Shreyas Srinivas]

I was upgrading my graph matchings library to v4.22.0-rc3 today. It uses mathlib as a dependency. When running lake update I got the warning:

Current branch: HEAD
Warning: Some Mathlib ecosystem tools assume that the git remote for leanprover-community/mathlib4 is named upstream. You have named it origin instead. We recommend changing the name to upstream. Moreover, origin should point to your own fork of the mathlib4 repository. You can set this up with git remote add upstream https://github.com/leanprover-community/mathlib4.git.

[Shreyas Srinivas]

This warning makes no sense for downstream projects.

[Shreyas Srinivas]

which tools care about the remote name specifically? Obviously lake git clones mathliib and the default remote name is origin so that's the source of the warning

[Kevin Buzzard]

See #mathlib4 > "You have named it `origin` instead." @ 💬 . I think that this is low prio at the minute; it's only a warning, and there are still being PRs made to try and ensure that everyone has cache working etc.

[Kevin Buzzard]

Maybe the best thing to do is to open an issue against mathlib?

[Shreyas Srinivas]

Thanks. I’ll do that.