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?
Yes, they do. This is most likely a problem in the plugin.
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.
In that case it seems that the plugin author did not find the API in
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.
In this case indeed the plugin failed to properly register the error with Coq, usually done by registering an error printer
but newer API for errors will be more strict on that, so indeed, that's a bug
user_err is kinda deprecated so a custom exception is preferred IMHO
Is it? What is the proper replacement?
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
The proper replacement for now is to provide your own exception and register a printer for it, instead of the generic
Could you point me to the function to register a printer for an exception?
This is the same than in OCaml upstream
You were referring to coq/coq#12347 BTW.
Indeed, thanks for the pointer, I will update the issue with the discussion
Issue about user_err https://github.com/coq/coq/issues/7560 [updating it]
Does the tactic monad catch these exceptions?
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).
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.
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.
Théo Zimmermann said:
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)
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.
"the monad" doesn't catch errors, specific combinators like enter do
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
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
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.
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