noisy tests

Stream: general

[Damiano Testa]

Dear All,

in the mathlib3 days, test files should not produce any form of output. I believe that this restriction was lifted in Mathlib4, due to the fact that the tactics that would allow to catch "noise" and make sure that it was of the right kind were unavailable.

Now, #guard_msgs allows for such catching and I thought that I would try out one PR where I add #guard_msgs for all the tests that contain a sorry: #6868. The test files are still noisy after this, just a little less!

However, if there is interest in going back to quiet tests, then this should be a step forward!

[Damiano Testa]

(The CI test that is currently failing is Detect changes to header SHAs and I am hoping that it will go away by running it again!)

[Mario Carneiro]

I think it is not so useful to use #guard_msgs to catch sorry specifically. It is better suited to catching errors and warnings from the thing under test

[Mario Carneiro]

But yes, I would definitely like us to move to quiet tests

[Mario Carneiro]

In most cases you can replace sorry by an axiom or hypothesis

[Scott Morrison]

Oh, sorry, I misread. Yes #guard_msgs should be used for everything except the sorries.

[Damiano Testa]

Ok, good! As I said, this was mostly a RFC and it seems that we are all on the same line! Catching sorries seemed the easiest fix to try, I'll try with the unused_variables then, maybe.

[Mario Carneiro]

that should also not be caught by #guard_msgs unless it is under test :)

[Damiano Testa]

Some of the noisy tests depend on the output of apply? and the give out a lot of information. Should these be all caught?

[Damiano Testa]

Mario, of course! I only caught sorries in test files.

[Mario Carneiro]

use set_option linter.unusedVariables false to suppress it if you can't avoid it otherwise

[Damiano Testa]

My plan was to simply prefix the unused variable with _.

[Mario Carneiro]

Mario, of course! I only caught sorries in test files.

By "under test" I mean that #guard_msgs should be capturing output from the thing the test is about, and anything else should just be quiet

[Damiano Testa]

But setting the linter in the failing declarations is also ok: what is preferred?

[Mario Carneiro]

using _ for unused variables is also fine

[Mario Carneiro]

whichever one is easier, I don't think it matters much

[Damiano Testa]

Ah, I understand my misinterpretation of "test"!

Mario Carneiro said:

Mario, of course! I only caught sorries in test files.

By "under test" I mean that #guard_msgs should be capturing output from the thing the test is about, and anything else should just be quiet

[Damiano Testa]

#6872 removes the unused_variables linter on the statements where it complained.

[Damiano Testa]

Given that I already had code to add some text before some other text for the #guard_msgs, this was easier than prefixing a _ to the unused variables (and then realizing that the unused variable was a non-declared this of an unused have!)

[Mario Carneiro]

actually it would be easier for review if you had used _, because in many cases it's not obvious why there are unused variables and it could be hiding a tactic bug

[Damiano Testa]

Done!

[Damiano Testa]

Not a huge improvement, but the lines printed by test/* are 970 in the PR, vs 985 on current master.

[Kevin Buzzard]

Got to start somewhere though :-)

[Damiano Testa]

The output of testing mathlib makes it hard to figure out which test file produced which output: is there a way to obtain the messages printed by each lake env lean test/... separately? I can always run the command locally, but I was wondering if I am just missing something from the CI output.

[Eric Wieser]

Mario Carneiro said:

In most cases you can replace sorry by an axiom or hypothesis

An axiom seems safer to me, as a hypothesis could be located by an eager tactic and defeat the point of the test

[Mario Carneiro]

Either one is fine with me

[Damiano Testa]

I've revamped #6868 using axiom test_sorry instead of #guard_msgs for the sorry. I tried to make the files that are touched by the PR entirely quiet, which means that I also added some _ for unused variables and some #guard_msgs for outputs of exact?/apply?/rw?.

Adding the axiom also made some instances/defs noncomputable and I marked those as Lean instructed me to!

On master, there are about 950 lines of output from tests, this PR removes about 300 of those lines.

[Damiano Testa]

(Quite a few of those lines became inputs to #guard_msgs: the PR add 563 lines, most of which are really Try this messages.)

[Damiano Testa]

This is an update on the noisy tests.

Test                                No of lines of output
----------------------------------------------------------
test/DeriveFintype.lean             7
test/Expr.lean                      4
test/FBinop.lean                    1
test/Find.lean                      57
test/Imports.lean                   4
test/MLList.lean                    5
test/MaxPowDiv.lean                 1
test/TypeCheck.lean                 7
test/eqns.lean                      1
test/finset_repr.lean               4
test/finsupp_notation.lean          1
test/left_right.lean                2
test/search/DepthFirst.lean         1
test/success_if_fail_with_msg.lean  1
test/symm.lean                      1
test/trace.lean                     2
test/vec_notation.lean              6

(all remaining tests have no output)

[Kevin Buzzard]

Thanks so much!