I wanted to try out some of the formal containers for SPARK, but I am having trouble finding the Sparklib mentioned in the Spark docs. My GNAT Studio doesn’t have a SPARK category under Help, as the SPARK manual mentions, and I usually do everything with ALR. I do see the SPARK Lemma libraries in my ALR cache of Gnatprove, but not the other libraries.
2 Likes
It’s actually packaged with the gnatprove release in Alire, but it’s not in the GPR_PROJECT_PATH so you cannot with it directly.
In the future this library will be packaged separately so it will be easier to depend on it.
3 Likes
You can grab its sources here: spark2014/include at master · AdaCore/spark2014 · GitHub
Note that, as Fabien said, this is more recent than the version of GNATprove in Alire, so some special handling (say, for SPARK.Big_Integers) won’t be available yet.
1 Like