Stream: Coq devs & plugin devs

Topic: Anomalies raised by plugins

Karl Palmskog (Jun 03 2020 at 11:57):

Maybe a very basic question, but do plugins cause anomalies when they don't catch all their exceptions? The latest CoqHammer for 8.11 now regularly gives this:

Error: Hammer failed: ATPs failed to find a proof
Error: Anomaly "Uncaught exception Failure("Hammer failed")." Please report at http://coq.inria.fr/bugs/.

Is this something that should be addressed in the plugin itself?

Janno (Jun 03 2020 at 12:23):

Yes, they do. This is most likely a problem in the plugin.

Théo Zimmermann (Jun 03 2020 at 12:38):

Indeed, and maybe we should have a mechanism to adjust the "Please report" part when the anomaly comes from the plugin and not Coq itself.

Enrico Tassi (Jun 03 2020 at 12:49):

In that case it seems that the plugin author did not find the API in CErrors (user_err IIRC) to raise an error and instead raised the generic OCaml Failure exception. So fixing the bug is mostly aesthetic here, I guess.

Emilio Jesús Gallego Arias (Jun 03 2020 at 13:06):

In this case indeed the plugin failed to properly register the error with Coq, usually done by registering an error printer

Emilio Jesús Gallego Arias (Jun 03 2020 at 13:06):

but newer API for errors will be more strict on that, so indeed, that's a bug

Emilio Jesús Gallego Arias (Jun 03 2020 at 13:06):

user_err is kinda deprecated so a custom exception is preferred IMHO

Théo Zimmermann (Jun 03 2020 at 13:09):

Is it? What is the proper replacement?

Emilio Jesús Gallego Arias (Jun 03 2020 at 13:13):

We should move to a registration API as the one we discussed in your PR [can't recall what is now] There is an issue for that actually

Emilio Jesús Gallego Arias (Jun 03 2020 at 13:13):

The proper replacement for now is to provide your own exception and register a printer for it, instead of the generic user_err

Théo Zimmermann (Jun 03 2020 at 13:14):

Could you point me to the function to register a printer for an exception?

Emilio Jesús Gallego Arias (Jun 03 2020 at 13:15):

CErrors.register_handler

Emilio Jesús Gallego Arias (Jun 03 2020 at 13:15):

This is the same than in OCaml upstream

Théo Zimmermann (Jun 03 2020 at 13:16):

You were referring to coq/coq#12347 BTW.

Emilio Jesús Gallego Arias (Jun 03 2020 at 13:16):

Indeed, thanks for the pointer, I will update the issue with the discussion

Emilio Jesús Gallego Arias (Jun 03 2020 at 13:18):

Issue about user_err https://github.com/coq/coq/issues/7560 [updating it]

Enrico Tassi (Jun 03 2020 at 13:20):

Does the tactic monad catch these exceptions?

Théo Zimmermann (Jun 03 2020 at 13:24):

No IIUC. That's not the same as tclFAIL and cie. In this case of the anomaly discussed above, we could even consider that the error should have been of the latter kind (catchable by the monad).

Enrico Tassi (Jun 03 2020 at 13:31):

I guess hammer should raise an exception that is catched by the monad, so that try hammer; bla does work as expected. CErrors.user_err raises such an exception.

Théo Zimmermann (Jun 03 2020 at 13:33):

It does?

Enrico Tassi (Jun 03 2020 at 13:33):

Gong back to the deprecation, I'm not very convinced. In particular there are many errors that are just a string (like the one being discussed here). Having to declare an exception and an handler for such a simple error seems not a good design to me.

Enrico Tassi (Jun 03 2020 at 13:35):

Théo Zimmermann said:

It does?

Yes, UserError is catched by the monad. Usually the problem is the converse, it is not obvious to raise an error that is not an anomaly but still fatal (there is an API, but is a bit hidden)

Enrico Tassi (Jun 03 2020 at 13:37):

The only advantage of the registration-based API I can see is that one could be 100% sure that all possible errors in the system are documented in the refman. My personal opinion is that error messages should be self-explanatory, not documented (error 0x3345ff, anyone?). So I never liked the idea. But maybe there are aspects of the registration based API I'm missing.

Gaëtan Gilbert (Jun 03 2020 at 13:58):

"the monad" doesn't catch errors, specific combinators like enter do

Emilio Jesús Gallego Arias (Jun 03 2020 at 14:05):

I have quite a different view, in my opinion introducing a new error on the system should be so hard as to require special review. Coq has like thousands? of different errors and it is quite a hell for the users, not to speak of anomalies

Emilio Jesús Gallego Arias (Jun 03 2020 at 14:05):

Every error should be properly documented, it would be great if errors didn't need documentation, or error messages could be improved like in some modern compilers, but that first requires having more control over error proliferation

Karl Palmskog (Jun 03 2020 at 17:19):

thanks for all the feedback, but maybe someone could open an issue or PR in the CoqHammer repo with advice on how this should be solved properly? A lot of the high-level issues went over my head.

Théo Zimmermann (Jun 03 2020 at 17:21):

For now, the best is simply to advise using CErrors.user_err instead of raising an exception.

Chantal Keller (Apr 15 2022 at 15:32):

Hi
I am refreshing this old topic because it partly solved my current problem, but not exactly: what should I do if I want to raise a critical exception, but not have Please report at http://coq.inria.fr/bugs/. printed?
Thanks!

Li-yao (Apr 15 2022 at 15:34):

You can use CErrors.user_err

Chantal Keller (Apr 15 2022 at 15:37):

As far as I understand the documentation in lib/cErrors.mli, this is not a critical error, is it?
In my case, I want an error that immediately makes a tactic fail (and not only one branch of an Ltac match). This is why I used anomaly, but maybe I misunderstood?

Guillaume Melquiond (Apr 15 2022 at 15:43):

You understood correctly. And unfortunately, there are no critical user errors, only noncritical ones.

Emilio Jesús Gallego Arias (Apr 15 2022 at 15:43):

Hi @Chantal Keller , that's indeed a weak point of the design of the current tactic engine (IMVHO @Pierre-Marie Pédrot may want to contribute)

Do you have more details on what is the reason you need this exception? TTBOMK, your best bet is to use Proofview.NonLogical.raise , let me know how well that worked for you

Emilio Jesús Gallego Arias (Apr 15 2022 at 15:44):

You may need to use tclLIFT too, of course

Emilio Jesús Gallego Arias (Apr 15 2022 at 15:45):

Guillaume Melquiond said:

You understood correctly. And unfortunately, there are no critical user errors, only noncritical ones.

depends what you mean by critical, user errors are critical, what the tactic engine does is a different story, and messy, due to legacy tactic code not being properly tested. If I was able to guess @Chantal Keller 's needs correctly she may be OK with Nonlogical.raise

Guillaume Melquiond (Apr 15 2022 at 15:47):

Emilio Jesús Gallego Arias said:

depends what you mean by critical

I mean what Coq means: CErrors.noncritical (UserError _ ) = true.

Chantal Keller (Apr 15 2022 at 15:47):

I want to raise an error in case of a timeout.

Guillaume Melquiond (Apr 15 2022 at 15:48):

Then you can raise Control.Timeout, which is critical.

Chantal Keller (Apr 15 2022 at 15:48):

And it does not print Please report at http://coq.inria.fr/bugs/?

Chantal Keller (Apr 15 2022 at 15:49):

And also, I actually used anomaly because I want to make a complete error message about what produced a timeout...

Gaëtan Gilbert (Apr 15 2022 at 16:16):

Chantal Keller said:

Hi
I am refreshing this old topic because it partly solved my current problem, but not exactly: what should I do if I want to raise a critical exception, but not have Please report at http://coq.inria.fr/bugs/. printed?
Thanks!

currently you can't

Emilio Jesús Gallego Arias (Apr 15 2022 at 16:22):

Guillaume Melquiond said:

Emilio Jesús Gallego Arias said:

depends what you mean by critical

I mean what Coq means: CErrors.noncritical (UserError _ ) = true.

That's critical, in the sense of the rest of the Coq system, but that's not what the tactic engine uses, it uses catchable exceptions, so indeed you can make even UserError not to backtrack using NonLogical.raise

Emilio Jesús Gallego Arias (Apr 15 2022 at 16:24):

To summarize, if I understand the code correctly:

• tclOr (raise Foo) bar == bar but
• tclOr (tclLift (NonLogical.raise Foo)) bar) == raise Foo

So in the context of Chantal's ltac request, what she wants can be done.

Emilio Jesús Gallego Arias (Apr 15 2022 at 16:25):

or else we have a bug

Emilio Jesús Gallego Arias (Apr 15 2022 at 16:25):

(which could be a bug in the spec or in code)

Chantal Keller (Apr 15 2022 at 16:46):

I have tested tclLift (NonLogical.raise Foo) and it does backtrack :-/

Gaëtan Gilbert (Apr 15 2022 at 16:59):

Emilio Jesús Gallego Arias said:

To summarize, if I understand the code correctly:

• tclOr (raise Foo) bar == bar but
• tclOr (tclLift (NonLogical.raise Foo)) bar) == raise Foo

I would rather say
tclOr (raise Foo) bar == raise Foo (standard ocaml evaluation rules)
tclOr (tclLift (NonLogical.raise Foo)) bar) == raise (Logic_monad.Exception Foo) (thunked) (the wrapper is removed and Foo reraised at the end of running tactics (Proofview.apply))
tlcZERO Foo == backtracking error

however Goal.enter catches exceptions raised by the function passed to it (the goal -> unit tactic function) and turns them into tclZERO if they are not anomalies and not Logic_monad.Exception

it's possible that there is an interleaving of running tactics such that the nonlogical.raise becomes a backtracking exception, eg AFAICT V82.tactic (V82.of_tactic (tclLift (NonLogical.raise Foo))) == tclZERO Foo
it's possible to get an interleaving without using V82, eg tactic calls pretyping -> pretyping calls T inference -> TC inference runs a tactic

Chantal Keller (Apr 15 2022 at 17:02):

While trying to write a minimal example, it appears that I was wrong and tclLift (NonLogical.raise Foo) actually does not backtrack and seems to do what I want. I have to understand why it does not in my large piece of code :-)

Chantal Keller (Apr 15 2022 at 17:05):

@Gaëtan Gilbert oh I see, and this is probably why it is backtracking in my code... I have to inspect

Emilio Jesús Gallego Arias (Apr 19 2022 at 19:38):

@Gaëtan Gilbert indeed sorry, I missed the thunk, it should have been tclOr (fun () -> raise Foo) bar) in whatever way we can write that in the engine.

Emilio Jesús Gallego Arias (Apr 19 2022 at 19:40):

maybe it is better to say tclOr bar foo where bar does eventually raise. @Chantal Keller indeed I think that code should do what you want, but yes in a sense all "OCaml effects" including exceptions should always happen inside the Nonlogical monad.

It is time we enforce this and cleanup legacy code raising in the main monad, what we have creates a few problems.

Last updated: Nov 29 2023 at 04:01 UTC