search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.69k stars 232 forks source link

F# binary mistakes z3 directory in PATH for z3 executable (on Unix) #978

Open catalin-hritcu opened 7 years ago

catalin-hritcu commented 7 years ago

This is a regression that appears on Linux with the F# binary:

$ fstar.exe --verify_module hello hello.fst
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
ApplicationName='z3', CommandLine='-version', CurrentDirectory='', Native error= Cannot find the specified file
$ z3 -h
Z3 [version 4.5.0 - 64 bit]. (C) Copyright 2006-2016 Microsoft Corp.
[...]

This used to work well, and I guess might be caused by the Linux z3 binary not having the exe extension? It also fails in a bad way, although that was supposed to be fixed already #336

@wintersteiger Thoughts on this?

wintersteiger commented 7 years ago

I build/run the Linux mono version frequently and I can confirm that it's picky about paths and filenames, but it works fine for me. But, I use the Ubuntu on Windows subsystem and mono is set to automatically translate Windows paths to Linux paths, so that all gets a bit complicated. Does it work if you set it via --smt?

catalin-hritcu commented 7 years ago

Just tried and it does work with --smt:

$ which z3
/home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin/z3
$ ../../bin/fstar.exe --smt /home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin/z3 --verify_module hello hello.fst
./hello.fst(5,0-5,37): (Warning) Top-level let-bindings must be total; this term may have effects
Verified module: Hello (26 milliseconds)
All verification conditions discharged successfully
ad-l commented 7 years ago

Try PATH=/home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin bin/fstar.exe hello.fst A possible source of this problem is that one of the entires in your $PATH contains a space.

catalin-hritcu commented 7 years ago

@ad-l setting the PATH as you said does make this problem go away. My PATH doesn't contain spaces though.

[hritcu@resurrected hello]$ PATH=/home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin ../../bin/fstar.exe hello.fst           (git)-[master] 
./hello.fst(5,0-5,37): (Warning) Top-level let-bindings must be total; this term may have effects
Verified module: Hello (27 milliseconds)
All verification conditions discharged successfully
[hritcu@resurrected hello]$ ../../bin/fstar.exe hello.fst                                                                (git)-[master] 
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
ApplicationName='z3', CommandLine='-version', CurrentDirectory='', Native error= Cannot find the specified file
[hritcu@resurrected hello]$ echo $PATH                                                                                   (git)-[master] 
/home/hritcu/.opam/4.04.0/bin:/home/hritcu/bin:/home/hritcu/Apps/Vampire---4.1:/home/hritcu/Projects/fstar/pub/bin/:/home/hritcu/.npm-global/bin:/home/hritcu/Apps/coq-8.5pl2/bin:/home/hritcu/Apps/SPASS-3.7/SPASS:/home/hritcu/Apps/E-1.8/PROVER:/home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin:/home/hritcu/Apps/ott_distro_0.24/bin/:/home/hritcu/.local/bin/:/home/hritcu/.cabal/bin:/home/hritcu/Apps/cvc4-1.1/bin:/home/hritcu/Apps/k-3.3/bin:/home/hritcu/Apps/proverif1.88:/home/hritcu/Apps/racket/bin:/home/hritcu/Apps/Isabelle2016/bin:/home/hritcu/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin
[hritcu@resurrected hello]$

Is F* directly playing with the PATH?

mtzguido commented 7 years ago

I'm puzzled by this. It works for me even using your $PATH.

Shot in the dark, is your PATH variable exported? Can you try running export PATH just before F*?

If this fixes it, you might need to it add it to your .bashrc.

catalin-hritcu commented 7 years ago

@mtzguido Tried exporting PATH, but didn't seem to help.

[hritcu@resurrected hello]$ export PATH                                                                               (git)-[master] 
[hritcu@resurrected hello]$ ../../bin/fstar.exe hello.fst                                                             (git)-[master] 
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
ApplicationName='z3', CommandLine='-version', CurrentDirectory='', Native error= Cannot find the specified file
parno commented 7 years ago

FWIW, I'm seeing similar behavior on Mac OS X (10.12.3). Z3 is on my path (which doesn't contain any spaces), but FStar can't find it unless I explicitly specify the path with the --smt option.

parno@Picasso:~$ echo $PATH
/Users/parno/.opam/system/bin:/Users/parno/.rbenv/shims:/Users/parno/git/FStar/bin:/Users/parno/git/everest-project/kremlin:/Users/parno/git/boogie/Binaries/:/Users/parno/git/dafny/Binaries/:/Users/parno/bin/:/usr/local/bin:/Users/parno/.rbenv/shims:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin:/Library/Frameworks/Mono.framework/Versions/Current/Commands:/Library/TeX/texbin

parno@Picasso:~$ which fstar
/Users/parno/git/FStar/bin/fstar

parno@Picasso:~$ which z3
/usr/local/bin/z3

parno@Picasso:~$ z3 -h
Z3 [version 4.5.0 - 64 bit]. (C) Copyright 2006-2016 Microsoft Corp.
...

parno@Picasso:~$ fstar Semantics.fst 
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
ApplicationName='z3', CommandLine='-version', CurrentDirectory='', Native error= Cannot find the specified file

parno@Picasso:~$ fstar --smt /usr/local/bin/z3 Semantics.fst 
Verified module: Semantics (3671 milliseconds)
All verification conditions discharged successfully
mtzguido commented 7 years ago

I've been looking at this, but can't really pinpoint a reason that could cause this. Also I couldn't reproduce it, even updating mono (so it works for me in 4.6.2 and 4.8.1).

Things to try are:

According to some F# docs, neither of those should be necessary, but...

parno commented 7 years ago

I ended up rebuilding the OCaml sources and then compiling those again. Now, FStar seems to find Z3 successfully. I'm not sure what changed, but I'm able to make progress. Thanks!

mtzguido commented 7 years ago

Right, it seems to be 'only' an F# runtime problem, but an annoying one indeed..

catalin-hritcu commented 7 years ago

@mtzguido Can still reproduce this with mono 4.8.0.495 and fsharp 4.0.1.21 on latest Arch Linux. Here is the result of trying the various things you suggested:

No change:

[hritcu@resurrected pub]$ sudo cp /home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin/z3 /usr/bin
...
[hritcu@resurrected pub]$ fstar.exe examples/hello/hello.fst
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
ApplicationName='z3', CommandLine='-version', CurrentDirectory='', Native error= Cannot find the specified file

unless changing the PATH too to just /usr/bin, in which case it starts working:

[hritcu@resurrected pub]$ export PATH=/usr/bin
[hritcu@resurrected pub]$ ./bin/fstar.exe examples/hello/hello.fst
./examples/hello/hello.fst(5,0-5,37): (Warning) Top-level let-bindings must be total; this term may have effects
Verified module: Hello (30 milliseconds)
All verification conditions discharged successfully
[hritcu@resurrected pub]$ which z3
z3 not found
[hritcu@resurrected pub]$ which z3.exe
/home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin/z3.exe
[hritcu@resurrected pub]$ ./bin/fstar.exe examples/hello/hello.fst
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
ApplicationName='z3', CommandLine='-version', CurrentDirectory='', Native error= Cannot find the specified file

I'm starting to suspect that this is some sort of PATH parsing error, so will try to minimize my current path.

catalin-hritcu commented 7 years ago

So, the following path causes F* to fail

PATH=/home/hritcu/Apps/Vampire---4.1:/home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin

but the one with only 2 dashes in Vampire---4.1 makes it work

PATH=/home/hritcu/Apps/Vampire--4.1:/home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin

Also tried to reproduce this with bryan @parno 's PATH, but didn't manage. I can of course fix this locally by just renaming the Vampire dir, but it would still be good to figure out what on earth is happening here.

catalin-hritcu commented 7 years ago

I can of course fix this locally by just renaming the Vampire dir, but it would still be good to figure out what on earth is happening here.

It's actually not so simple. I can only make this work if the path to vampire doesn't point to the actual Vampire dir. One thing I just noticed is that the Vampire dir includes a subdirectory called z3:

[hritcu@resurrected Vampire4.1]$ ls -l ~/Apps/Vampire4.1/
...
drwxr-xr-x 3 hritcu hritcu     4096 Jun 10  2016 z3

So this is not about parsing the path or anything like that, but about mistaking a directory in the PATH for an executable. Tried renaming the z3 directory in the vampire and things work again.

Wondering whether this is an F* problem or a general problem with executable lookup in F#/Mono.

mtzguido commented 7 years ago

Great detective work!

I can indeed reproduce this now and I also think it's probably a problem with F#/Mono. Will try to pin it down and maybe try to find a workaround.

catalin-hritcu commented 5 years ago

Can this still be reproduced?