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!
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.
- Is that what’s supposed to happen?
- Is this documented somewhere? I didn’t see it if so.
- 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?
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.
This document has a section:
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
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.
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.