Another Mathlib cache download problem

Stream: new members

[Noam Kantor]

Hi there, I am attempting to use Lean in VSCode on my Mac, which was going fine for a few days but then I started getting errors in my import lines related to Mathlib. Now, when I try to run lake exe cache get, I get a 15% success rate and a warning that "Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later."

I have tried the instructions here but didn't get anywhere with it. I'm happy to just uninstall the entire package and reinstall, or try anything else that might help.

[Alex J. Best]

The cache is unfortunately currently broken for everyone, see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20cache.20doesn't.20work/near/410776665

[Noam Kantor]

That makes me feel better, at least. Thanks Alex - by the way, this is Noam Kantor! Great to see you virtually!