[error] Replace msg_error by a proper exception. #6262
Conversation
engine/logic_monad.ml
Outdated
| @@ -107,7 +107,7 @@ struct | |||
| let print_debug s = make (fun _ -> Feedback.msg_info s) | |||
| let print_info s = make (fun _ -> Feedback.msg_info s) | |||
| let print_warning s = make (fun _ -> Feedback.msg_warning s) | |||
| let print_error s = make (fun _ -> Feedback.msg_error s) | |||
| (* let print_error s = make (fun _ -> Feedback.msg_error s) *) | |||
There was a problem hiding this comment.
Why comment instead of removing?
There was a problem hiding this comment.
Yup, it seems that print_error actually makes little sense, instead you want to "raise an error"
library/summary.ml
Outdated
| @@ -107,7 +107,7 @@ let unfreeze_summaries fs = | |||
| try fold id decl state | |||
| with e when CErrors.noncritical e -> | |||
| let e = CErrors.push e in | |||
| Feedback.msg_error | |||
| Feedback.msg_warning | |||
There was a problem hiding this comment.
I don't know the implications of this. Are warning and error feedbacks interpreted in the same way, say in CoqIDE? It looks strange to print a warning message that is actually an error, right? Should it be fixed in another way?
There was a problem hiding this comment.
This error should be pretty uncommon. I wonder why it's not an anomaly actually.
There was a problem hiding this comment.
So it is really a bit of a remaining mess, because what we want to do in an error is raise an exception and let the handler print it. But some handlers want to "decorate" the printing exception. So I dunno how to proceed.
There was a problem hiding this comment.
This PR just fixed the msg_error not being printed, even in a non-optimal way in these two [extremely rare] cases.
910e666 to
da02558
Compare
da02558 to
beb9747
Compare
|
Not a lot to review here, the change is a clear bugfix, comments about the status of error handling should go on their own issue #5479 is a good place to start. |
|
Sorry, but I don't understand why this PR changes a few occurrences of |
|
If code needs to submit an error, it must raise an exception. We are missing a mechanism to decorate exceptions, and I don't want to add one, neither to touch the offending code [marginal and rare errors] so I am indeed turning a no-op message into a warning. I could also be msg_info. There is no point in adding a decoration for exceptions [we already have a half-baked one] or tweaking the offending code until we don't fix the more fundamental issues pointed out in the bugs about error handling. |
|
In fact look at the current documentation of what it he point of such a function? Now the STM sends a |
b98525d to
408211a
Compare
kernel/nativelib.ml
Outdated
| @@ -158,7 +158,7 @@ let call_linker ?(fatal=true) prefix f upds = | |||
| with Dynlink.Error e as exn -> | |||
| let exn = CErrors.push exn in | |||
| let msg = "Dynlink error, " ^ Dynlink.error_message e in | |||
| if fatal then (Feedback.msg_error (Pp.str msg); iraise exn) | |||
| if fatal then (Feedback.msg_warning (Pp.str msg); iraise exn) | |||
There was a problem hiding this comment.
This should not be made a warning-level printing. From what I understand from this PR, this data (msg) should be part of the exception. I'm not sure how that can be done, since we don't know the exception statically. But I'll have to think more. Probably it is the handler logic that should be fixed to print the right message.
There was a problem hiding this comment.
I wish there was a simple fix to this, but a proper fix is involved due to the complicated state of error handling/printing system. This PR is pragmatic: at least output something, vs the current state of not outputting anything.
If the STM / protocol was not broken in that regard indeed we could use msg_error, but that is not the case.
408211a to
e08a7b7
Compare
|
The discussion here doesn't seem to be resolved, so postponing. |
|
Well, I would add this 8.7-only. Now, some messages are just not printed, with the patch, they are printed as a warning + an error later on. Clearly the last option is much better. |
|
When has |
|
Yeah I don't see it, even after reading #5479. IIUC, |
|
I have explained quite a few times, |
|
So you are saying that when I wrote |
If you have a link to previous explanations, I'd be happy to read. |
|
The only reliable way to print errors is to send and exception. The problem with the logic is that it doesn't print a message on some exceptions, so if you print So the only sensible way is indeed to ignore |
Depends on what time of the year was, and what your UI was. But likely what you saw was the message embedded in the exception after it. |
|
@maximedenes ping |
|
Sorry, but I'm still not convinced. In particular, how are we going to distinguish warnings from errors after this change? That is, warnings that are intended to be warnings and warnings that are intended to be errors, but that wouldn't print if we used I would be happier if at least we were using a distinct function ( |
I think you are missing the point of this patch, no error is lost by this change, in fact a few ones that were lost have been recovered. Said otherwise, there is no place where such change should happen AFAICT, so the patch is good to go. As we have discussed, the state of error handling is not good, in particular since the introduction of resilient stuff which brought into play two different kind of errors [fatal and recoverable], but these issues should be addressed on a separate PR. We cannot reuse |
|
@ejgallego I think you completely missed Maxime's concern. It's not about the effect that these functions were having (whether they were printing something or not) but about the information loss inside the code. These changes from |
I am not missing the point, originally these functions were using just the "print to stderr" function and when we did the transition to the feedback combinators the warning/error thing got chosen arbitrarily, as both warning and errors were printed the same in the old system [to stderr]. There is no information to preserve, but a lot of code to clean up and a many many absolutely non-trivail fixes to the error handling code to be done. |
|
OK, so Emilio's answer is that these error messages were recently and arbitrarily separated into |
I have carefully considered all the suggestions and I still think that the current version is the best, at least I cannot appreciate an improvement in any of the suggestions but I do however see misconceptions about what the current state of the system which I would rather not see perpetuated in the form of falsely pretending the code is going to be less broken than what it is today. The situation is very complex to understand thou, but let me summarize: error handling is globally broken, and nothing we do in this PR will change it. If people want to help please start by having a look at the bugs that I've pointed out. I am not willing to invest a lot of time more on this PR, if due to micromanagement a PR containing critical fixes is not merged, well, c'est la vie. |
|
Let's take a concrete example: turning The code I wrote was using |
|
That's a good example, but note what the original code did: So indeed in c78e8d3 the code was changed to use Basically you want a feature of the error handling system [enriching an existing exception] that doesn't exist or is broken, so it cannot be satisfied in this PR. Other parts of the code have implemented some kind of enriching system similar to the one here. But certainly calling |
|
In this case the top-level error printer should learn about But again that's a separate PR not related to this one. |
I don't want this PR to fix the problem. I want it not to lose the information that I meant an error there. I don't see what is the problem in adding a comment... |
|
So for that one a PR "Improve printing of Dynlink erros" teaching the general error printer about dynlink should be submitted. For the code in STM, the situation is complex but I believe this is the best we can do until we fix some other stuff, similarly for toplevel. I don't see more msg_warning other than those. |
The information is not lost, |
Do you mean you are going to fix it now? |
|
Done #6729 |
|
Of course this PR could have been merged long time ago but now I'll eat another rebase, mais c'est la vie mes amis |
Instead, we properly register a printer for such exception and update the code.
The current error mechanism in the core part of Coq is 100% exception based; there was some confusion in the past as to whether raising and exception could be replace with `Feedback.msg_error`. As of today, this is not the case [due to some issues in the layer that generates error feedbacks in the STM] so all cases of `msg_error` must raise an exception of print at a different level [for now].
4c7909d to
33789b2
Compare
|
@ejgallego I can't backport as-is because this removes stuff from |
|
@Zimmi48 sure you can keep that one. |
The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with
Feedback.msg_error.As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of
msg_errormust raise an exception of print at a different level [for now].