Noisy files and CI

Stream: general

[Damiano Testa]

I believe that the current CI setup allows some noisy files to pass through CI.

You can take a look at #12884, where a file with a logInfo gets a CI pass.

I modified the "noisy" step of CI in #12886 to catch this sort of issue. You can see that the same file fails the new CI in #12885.

[Kim Morrison]

:writing:

[Damiano Testa]

Comments added!

[Damiano Testa]

In fact, our current tests for noisiness allow sorry in examples (#12912) and probably also in theorems (#12913).

[Damiano Testa]

I think that it all boils down to the fact that lake no longer prepends stdout/stderr to messages, but has switched to info/warning/error. The current CI filters the output by scanning for the no-longer-used words.