Stream: Coq devs & plugin devs

Topic: Testing anomaly that becomes error


view this post on Zulip Ali Caglayan (Jul 09 2021 at 11:17):

How should I add a test for an anomaly that becomes an error message? How do I distinguish between the two?

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 11:25):

Fail does not catch anomalies
If you want to test the specific error message you can also use an output test

view this post on Zulip Ali Caglayan (Jul 09 2021 at 11:48):

Really? I have an example where Fail catches anomalies:

Set Printing Universes.
Definition foo@{i j}(A:Type@{i})(B : Type@{j}) : True.
Proof.
  Fail constr_eq_strict (Type@{i}) (Type@{j}). (*normal expected failure*)
  Fail constr_eq_strict (Type@{i}) (Type@{i+1}). (*Anomaly*)
  Fail constr_eq_strict (Type@{i+1}) (Set). (*Anomaly*)
  Fail constr_eq_strict (Type@{i+1}) (Type@{j}). (*Anomaly*)
  Fail constr_eq_strict (Type@{i}) (Type@{max(i,j)}). (*Anomaly*)

This is https://github.com/coq/coq/issues/13825

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 11:52):

that's an invalid_argument, not an anomaly
(it says anomaly uncaught exception because the error printer is wonky)

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 11:55):

so for that you have to use an output test

view this post on Zulip Ali Caglayan (Jul 09 2021 at 11:56):

But this bug hasn't been fixed yet :-) It was just an example of the behavior of Fail

view this post on Zulip Ali Caglayan (Jul 09 2021 at 11:56):

But does that mean there are two bugs with 13825? The actual anomalies and the error messages?

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 12:01):

just the error message, there is no anomaly

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 12:03):

https://github.com/coq/coq/pull/14626


Last updated: Mar 28 2024 at 18:02 UTC