search

AdaCore / spark2014

SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
GNU General Public License v3.0
249 stars 33 forks source link

Cannot prove with Coq #3

Closed mindbound closed 6 years ago

mindbound commented 6 years ago

I'm using GNAT Community Edition 2018 on Arch Linux 4.17.4 x86_64, installed in a local folder $GNAT_HOME. When trying to run "SPARK/Prove File" and specifying the command as gnatprove -P/path/to/project.gpr -j0 --ide-progress-bar -u file.adb --prover=Coq, it fails with the error

Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
gnatprove: Could not find driver file alt_ergo
gnatprove: error during flow analysis and proof
[2018-07-14 14:20:26] process exited with status 1, elapsed time: 02.00s

which also happens when running the same command in the terminal. The alt_ergo driver is in $GNAT_HOME/libexec/spark/bin, as put there by the installer.

I have installed Coq v8.5pl3 using OPAM on OCaml 4.05.0 and it is available in $PATH. Please advise.

mindbound commented 6 years ago

I was able to "solve" the issue by simply reinstalling the entire GPS package, although I am still unable to pinpoint the cause of the original failure. I have no other Why3 installations on the system at the moment.

kanigsson commented 6 years ago

Thanks for letting us know.