Quiet Archive, Counterexamples, upload cache

Stream: mathlib4

[Damiano Testa]

I just opened #11377, which introduces two changes to CI:

• it checks that Archive and Counterexamples are quiet;
• it uploads the cache even when Mathlib is noisy.

Of course, I think that both are improvements, but I am happy to take comments! :smile:

[Damiano Testa]

I am also running a side PR to make sure that the noisiness of Mathlib is indeed guaranteed: #11378.

[Damiano Testa]

Floris pointed out that the cache is uploaded already, before the change. The check of noisiness does not happen with the current CI, though and does happen with the proposed change.

[Kim Morrison]

A bigger change to CI that would be great would be too parallelize as much as possible after the build job. This would require turning steps into jobs, and generally making the CI file more complicated.

[Kim Morrison]

Artifacts are not automatically shared between jobs.

[Kim Morrison]

We could either do a lot of cache get, or use existing GitHub tools to move files between jobs. I don't think there is an example of this in Mathlib CI yet, although Lean CI does this I think.

[Damiano Testa]

Running the lean4checker requires nothing of the sort, right? It could start running as soon as you know that mathlib built, while Archive and Counterexamples still use the Mathlib cache, no?

[Damiano Testa]

I am saying this, since that is the single slowest step after building mathlib and does not actually seem to use any artifacts, other than the knowledge that it has a chance of succeeding, since Lean already verified mathlib.

[Damiano Testa]

Ok, I did not realize that lean4checker verifies the correctness of the oleans, so sharing is required.

[Kim Morrison]

Given the expected failure profile of lean4checker, it would be completely okay to turn this into a job that runs only daily or weekly on master, as long as it reports failures very obviously. (e.g. zulip bot message)

[Damiano Testa]

Maybe it could be a test that is only run by bors when merging into master, but that does not run on PRs.