Hi folks, I am seeing quite a few problems with code that is not safe w.r.t. async interruptions, in this case I'm talking about the current check_for_interrupt
check and 8.17. What is the state of master
w.r.t. this?
Being able to interrupt Coq is critical for quite a few applications.
I'm seeing this is very heavy SSR code
What's the check_for_interrupt problem?
Control.interrupt
(from a different thread)check_for_interrupt
, which raises the Sys.Break
exceptionI was able to get a pretty interesting message about tclZERO
getting an interrupt and that being an anomaly, testing 8.18 now
Best way to reproduce is to open for example topology.v from analysis in coq-lsp, then do a lot of hover / clicking around to see goals, you'll get spurious errors
What I would expect in step 3 is to get the exception myself, so I can handle that and I know the command was interrupted
I set check_for_interrupt (from a different thread)
Do you mean call? It's a function not a ref
Sorry, indeed I set Control.interrupt
let me edit the message
8.18 is similar, sometimes (rarely) I can trigger this message:
let tclZERO ?(info=Exninfo.null) e =
if not (CErrors.noncritical e) then
CErrors.anomaly (Pp.str "tclZERO receiving critical error: " ++ CErrors.print e);
Proof.zero (e, info)
But more often just the interrupt is absorbed, so I see what it looks like a legitimate failure.
I'll cc: @Pierre-Marie Pédrot
is it different after https://github.com/coq/coq/pull/17638 ?
Oh I was under the impression that had gone in 8.18
Let me indeed test master
Indeed ssr code seems much better in master
!
Maybe that PR worth backporting?
Another question is how to ensure new code / plugins are doing the right thing here?
Last updated: Oct 13 2024 at 01:02 UTC