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_interruptcheck and 8.17. What is the state of
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
I 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
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
Indeed ssr code seems much better in
Maybe that PR worth backporting?
Another question is how to ensure new code / plugins are doing the right thing here?
Last updated: Nov 29 2023 at 22:01 UTC