search

ptroja / spark-navigation

Robot navigation algorithms implemented in SPARK
11 stars 4 forks source link

formal_numerics.gpr is missing #1

Open yannickmoy opened 10 years ago

yannickmoy commented 10 years ago

Hi Piotr, Project algorithm.gpr in snd/ada requires the presence of a project formal-numerics/formal_numerics.gpr which is missing from the repository. Could you add it? Great work by the way!

ptroja commented 10 years ago

This file is in the a separate repository that should be cloned into the same folder as the spark-navigation: https://github.com/ptroja/formal-numerics. The contents of the formal-numerics is independent of the navigation algorithms, so I decided to split them.

Note: For external axiomatization I needed a custom build of gnatprove. All the patches are in the "gnatprove" branch of the formal-numerics repo. Hopefully, the GNAT GPL 2014 release should work out-of-the-box, but I did not ported my code yet.

Thanks for looking, but the hard work was done by you and by your workmates! I am merely a SPARK user.