Stream: Coq devs & plugin devs

Topic: Situation of async interruptions


view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 15:22):

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 masterw.r.t. this?

Being able to interrupt Coq is critical for quite a few applications.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 15:25):

I'm seeing this is very heavy SSR code

view this post on Zulip Gaëtan Gilbert (Sep 22 2023 at 15:28):

What's the check_for_interrupt problem?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 15:52):

  1. I set Control.interrupt (from a different thread)
  2. The code at some point does the check_for_interrupt, which raises the Sys.Break exception
  3. The exception is not properly handled, I get instead a regular error, the tactic in question fails, and Coq is kind of borked

I was able to get a pretty interesting message about tclZERO getting an interrupt and that being an anomaly, testing 8.18 now

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 15:54):

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 15:57):

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

view this post on Zulip Gaëtan Gilbert (Sep 22 2023 at 15:58):

I set check_for_interrupt (from a different thread)

Do you mean call? It's a function not a ref

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 16:00):

Sorry, indeed I set Control.interrupt

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 16:00):

let me edit the message

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 16:06):

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)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 16:07):

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

view this post on Zulip Gaëtan Gilbert (Sep 22 2023 at 16:09):

is it different after https://github.com/coq/coq/pull/17638 ?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 16:10):

Oh I was under the impression that had gone in 8.18

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 16:11):

Let me indeed test master

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 16:49):

Indeed ssr code seems much better in master!

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 16:50):

Maybe that PR worth backporting?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 16:51):

Another question is how to ensure new code / plugins are doing the right thing here?


Last updated: Apr 14 2024 at 11:02 UTC