Zulip Chat Archive

Stream: mathlib4

Topic: Writing tests that fail


Thomas Murrills (Jan 06 2023 at 07:23):

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 (Jan 06 2023 at 07:28):

In mathlib3 we had success_if_fail_with_msg. Can we port that?

Thomas Murrills (Jan 06 2023 at 09:34):

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 (Jan 06 2023 at 09:35):

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 (Jan 06 2023 at 17:53):

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 (Jan 06 2023 at 18:20):

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 (Jan 06 2023 at 18:21):

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

Thomas Murrills (Jan 06 2023 at 18:33):

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 (Jan 06 2023 at 18:34):

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 (Jan 06 2023 at 18:48):

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

Floris van Doorn (Jan 06 2023 at 18:55):

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

Floris van Doorn (Jan 06 2023 at 18:55):

But that is a monad operation, but a tactic.

Thomas Murrills (Jan 06 2023 at 21:37):

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 (Jan 06 2023 at 21:41):

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

Thomas Murrills (Jan 06 2023 at 21:41):

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

Floris van Doorn (Jan 06 2023 at 23:56):

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 (Jan 07 2023 at 01:52):

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

Thomas Murrills (Jan 07 2023 at 02:27):

Isn’t that the opposite?

Scott Morrison (Jan 07 2023 at 02:43):

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

Scott Morrison (Jan 07 2023 at 02:43):

Both swap success and failure of the enclosed tactic.

Thomas Murrills (Jan 07 2023 at 02:51):

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

Kevin Buzzard (Jan 07 2023 at 08:01):

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


Last updated: Dec 20 2023 at 11:08 UTC