# Who exstinguished Alire's SPARK? ;-)
**URL:** https://forum.ada-lang.io/t/who-exstinguished-alires-spark/345
**Category:** General
**Tags:** spark
**Created:** [March 1, 2023, 1:31am UTC](https://forum.ada-lang.io/t/who-exstinguished-alires-spark/345 "2023-03-01T01:31:58Z")
**Posts on this page:** 5
**Page:** 1
### Author:  [@cantanima](https://forum.ada-lang.io/u/cantanima)
#### Post date: [March 1, 2023, 1:31am UTC](https://forum.ada-lang.io/t/who-exstinguished-alires-spark/345/1 "2023-03-01T01:31:59Z")
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.
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?
---
### Author:  [@mosteo](https://forum.ada-lang.io/u/mosteo)
#### Post date: [March 1, 2023, 10:08am UTC](https://forum.ada-lang.io/t/who-exstinguished-alires-spark/345/2 "2023-03-01T10:08:40Z")
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.
---
### Author:  [@Max](https://forum.ada-lang.io/u/Max)
#### Post date: [March 2, 2023, 11:08am UTC](https://forum.ada-lang.io/t/who-exstinguished-alires-spark/345/3 "2023-03-02T11:08:42Z")
[This document](https://alire.ada.dev/transition_from_gnat_community.html) 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:
>
> ```ada
> $ alr with gnatprove
>
> ```
---
### Author:  [@cantanima](https://forum.ada-lang.io/u/cantanima)
#### Post date: [March 2, 2023, 12:59pm UTC](https://forum.ada-lang.io/t/who-exstinguished-alires-spark/345/4 "2023-03-02T12:59:43Z")
Thank you! Trouble is, I was starting from [this page](https://alire.ada.dev/docs/). I think I have seen the page you linked before, but I was unable to find it the other night.
---
### Author:  [@cantanima](https://forum.ada-lang.io/u/cantanima)
#### Post date: [March 2, 2023, 1:02pm UTC](https://forum.ada-lang.io/t/who-exstinguished-alires-spark/345/5 "2023-03-02T13:02:29Z")
> [@mosteo](#):
>
> you could `alr get gnatprove` somewhere and add its `bin` to your path
I did try this, more than once:
```ada
alr get gnatprove
```
only to be told:
```ada
$ 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.