Stream: Coq devs & plugin devs

Topic: Testing anomaly that becomes error

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?

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

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

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)

Gaëtan Gilbert (Jul 09 2021 at 11:55):

so for that you have to use an output test

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

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?

Gaëtan Gilbert (Jul 09 2021 at 12:01):

just the error message, there is no anomaly

Gaëtan Gilbert (Jul 09 2021 at 12:03):

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

Last updated: Sep 09 2024 at 04:02 UTC