Commit 2023-01-03 21:54 01a2153b

feat: caching build files on Azure (#1230) 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