CI: continue on failure?

Stream: mathlib4

[Yury G. Kudryashov]

I just found out that Mathlib CI doesn't run "lint mathlib" and leanchecker if "check for unused imports" fails. IMHO, we should change this: failures in various tests should set the build status to failure but shouldn't cancel other tests.

[Damiano Testa]

#11377 is a recent PR that I opened to make CI fail when Archive or Counterexamples are noisy. There is a proposal to remove lean4checker from CI on PRs and activate it only on merges. I am happy with all of the above and your suggestion: maybe we can coordinate in a single PR?

[Damiano Testa]

Combining all the above, the proposal would be:

• make CI continue as much as reasonable after any failed test;
• ensure that Archive and Counterexamples are quiet;
• run lean4checker only at the merging stage.

[Kim Morrison]

Please don't coordinate into a single PR, that's a recipe for slow action! Each of these changes is good separately.

[Damiano Testa]

Ok, so I'll leave #11377 as is.

[Damiano Testa]

One step at a time: #11454 should be what @Yury G. Kudryashov asked.

[Damiano Testa]

I did not also make lean4checker be part of the "continuing" CI, since I actually would like to remove lean4checker from PRs and only make it run at the merging stage.