Who exstinguished Alire's SPARK? ;-)

General
1

I just ran alr edit to try something with SPARK and… gps had no SPARK menu! What happened to it?

I wondered if I don’t have the gnatprove crate installed. Neither alr get nor alr toolchain -i seemed to help, and alr show gnatprove gave a very unhelpful error message.

It somehow occurred to me that alr with might work, and sure enough, within moments gnatprove was being added to a project, and SPARK showed up in the gps menu! :grin: :dark_sunglasses: :grinning: :sunglasses: :fireworks:

But… it does not show up in other projects! Apparently I have to alr with spark in every project I want to use it in.

  1. Is that what’s supposed to happen?
  2. Is this documented somewhere? I didn’t see it if so.
  3. Will it install a new gnatprove bin every time I install it, or is it just installed once, and set up in the projects where we use it?
2

Yes, at present that’s the way to bring in gnatprove into a project, as a regular dependency.

Next Alire version will have features to avoid the multiple installations of such a dependency. For the time being, you could alr get gnatprove somewhere and add its bin to your path, and I guess it will be available in GNAT even without being a dependency of your project.

1 Like
3

This document has a section:

SPARK

The SPARK formal verification tool GNATprove is available as a binary release for Windows x64-64, Linux x86-64 and macOS x86-64. To use it, simply add gnatprove as a dependency of your crate:

$ alr with gnatprove
1 Like
4

Thank you! Trouble is, I was starting from this page. I think I have seen the page you linked before, but I was unable to find it the other night.

5

I did try this, more than once:

alr get gnatprove

only to be told:

$ alr get gnatprove
error: Cannot get a release inside another alr release, stopping.

I didn’t understand the error message at the time, but now I do: I was inside an alr crate, and gnatprove is apparently considered a library in that context. Perhaps the error message could be clearer, but offhand I can’t think of a better wording.