Where is Sparklib?

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.


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.


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