feat(scripts/cache-olean): --fetch queries a remote mathlib cache

[cipher1024]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[robertylewis]

I guess this migrates to https://github.com/leanprover-community/mathlib-tools now?

[cipher1024]

Does github have an option to migrate PRs?

[jcommelin]

I would be surprised, especially since the repo isn't a fork. But you can just write the patch to a file, and replay it on the new repo...

[cipher1024]

That was my plan B. The other repo was created by just copying the history of the scripts/ directory over to a new repo.

[robertylewis]

I don't think you can move the whole PR, but you can cherry-pick this one commit to mathlib-tools/master.

[robertylewis]

Moved to leanprover-community/mathlib-tools#2