Stream: Coq devs & plugin devs

Topic: Testing that an error is not an anomaly


view this post on Zulip Hugo Herbelin (Dec 13 2021 at 09:58):

Hi, how do we test that a failure is a proper error and not an anomaly these days? (It seems that the behavior of Fail changed in 8.11 wrt to anomalies.)

view this post on Zulip Gaëtan Gilbert (Dec 13 2021 at 10:01):

(It seems that the behavior of Fail changed in 8.11 wrt to anomalies.)

WDYM?

view this post on Zulip Hugo Herbelin (Dec 13 2021 at 10:04):

Below, Extraction F raises a Not_found anomaly. From 8.11, this anomaly is catched by Fail.

Require Import Extraction.
Module Type T. End T.
Module F (X:T). Declare Module X : T. End F.
Fail Extraction F.

view this post on Zulip Janno (Dec 13 2021 at 10:07):

Possibly related to the discussion in https://github.com/coq/coq/issues/12737?

view this post on Zulip Gaëtan Gilbert (Dec 13 2021 at 10:17):

I guess the noncritical from be9a1834a48393185ec9cfd9c18d157fd2a7ff02 should be not (is_anomaly)?
is_anomaly is not great code though (calling is_handled so it does printing and throws it away)

view this post on Zulip Hugo Herbelin (Dec 14 2021 at 07:42):

Gaëtan Gilbert said:

I guess the noncritical from be9a1834a48393185ec9cfd9c18d157fd2a7ff02 should be not (is_anomaly)?
is_anomaly is not great code though (calling is_handled so it does printing and throws it away)

I would say so. Is there some consensus, or at least not-not-consensus, that we don't want Fail to catch anomalies?

view this post on Zulip Hugo Herbelin (Dec 14 2021 at 07:46):

Janno said:

Possibly related to the discussion in https://github.com/coq/coq/issues/12737?

Related in the sense that it is difficult to define what is an anomaly w/o calling the error handler which will then be in time proportional to the number of declared errors. But unrelated in that it is about a handler in a different part of the code.

view this post on Zulip Hugo Herbelin (Dec 14 2021 at 07:51):

Then catchable_exception catches Not_found, Exit, NotConvertible, and any other exceptions that is supposed to only communicate internal information between internal functions. Should this be considered a bug?

view this post on Zulip Li-yao (Dec 14 2021 at 14:51):

Fail not catching anomalies sounds quite sensible indeed.

view this post on Zulip Paolo Giarrusso (Dec 14 2021 at 16:15):

that’s also what #12737 argues for…

view this post on Zulip Paolo Giarrusso (Dec 14 2021 at 16:16):

and this choice seems canonical, as long as we agree that the right reaction for anomalies lies in bugtracking not backtracking.


Last updated: Feb 06 2023 at 18:03 UTC