Make it easier to interrupt a running computation

[cpitclaudel]

Forked from https://github.com/FStarLang/fstar-mode.el/issues/50. It would be nice to be able to kill Z3 from Emacs, or more generally to interrupt the current calculation. Questions:

• Is there a small example of code that takes Z3 a long time that I could use for testing?
• Could F* process a ^C signal and kill Z3 on its own?

[cpitclaudel]

Please try the 51-kill-z3 branch and tell me if C-c C-c helps there (I couldn't test it, as I don't have a small, slow example on hand)

[kkohbrok]

It seems to work, but I'm getting quite a few errors from Z3, and some of the lines in the killed block are underlined with the error: unknown assertion failed.

A couple more observations:

• the cursor jumps to the top most line of the file upon a "successful" C-c C-c.
• C-c C-c does not seem to work on the very first block.
• If there is no busy block, then pressing C-c C-c seems to kill the process the next time C-c C-n is pressed

Hope that helps a bit. If you need any testing or further info, I'm happy to help!

[s-zanella]

Doesn't work for me on Mac OS X (C-c C-c does nothing).

This small example should give you ample time to kill the Z3 process:

module N

val ack: nat -> nat -> nat
let rec ack m n =
  if m = 0 then n + 1
  else if n = 0 then ack (m - 1) 1
  else ack (m - 1) (ack m (n - 1))

#set-options "--max_fuel 16 --z3rlimit 2000"

let test =
  assert (ack 2 8 == 19)

[s-zanella]

Doesn't work on Mac OS X because process-attributes returns nil.

Found this on reddit: Should be noted that this is limited to platforms supporting process-attributes. That excludes OS X, and probably other systems without /proc. Windows is supported, though.

More info and a patch (sadly, only for the next Emacs 26 release) here: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=16579

Same problem with Cygwin Emacs.

[cpitclaudel]

@s-zanella Thanks for the test. It should be easy to run a command instead of killing z3 from ELisp on macOS. That being said, testing suggests that F isn't always robust to Z3 dying (in most cases, killing Z3 causes F to exit too, which confirms what @kkohbrok observed):

z3 exited inadvertently

Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Unexpected output from Z3: got output lines: 

Thus I'm not sure that killing z3 is the way to go. Maybe the signals approach would work better? Or maybe F* can be made more resilient to z3 crashes?

[s-zanella]

In my experience (I've doing this a lot) killing Z3 works in most situations. I came across a couple of situations where this crashed F*, but I found this quite uncommon and the feature very useful in practice.

Of course a proper solution handling signals from F* will be more elegant and robust.

[cpitclaudel]

In my experience (I've doing this a lot) killing Z3 works in most situations. I came across a couple of situations where this crashed F*, but I found this quite uncommon and the feature very useful in practice.

Noted, thanks. How do you kill the z3 process? pkill or pkill -9?

[cpitclaudel]

Actually, looks like sending a SIGINT twice does the trick. How odd.

[cpitclaudel]

Ok. @kkohbrok, can you try it again? On my machine I need to press C-c C-c it twice. Not sure why yet.

@s-zanella I changed the script it to use ps if list-system-processes isn't available. Can you try again? Hopefully glibc's macOS port has kill; otherwise I'll apply a similar workaround for signal-process.

[s-zanella]

On Mac OS X list-system-processes is available, but it returns a list of pid nil nil. I got it working after modifying the script to always use ps.

Thanks! That's a big improvement over using a shell and figuring out which Z3 process to kill when running several F* instances at the same time.

I also see the behaviour you observe @cpitclaudel: I need to hit C-c C-c twice for the Z3 process to stop. Looks like a quirk of how Z3 handles signals. It must be catching SIGINT to e.g. display statistics before quitting.

By sending SIGTERM rather than SIGINT, Z3 exits immediately but produces garbage output (same problem as @kkohbrok) and the cursor jumps to the beginning of the buffer.

[nikswamy]

I also use M-x shell-command "taskkill /im z3.exe /f" quite a lot to interrupt the prover. Would it be easier for fstar-mode.el if fstar --in reported back the pid of the z3 process it just launched?

[cpitclaudel]

@s-zanella thanks! Indeed, I'm seeing the same issue with SIGTERM, so I think we should stick with SIGINT. It seems to work reliably, and to cause Z3 produce F*-friendly output.

I tried simply sending the signal twice, but that doesn't seem to cut it. It seems that z3 needs a bit of time between the two signals. Hopefully having to press C-c C-c twice isn't too much of a burden (I'd rather understand what the root cause is than work around it).

I've improved the detection, so the function hopefully does the right thing on macOS now. Nik, can you test it on Windows? I'm hoping that gnulibc handles kill correctly there, and that process-attributes works fine too.

Would it be easier for fstar-mode.el if fstar --in reported back the pid of the z3 process it just launched?

I don't think so; I think it's simpler to just kill all z3 processes that are children of the current fstar process.

[kkohbrok]

Here are some observations I made with the current version on linux:

• first block still not retractable
• it takes two to four C-c C-c to kill actually retract a busy section. When it does work, it still shows "assertion failed" warnings in some parts of the code. For the following example, it takes two time C-c C-c if the block includes only one test and four times C-c C-c if the block includes both tests

  
  module Test

val ack: nat -> nat -> nat let rec ack m n = if m = 0 then n + 1 else if n = 0 then ack (m - 1) 1 else ack (m - 1) (ack m (n - 1))

set-options "--max_fuel 16 --z3rlimit 2000"

let test = assert (ack 2 8 == 19)

let test2 = assert (ack 2 8 == 19)

* C-c C-c followed by C-c C-n kills the process when no section is busy.

[s-zanella]

• The fact that the first block is not retractable can be explained: F* spends most of its time lax typechecking dependencies when pushing the first block of a file and can't be interrupted with C-c C-c because there's no active Z3 process to interrupt.

• Assertion failures on C-c C-c are expected: we're interrupting the Z3 process in the middle of a query, which from the point of view of F* is the same as Z3 failing to verify the query.

• I can't reproduce the C-c C-c followed by C-c C-n behaviour you see. May be specific to Linux.

[cpitclaudel]

It takes two to four C-c C-c to kill actually retract a busy section. When it does work, it still shows "assertion failed" warnings in some parts of the code. For the following example, it takes two time C-c C-c if the block includes only one test and four times C-c C-c if the block includes both tests

Interesting. I see this here too, and I'm not sure why Z3 behaves that way.

The assertion failures are indeed expected; I think they are fine (I expect this to be a temporary solution anyway, until F* can process signals)

C-c C-c followed by C-c C-n kills the process when no section is busy.

Right — it seems that F* keeps an instance of Z3, and gets confused if it dies. I disabled C-c C-c when no section is busy.

[cpitclaudel]

Ok, let's try this for now. Please report further issues, if any, in new threads :)