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 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.
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 user_err
Could you point me to the function to register a printer for an exception?
CErrors.register_handler
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.
It does?
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:
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)
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.
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!
You can use CErrors.user_err
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?
You understood correctly. And unfortunately, there are no critical user errors, only noncritical ones.
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
You may need to use tclLIFT
too, of course
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
Emilio Jesús Gallego Arias said:
depends what you mean by critical
I mean what Coq means: CErrors.noncritical (UserError _ ) = true
.
I want to raise an error in case of a timeout.
Then you can raise Control.Timeout
, which is critical.
And it does not print Please report at http://coq.inria.fr/bugs/
?
And also, I actually used anomaly
because I want to make a complete error message about what produced a timeout...
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 havePlease report at http://coq.inria.fr/bugs/.
printed?
Thanks!
currently you can't
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
To summarize, if I understand the code correctly:
tclOr (raise Foo) bar == bar
buttclOr (tclLift (NonLogical.raise Foo)) bar) == raise Foo
So in the context of Chantal's ltac request, what she wants can be done.
or else we have a bug
(which could be a bug in the spec or in code)
I have tested tclLift (NonLogical.raise Foo)
and it does backtrack :-/
Emilio Jesús Gallego Arias said:
To summarize, if I understand the code correctly:
tclOr (raise Foo) bar == bar
buttclOr (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
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 :-)
@Gaëtan Gilbert oh I see, and this is probably why it is backtracking in my code... I have to inspect
@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.
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: Jun 08 2023 at 04:01 UTC