search

jgalenson / piVC

The Pi verifying compiler.
GNU General Public License v3.0
4 stars 4 forks source link

pivc fails to compile .pi source code #3

Open maranp opened 6 years ago

maranp commented 6 years ago

Hi, I am trying to setup pivc on my system as part of educating myself with "The Calculus of computation".

There are two issues 1) under src/ folder, make fails with the error Error: I/O error: ../../bin/test_parser: No such file or directory If make is invoked after manually creating bin folder under piVC and the make is invoked from src/, error is no more seen and make is successful. Executables pi_gui, servers are created in bin. Then I copied yices binary (obtained by following the steps under Aptitude section of https://github.com/SRI-CSL/yices2 to obtain pre-built binaries) in the bin/ folder.

2) When I tried to compile samples/feature_demonstrations/predicates.pi by the user interface provided by bin/pi_gui, I get the following exception. Exception

Verify.Dp_server_exception("Smt_solver.SolverError(\"yices: invalid option: -e\")")

Earlier, I executed both_servers in a separate terminal and set server to 127.0.0.1 in settings menu in pi_gui window so that it connects to the server instantiated by both_servers.

Can you please help me with this?

jgalenson commented 6 years ago

Hi,

Thanks for pointing out the error in 1. I just added a commit that fixes this by ensuring that the makefiles create the bin/ directory if it doesn't exist. Tell me if you see any more problems with this.

For your second problem, it looks like you're using Yices 2. PiVC only supports Yices 1 (with experimental support for Z3 and I believe non-working support for Yices 2). See the top-level README.md for instructions on how to download Yices 1 or use Z3. Does that help?

maranp commented 6 years ago

Hi, Thanks for the quick response and fixing 1.

Reg. 2., unfortunately http://yices.csl.sri.com is not reachable. So, I could not download yices 1. However, by configuring to use z3, I could manage to get pivc working. Thanks for the help.