chore: use #guard_msgs in run tests

[semorrison]

Many of our tests in tests/lean/run/ produce output from #eval (or #check) statements, that is then ignored.

This PR tries to capture all the useful output using #guard_msgs. I've only done a cursory check that the output is still sane --- there is a chance that some "unchecked" tests have already accumulated regressions and this just cements them!

In the other direction, I did identify two rotten tests:

• a minor one in setStructInstNotation.lean, where a comment says Set Nat, but #check actually prints ?_. Weird?
• CompilerProbe.lean is generating empty output, apparently indicating that something is broken, but I don't know the signficance of this file.

In any case, I'll ask about these elsewhere.

(This started by noticing that a recent grind test file had an untested trace_state, and then got carried away.)

[nomeata]

Thanks a lot!

Once that is taken care of, I’d like to propose that a run test with any output is considered failing, to avoid mistakes.

(And then we could actually remove special handling of run and treat an absent .expected file as indicating that the expected output is empty. Maybe with an opt-in escape hatch for “really ignore this output, even though I cannot use #guard_msg for it.)

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-4175 has successfully built against this PR. (2024-05-15 14:41:09) View Log
• ✅ Mathlib branch lean-pr-testing-4175 has successfully built against this PR. (2024-05-16 01:50:03) View Log

[semorrison]

Once that is taken care of, I’d like to propose that a run test with any output is considered failing

We're not quite there yet. There are many #check statements that I though it was pointless to wrap in #guard_msgs. The output here is irrelevant, the point in the test file is that it typechecks.

There are also many cases where a test either #prints a large statement, or looks a IR output, or long simp/defeq/etc trace output... So there is more thought and cleanup required before we can silence tests.

I guess the intermediate solution is to split run into the quiet ones and the noisy ones.

[nomeata]

I'd the point of the check command is not it's output, you can make that explicit using #guard_msgs() in, can't you?

[digama0]

I'd the point of the check command is not it's output, you can make that explicit using #guard_msgs() in, can't you?

I think you mean #guard_msgs(drop info)

[nomeata]

Some variant thereof, yes :-D