CI: noisy "test mathlib"

Stream: mathlib4

[Michael Stoll]

In a recent CI run, I noticed this output from the "test mathlib" stage:

⚠ [5831/5840] Built MathlibTest.AssertImported
warning: ././././MathlibTest/AssertImported.lean:9:0: ❌️ 'CStarAlgebra.star' (declaration) asserted in 'Mathlib.Topology.ContinuousMap.Bounded.Basic'.
---
✅️ means the declaration or import exists.
❌️ means the declaration or import does not exist.

This does not lead to a CI failure, but out of curiosity: is this intended?

[Ruben Van de Velde]

I assume not

[Damiano Testa]

I agree that this is not as intended. The test reports a warning, but maybe the setting used to run the tests is not "warning as failures".

[Ruben Van de Velde]

CC @Kim Morrison

[Damiano Testa]

Seems to have been introduced in #19187.

[Damiano Testa]

At 54d12203eb as a commit to master.

[Damiano Testa]

I wonder if the issue is that the test step is contained in this action and it hides the error.

[Damiano Testa]

The other issue is probably that the assert not exist should be on docs#StarRing.star, rather than on docs#CStarAlgebra.star.

[Damiano Testa]

docs#CStarRing, maybe?

[Damiano Testa]

I am hoping that #19226 is what Kim had in mind.

[Bryan Gin-ge Chen]

Damiano Testa said:

I wonder if the issue is that the test step is contained in this action and it hides the error.

I didn't look into the problem matcher action carefully but it didn't seem like it had any config options on this front, so I wonder if we need to run the tests in a separate step and then feed the output to the action afterwards.

In the mathlib3 days we had a python script which complained if there were noisy files, but I guess that went away at some point.

[Damiano Testa]

#19227

[Damiano Testa]

I propose to just remove the wrapper: it is unclear what suggestions would be reasonable for a failed test.

[Damiano Testa]

Supposedly, lake test already fails on noisy tests, so I am hoping that this will be enough.

[Damiano Testa]

Since master still has the failure above, we will see if unwrapping make CI complain about the PR.

[Damiano Testa]

Oh, even without the wrapping action it still passes the tests.

[Damiano Testa]

I am still hoping that there is a way to make the tests fail so that CI does not continue, rather the inspecting the output of the lake test step.

[Damiano Testa]

I made the test fail less gracefully and now the exit code is 1.

[Damiano Testa]

I do not know if there is any point in keeping the action wrapper on this step, though.

[Damiano Testa]

With #19226 merged, mathlib's tests are silent again!

[Damiano Testa]

There is still the issue of making sure that they stay silent, even if future changes will make them fail.

[Damiano Testa]

#19227 makes sure that this particular test will produce an error, instead of a warning and therefore make CI fail.

[Damiano Testa]

However, maybe lake test should be responsible for making sure that the tests are not noisy?

[Kim Morrison]

Damiano Testa said:

However, maybe lake test should be responsible for making sure that the tests are not noisy?

@Mac Malone, can we make use of existing --wfail (I forget if there is a version for info messages, and the Lake README doesn't even mention --wfail.) machinery here?

[Mac Malone]

Yes you can! lake --iofail test will fail if the test library produces any output.

[Damiano Testa]

Any message would be good. The earlier issue that was noted was that also logWarning did not cause lake test to fail.

[Mac Malone]

(As for documentation, CLI options appear in the lake --help ouptut, not currently the README.)

[Kim Morrison]

Mac Malone said:

Yes you can! lake --iofail test will fail if the test library produces any output.

@Damiano Testa can I take your octopus to mean you will make the PR for this? :-)

[Damiano Testa]

Kim Morrison said:

Mac Malone said:

Yes you can! lake --iofail test will fail if the test library produces any output.

Damiano Testa can I take your octopus to mean you will make the PR for this? :-)

Sure! This would be to Batteries, right? Where lake test is defined?

[Kim Morrison]

No, this Mathlib CI

[Kim Morrison]

Literally replacing lake test with lake --iofail test in build.in.yml

[Kim Morrison]

(and then checking it works :-)

[Damiano Testa]

Ok, let me take care of this!

[Damiano Testa]

#19268 adds the option to lake test and #19269 failed with a test that just had #eval "".

[Damiano Testa]

Btw, does this mean that the lake build step could also be using lake --iofail build, instead of bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"?

[Mac Malone]

Probably.

[Edward van de Meent]

Damiano Testa said:

Kim Morrison said:

Mac Malone said:

Yes you can! lake --iofail test will fail if the test library produces any output.

Damiano Testa can I take your octopus to mean you will make the PR for this? :-)

Sure! This would be to Batteries, right? Where lake test is defined?

Ever since mathlib tests became their own library, lake test didn't use the batteries tool anymore. Aamof, even batteries doesn't use its own testing tool for testing!

[Edward van de Meent]

It still exists, just doesn't get used by either Batteries or Mathlib

[Michael Rothgang]

Damiano Testa said:

Btw, does this mean that the lake build step could also be using lake --iofail build, instead of bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"?

(How) would this set LEAN_ABORT_ON_PANIC=1? (Is that still needed?)

[Damiano Testa]

You can try it on a file

#eval
  let ls := [0]
  ls[1]!

It is both noisy and lake --iofail build <thatFile> fails.