Stream: Coq devs & plugin devs

Topic: Anomalies raised by plugins


view this post on Zulip 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?

view this post on Zulip Janno (Jun 03 2020 at 12:23):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2020 at 13:06):

user_err is kinda deprecated so a custom exception is preferred IMHO

view this post on Zulip Théo Zimmermann (Jun 03 2020 at 13:09):

Is it? What is the proper replacement?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jun 03 2020 at 13:14):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2020 at 13:15):

CErrors.register_handler

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2020 at 13:15):

This is the same than in OCaml upstream

view this post on Zulip Théo Zimmermann (Jun 03 2020 at 13:16):

You were referring to coq/coq#12347 BTW.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2020 at 13:16):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2020 at 13:18):

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

view this post on Zulip Enrico Tassi (Jun 03 2020 at 13:20):

Does the tactic monad catch these exceptions?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jun 03 2020 at 13:33):

It does?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jun 03 2020 at 13:58):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.


Last updated: Oct 21 2021 at 20:02 UTC