search

AdaCore / gnatstudio

GNAT Studio is a powerful and lightweight IDE for Ada and SPARK.
405 stars 53 forks source link

Cannot prove with Coq #30

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.

setton commented 6 years ago

Hello, this is not a GPS issue, more a SPARK issue. You could try asking on spark2014-discuss@lists.adacore.com or perhaps opening an issue on https://github.com/AdaCore/spark2014...

mindbound commented 6 years ago

You're right, thank you.