Where is Sparklib?

General
1

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
2

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
3

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
4

Ok, I have an Alire project with gnatprove (13.2.1) as dependency, but I’m still stuck using SPARKlib. :frowning:

The docs say I need a sparklib.gpr extending sparklib_internal:

project SPARKlib extends "sparklib_internal" is
   for Object_Dir use "sparklib_obj";
   for Source_Dirs use SPARKlib_Internal'Source_Dirs;
   for Excluded_Source_Files use SPARKlib_Internal'Excluded_Source_Files;
end SPARKlib;

@daniel-larraz in his AoC project uses a sparklib.gpr extending sparklib_external:

project SPARKlib extends "sparklib_external" is
   for Object_Dir use "sparklib_obj";
   for Source_Dirs use SPARKlib_External'Source_Dirs;
   for Excluded_Source_Files use SPARKlib_External'Excluded_Source_Files;
end SPARKlib;

But in both cases, I get a project not found error. Is there something obvious that am I missing?

5

I’m using gnatprove 14.1.1 and gnat_native 14.2.1, in case it helps.

6

What’s the content of your GPR_PROJECT_PATH? It should contain the path to the “sparklib_external” project.

Note that this project was renamed recently to “internal”, but it’s not the case for any released gnatprove version. The online documentation is for the development version of SPARK.

7

Hm. So my question gets more stupid: Where should the “sparklib_external” project be, given that it’s bundled with gnatprove? Or do I need to provide/install it explicitly?

Sorry for this, I have a very blurry mental model of how this is supposed to work. :see_no_evil:

(I tried pointing GPR_PROJECT_PATH to the root of my project, but that doesn’t change the error. The Source_Dirs points to “src/**”.)

8

Assuming you have latest gnatprove 14.1.1 then you should only need to set GPR_PROJECT_PATH to the folder that contains sparklib_external.gpr. I don’t know which folder that would be with alire to be honest. Then it’s recommended to create your own sparklib.gpr as is documented here in the thread.

9

If I try this, I get an error during binding:

Bind
   [gprbind]      aoc2024.bexch
   [Ada]          aoc2024.ali
fatal error, run-time library not installed correctly
cannot locate file system.ads

raised TYPES.UNRECOVERABLE_ERROR : targparm.adb:168
gprbind: invocation of gnatbind failed
gprbuild: unable to bind aoc2024.adb

But I managed to upgrade both gnatprove and gnat_native to the latest version, and now it does work the with the sparklib.gpr file that @daniel-larraz uses.

Thanks a lot to both of you for helping me figure it out! :slightly_smiling_face:

10

By the way I was confused. The method I provided was OK but unnecessarily complicated. I updated my post with the “best” current method. As Fabien said earlier, in the future we want to make sparklib be standalone and not depend on a gnatprove install.

2 Likes
11

Hi, I just wanted to say that this sound great! It would make the release of the library more flexible and also its use in other programs!

Best regards,
Fer