feat(ci): upload all branch builds to Azure server

[robertylewis]

The artifacts from every build (successful or not) of a leanprover-community/mathlib branch will get uploaded to the cloud. Forthcoming changes to cache-olean/update-mathlib will retrieve these.

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• 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]

See the result of a successful run here (21mb file).

[gebner]

Can/should we migrate the old mathlib-nightly releases to the new ☁️-scale deployment platform?

[robertylewis]

Can/should we migrate the old mathlib-nightly releases to the new -scale deployment platform?

We can/should. It will take a bit of scripting I guess. This will already push us into the paid tier (we get 5gb free). Maybe only the recent ones and noteworthy ones, like the last 3.4.2 release?

[robertylewis]

BTW, I have an unfinished, partially tested PR to mathlib-tools that points the scripts to these archives and falls back to mathlib-nightly.

[robertylewis]

I just counted -- we had ~40 push builds in the past 24 hours. So ~800mb a day. We'll hit the free limit in a week once this is merged. It says something about $170 in free credit though.

The Azure prices quote $0.018/gb/mo for storage. So if we keep everything, ~$2/mo, accumulating (first month $2, second $4, third $6, ...). Obviously this goes up as mathlib grows. I don't have any guess about the bandwidth usage.

It seems reasonable to store all master builds forever and branch builds for, say, a month. Distinguishing master/branch in the filename is inconvenient for fetching. Maybe we need a way to register the status of an archive with the server? This could also be used for branch builds that we want to keep forever, e.g. if an external project points to that commit.

[gebner]

Maybe we need a way to register the status of an archive with the server? This could also be used for branch builds that we want to keep forever, e.g. if an external project points to that commit.

I think we'll have a script that regularly runs and deletes "unwanted" builds. We can define the the meaning of "unwanted" in that script. I don't think we need to know this at upload time. For example, delete if none of the following is true:

• revision is part of current mathlib master
• revision is part of any branch/tag on mathlib
• file is at most 30 days old

[robertylewis]

Other thoughts:

• We should check for an existing archive of a build (1) at the beginning of CI and (2) before trying to push a new archive. (2) comes up if someone pushes the same commit to two branches around the same time. (1) comes up if someone does this but with enough time to finish the build in between.

  For (1) we can just call cache-olean and that stage of the build will be fast. We shouldn't cancel the build entirely, since the build stages can be different for different branches. For (2), the second build shouldn't fail.

• Eventually we should reconfigure/replace Mergify. It should build the actual merge commit that it will push to master. This puts us in situation (1) above. Archives will be available as soon as a PR hist master, instead of two hours later; master builds will only be docs, bundles, etc.

[PatrickMassot]

Let's merge this and see how it goes. Rob's concerns will be handled when we'll get the new scripts.