Stream: Coq devs & plugin devs

Topic: Testing that an error is not an anomaly

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.)

Gaëtan Gilbert (Dec 13 2021 at 10:01):

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

WDYM?

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.

Janno (Dec 13 2021 at 10:07):

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

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)

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?

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.

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?

Li-yao (Dec 14 2021 at 14:51):

Fail not catching anomalies sounds quite sensible indeed.

Paolo Giarrusso (Dec 14 2021 at 16:15):

that’s also what #12737 argues for…

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: Apr 16 2024 at 15:02 UTC