procedure to run GNATprove not complete

ptroja / spark-navigation

Robot navigation algorithms implemented in SPARK

11 stars 4 forks source link

procedure to run GNATprove not complete #3

Open yannickmoy opened 10 years ago

yannickmoy commented 10 years ago

I think you should add that, prior to do proof, one should copy Why3 theory files in the SPARK installation under share/spark/theories:

cp formal-numerics/theories/* /path/to/spark/install/share/spark/theories

Currently, this is a bit hidden under gnatprove branch in the README.md, together with all instructions to build gnatprove, which are not needed anymore with SPARK GPL 2014.

ptroja commented 10 years ago

Thanks, I will update the toolchain installation guide after I get more familiar with SPARK GPL 2014. (I have just reported an issue about gnatprove and alternative provers, GNAT Tracker reference N528-016.)