# In Alire, how to use SPARKlib without all assertions enabled? **URL:** \ **Category:** General\ **Tags:** spark, alire\ **Created:** [July 27, 2026, 8:29pm UTC](https://forum.ada-lang.io/t/in-alire-how-to-use-sparklib-without-all-assertions-enabled/4595 "2026-07-27T20:29:21Z")\ **Posts on this page:** 6\ **Page:** 1
**Author:** ![pat-rogers](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/pat-rogers/32/1024_2.png) [@pat-rogers](https://forum.ada-lang.io/u/pat-rogers)\ **Post date:** [July 27, 2026, 8:29pm UTC](https://forum.ada-lang.io/t/in-alire-how-to-use-sparklib-without-all-assertions-enabled/4595/1 "2026-07-27T20:29:21Z")
I have recently published my first crate (Proven\_Components) that contains a bunch of reusable packages that I’ve written over the years and updated as Ada evolved. Most are now formally proven. Proof for one of them (sorting) requires the Multisets package from SPARKlib. Before publishing the project as a crate it depended on the SPARKlib gpr files included with gnatprove. I used gnatprove’s approach to exclude all the SPARKlib sources not in the transitive closure of Multisets. Now, as a crate, it depends on the SPARKlib crate and my client projects are having difficulties building. I understand the problem that the compiler is complaining about, but not how to address it in the context of Alire and the SPARKlib crate. My code follows the convention of not testing at run-time those conditions that were also tested via preconditions. The preconditions are functional, in other words, not just for proof. I always want my code’s preconditions executed at run-time. Along the same line, I don’t want most of the other assertions enabled, eg Ghost code and Loop\_Invariants. I never want them executed. I usually don’t want postconditions enabled, either, except when debugging. Therefore, in my various client projects I have a configurations pragma file containing a pragma Assertions\_Policy enabling preconditions (and a few others) but disabling the other assertions. In alire this leads to conflicts in ghost policies when building. Presumably one or more of the units in SPARKlib has a precondition that calls Ghost code. I can compile individual client files without the problem occurring. The problem arises when building the whole client project, because the builder tries to compile all the sources in SPARKlib, not just the ones required. The fact that it didn’t conflict outside of Alire doesn’t mean that Alire is wrong about this. The SPARKlib gpr files provided in gnatprove are convoluted, shall we say, and the gpr file in the SPARKlib crate is quite different. I may have just been lucky before switching to the SPARKlib crate. However, I assume the problem stems from the fact that SPARKlib.gpr in the crate applies “-gnata” unilaterally now, unlike the SPARKLib gpr files in gnatprove. So, bottom line: how can I use SPARKlib in Alire in the way that, IMO, it should be possible to use it? ---
**Author:** ![krischik](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/krischik/32/420_2.png) [@krischik](https://forum.ada-lang.io/u/krischik)\ **Post date:** [July 28, 2026, 7:56am UTC](https://forum.ada-lang.io/t/in-alire-how-to-use-sparklib-without-all-assertions-enabled/4595/2 "2026-07-28T07:56:43Z")
Alire supports three variants: release, debug and validation.The way I do it is to activate all checks in in validation but not in release. That way users of the libraries aren’t slowed down by the checks. More importantly I use separate prove crates so there is no dependency on SPARK for the end user. Which is also considered best practice and the Alire moderators will question crates with gnatprove dependencies. See [How to Set Up Unit Tests and SPARK Proofs](https://adacl.sourceforge.net/setup-prove_and_test/) for details. ---
**Author:** ![damaki](https://forum.ada-lang.io/letter_avatar_proxy/v4/letter/d/3bc359/32.png) [@damaki](https://forum.ada-lang.io/u/damaki)\ **Post date:** [July 28, 2026, 8:46am UTC](https://forum.ada-lang.io/t/in-alire-how-to-use-sparklib-without-all-assertions-enabled/4595/3 "2026-07-28T08:46:55Z")
> [@pat-rogers](#): > > However, I assume the problem stems from the fact that SPARKlib.gpr in the crate applies “-gnata” unilaterally now, unlike the SPARKLib gpr files in gnatprove. SPARKlib 15.1.0 did apply `-gnata` unilaterally, but the recently released SPARKlib 16.1.0 makes this configurable via the `SPARKLIB_BUILD` GPR external variable. This variable accepts three values: - `"Production"` (default) sets `-O2 -gnatn` - `"Assertions"` sets `-O2 -gnatn -gnata -g` - `"Debug"` sets `-Og -g` This can be set in an `alire.toml` with: ```toml [gpr-set-externals] SPARKLIB_BUILD = "Assertions" ``` Also, GNAT, GNATprove, and SPARKlib version 16 support [Assertion Levels](https://docs.adacore.com/spark2014-docs/html/ug/en/source/specification_features.html#assertion-levels-l2212), which can be used selectively enable different kinds of assertions. SPARKlib 16 defines three assertion levels: - `SPARKlib_Defensive` is used for preconditions in SPARKlib. - `SPARKlib_Logic` is used for the ghost code that models the formal containers. - `SPARKlib_Full` is used for postconditions in SPARKlib. This one depends on level `Static` so it is never enabled at run-time. So if you want to enable precondition checks in SPARKlib, which keeping other assertions in model functions turned off you can use: ```ada pragma Assertion_Policy (SPARKlib_Defensive => Check); pragma Assertion_Policy (SPARKlib_Logic => Ignore); ``` You can also define your own assertion levels if you want to have more control over which assertions/contracts are executed in your code. Hopefully this helps with solving your problem. ---
**Author:** ![pat-rogers](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/pat-rogers/32/1024_2.png) [@pat-rogers](https://forum.ada-lang.io/u/pat-rogers)\ **Post date:** [July 28, 2026, 3:31pm UTC](https://forum.ada-lang.io/t/in-alire-how-to-use-sparklib-without-all-assertions-enabled/4595/4 "2026-07-28T15:31:11Z")
Thanks, I’ll take a look! ---
**Author:** ![pat-rogers](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/pat-rogers/32/1024_2.png) [@pat-rogers](https://forum.ada-lang.io/u/pat-rogers)\ **Post date:** [July 28, 2026, 3:33pm UTC](https://forum.ada-lang.io/t/in-alire-how-to-use-sparklib-without-all-assertions-enabled/4595/5 "2026-07-28T15:33:52Z")
Those changes to SPARKlib sound like a considerable improvement indeed. Unfortunately my immediate client project requires a cross-compiler, and if I am correct, there is no currently available gnat 16 cross-compiler. Thanks for this! I have something to look forward to using in the future anyway. ---
**Author:** ![damaki](https://forum.ada-lang.io/letter_avatar_proxy/v4/letter/d/3bc359/32.png) [@damaki](https://forum.ada-lang.io/u/damaki)\ **Post date:** [July 29, 2026, 12:09pm UTC](https://forum.ada-lang.io/t/in-alire-how-to-use-sparklib-without-all-assertions-enabled/4595/6 "2026-07-29T12:09:16Z")
> [@pat-rogers](#): > > Unfortunately my immediate client project requires a cross-compiler, and if I am correct, there is no currently available gnat 16 cross-compiler. Indeed, cross compilers for GNAT FSF 16 are not available (yet). Note that if you’re working on an bare-board project with a light or light-tasking runtime, then you might also find it useful to know that SPARKlib 16 also provides the `SPARKLIB_MODE` GPR external variable to choose between the `"light"` and `"full"` versions of SPARKlib. I’m sure you’re aware of this Pat, but for the benefit of others reading this post SPARKlib has two versions: a “full” version which provides all components in SPARKlib (including unbounded containers whose implementations use of finalization and heap allocated memory), and a “light” version which provides a subset of features that are compatible with the “light” GNAT runtime profile (so no things that use heap allocation or finalization). So those that developing programs for bare-board targets can still use the SPARKlib 16 crate with `SPARKLIB_MODE = "light"` in their `alire.toml`.