Comments (16)
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)
from fstar-mode.el.
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!
from fstar-mode.el.
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)
from fstar-mode.el.
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.
from fstar-mode.el.
@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?
from fstar-mode.el.
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.
from fstar-mode.el.
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
?
from fstar-mode.el.
Actually, looks like sending a SIGINT twice does the trick. How odd.
from fstar-mode.el.
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
.
from fstar-mode.el.
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.
from fstar-mode.el.
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?
from fstar-mode.el.
@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.
from fstar-mode.el.
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.
from fstar-mode.el.
-
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 byC-c C-n
behaviour you see. May be specific to Linux.
from fstar-mode.el.
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.
from fstar-mode.el.
Ok, let's try this for now. Please report further issues, if any, in new threads :)
from fstar-mode.el.
Related Issues (20)
- F* over TRAMP crashes HOT 17
- No company completion HOT 4
- fstar-mode over docker-tramp HOT 5
- fstar-jump-to-definition on a module should jump to the fsti if it exists HOT 1
- Code that typechecks normally from the command line can crash fstar-mode HOT 1
- Cleanup of compiler hacking subp-prover args in fstar-mode.el HOT 6
- `nil` confusion HOT 2
- fslit seems to no longer work very well HOT 6
- can't include file in subdirectory with fslit HOT 4
- Weird display of the highlighted blocks HOT 1
- Highlight sladmit
- c-c c-v verify should ask to save the current file HOT 5
- fstar literate setup problems on Ubuntu 22.04 and emacs 28 HOT 4
- Not all errors going to *Flycheck errors*
- Open not always working HOT 1
- c-c c-r reload better description HOT 3
- elaborate trace mode HOT 2
- Definition lookup works only once
- Using F* remotely, over TRAMP HOT 5
- advancing is missing a bunch of new top-level constructs HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from fstar-mode.el.