Writing tests that fail

Stream: mathlib4

[Thomas Murrills]

In lean4 core, tests come with expected.out files which confirm that certain error messages/traces/etc. are generated.

I don't see those in mathlib4; how do we specify that we want a certain example in a test file to fail in a certain way?

[Scott Morrison]

In mathlib3 we had success_if_fail_with_msg. Can we port that?

[Thomas Murrills]

For the time being I'm just going to leave commented code in test files describing what the behavior should be when uncommented, I guess?

[Thomas Murrills]

There are also certain instances where we're not in a tactic but still want to demonstrate certain error-message functionality. I imagine it's low-priority at the moment, but I wonder if we could have similar *.expected.out files somehow.

[Heather Macbeth]

Scott Morrison said:

In mathlib3 we had success_if_fail_with_msg. Can we port that?

I opened mathlib4#1390 to record this.

[Floris van Doorn]

There are a bunch of @[simps] tests that also used this, and for now are just using the less informative success_if_fail.

[Heather Macbeth]

I didn't realise we had success_if_fail, @Thomas Murrills you can probably use this for now?

[Thomas Murrills]

A bit of poking around reveals it might be called expect_failure and expect_failure_msg now? Trying to use success_with_failure hits me with “unknown tactic”, and I can’t find it in mathlib4.

[Thomas Murrills]

Does this look like a good way to write this test?

example : 3 ^ 3 + 4 = 31 := by
  expect_failure_msg "type mismatch
  HEq.rfl
has type
  HEq ?m.38198 ?m.38198 : Prop
but is expected to have type
  3 ^ 3 + 4 = 31 : Prop" (norm_num1; with_reducible rfl)
  admit

[Yaël Dillies]

I'm afraid the ?m.38198 is not import changes-resilient.

[Floris van Doorn]

It's called successIfFail in Mathlib.Lean.Exception.

[Floris van Doorn]

But that is a monad operation, but a tactic.

[Thomas Murrills]

I see. I think I'll do this particular test with a syntactic guard_target followed by an admit, but this is all good to know!

[Thomas Murrills]

Or, wait. Is admit frowned upon in tests? is successIfFail better?

[Thomas Murrills]

I'm not totally sure how to translate the monad operation into a tactic in this case.

[Floris van Doorn]

In Lean 3 we mandated that all tests are silent. In Lean 4 I think that might also be nice, but we're not doing it at the moment.
I prefer doing a successIfFail followed by some (trivial) way to close the goal, which you can usually ensure there exists by changing the example a little bit.

[Scott Morrison]

There is a tactic fail_if_success, defined in core Lean 4, that is used in test/.

[Thomas Murrills]

Isn’t that the opposite?

[Scott Morrison]

Confusingly, fail_if_success and successIfFail mean the same thing. :-)

[Scott Morrison]

Both swap success and failure of the enclosed tactic.

[Thomas Murrills]

so what you’re saying is…it should really be called fail_iff_success :)

[Kevin Buzzard]

You can switch off universes being displayed with set_option pp.universes false if this is still an issue