[Merged by Bors] - feat: caching build files on Azure

[arthurpaulino]

This PR implements caching for Mathlib build files. The basic API is:

• lake exe cache get to download missing build files
• lake exe cache put to upload files that are missing on the server
• lake exe cache to print the help menu

This caching method has a few enhancements on top of the solution we had for mathlib in Lean 3:

1. Source files are content-addressed and build files are referenced by such hashes separately
2. Minimized download traffic with queries that only pull files that are missing locally
3. Minimized upload traffic with queries that only push files that are missing on the server

[gebner]

We should also upload some kind of manifest file for every upload, containing at least the list of referenced cache files and the git revision of mathlib4, so that we can do garbage collection.

[arthurpaulino]

We should also upload some kind of manifest file for every upload, containing at least the list of referenced cache files and the git revision of mathlib4, so that we can do garbage collection.

Can we do garbage collection by detecting files that were created a long time ago? I believe anything older than 7 days can be discarded safely (it's easy to replace it anyways)

[gebner]

There's still a couple TODOs here, but I think it's best to merge this now and iterate later.

Please add copyright headers (just copy&paste from the Mathlib files).

bors d+

[bors]

✌️ arthurpaulino can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[arthurpaulino]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style