# AdaCL.Serial is on Alire — and a call for SPARK eyes **URL:** \ **Category:** Releases\ **Tags:** spark, ada, alire\ **Created:** [August 27, 2026, 4:43pm UTC](https://forum.ada-lang.io/t/adacl-serial-is-on-alire-and-a-call-for-spark-eyes/4685 "2026-08-27T16:43:05Z")\ **Posts on this page:** 10\ **Page:** 1
**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:** [August 27, 2026, 4:43pm UTC](https://forum.ada-lang.io/t/adacl-serial-is-on-alire-and-a-call-for-spark-eyes/4685/1 "2026-08-27T16:43:05Z")
I am pleased to announce that **AdaCL.Serial** has been accepted into the Alire index as crate [`adacl_serial`](https://alire.ada.dev/crates/adacl_serial) (version 7.2.1). It is a compact, SPARK-friendly companion to `GNAT.Serial_Communications`. The crate contains a single package, `AdaCL.Serial_IO`. A null-record derivation turns `Serial_Port` into a proper class, so the usual operations read as methods: `Port.Get`, `Port.Put_Line`, `Port.Expect`, and so on. What it offers: - conversion helpers between `Stream_Element` / `Stream_Element_Array` and `Character` / `String`; - the familiar `Get` / `Put` / `Get_Line` / `Put_Line` operations; - high-level `Expect` procedures that discard or capture skipped text until a given sequence arrives; - full SPARK contracts. The intended use is console-style protocols on classic and modern retro calculators — SwissMicros DM-series, HP-IL emulators, and similar devices. The package is **proven to SPARK bronze**. That is a deliberate, usable baseline: the contracts are there and bronze-level verification completes. I should like to take it further. At present GNATprove **hangs** when asked for a higher assurance level, rather than finishing with unproved VCs or a clean timeout. A prover should not hang; I suspect this is a known class of tool issue rather than a defect in the contracts themselves. If you have seen the same stall, know a workaround (proof switches, splits, ghost helpers, a different prover backend, a timeout that actually fires), or can spot what in `AdaCL.Serial_IO` triggers it, I would be very grateful for a note. An application that uses the library is already in progress and will be released shortly — libraries are more convincing when something real sits on top of them. When that application is out I will also publish a short tutorial showing how the crate is used in practice. Crate: [https://alire.ada.dev/crates/adacl\_serial](https://alire.ada.dev/crates/adacl_serial) Depends on: `adacl ^7.2` Licence: GPL-3.0-or-later Project: [https://adacl.sourceforge.net/](https://adacl.sourceforge.net/) Repository: [https://sourceforge.net/p/adacl/git/ci/develop/tree/](https://sourceforge.net/p/adacl/git/ci/develop/tree/) Martin Krischik ---
**Author:** ![Avila](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/avila/32/1100_2.png) [@Avila](https://forum.ada-lang.io/u/Avila)\ **Post date:** [August 27, 2026, 4:56pm UTC](https://forum.ada-lang.io/t/adacl-serial-is-on-alire-and-a-call-for-spark-eyes/4685/2 "2026-08-27T16:56:20Z")
Hello, The link to the repository fails =\> "Looks like there’s a problem with this site. The server at [git.code.sf.net](http://git.code.sf.net) sent back an error: 404 Not Found" I already tried copying and pasting directly, but it still fails. ---
**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:** [August 27, 2026, 5:14pm UTC](https://forum.ada-lang.io/t/adacl-serial-is-on-alire-and-a-call-for-spark-eyes/4685/3 "2026-08-27T17:14:38Z")
> [@Avila](#): > > Hello, The link to the repository fails =\> Try this one: [https://sourceforge.net/p/adacl/git/ci/develop/tree/](https://sourceforge.net/p/adacl/git/ci/develop/tree/) - That is the main entry and then you can choose protocol as well. But you could also us `alr get adacl_serial` 😉 ---
**Author:** ![ksson](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/ksson/32/1082_2.png) [@ksson](https://forum.ada-lang.io/u/ksson)\ **Post date:** [September 3, 2026, 9:19am UTC](https://forum.ada-lang.io/t/adacl-serial-is-on-alire-and-a-call-for-spark-eyes/4685/4 "2026-09-03T09:19:40Z")
Hello, I can reproduce the hang, apparently if you remove the “-u ” from the gnatprove invocation, it passes. We will investigate this further. ---
**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:** [September 3, 2026, 11:26am UTC](https://forum.ada-lang.io/t/adacl-serial-is-on-alire-and-a-call-for-spark-eyes/4685/5 "2026-09-03T11:26:12Z")
> [@ksson](#): > > if you remove the “-u ” from the gnatprove invocation Thanks for looking into it but I don’t use `-u` - at least not knowingly. I use the following 4 command to test the various level: ```mak test_1: validation alr exec -P1 -- gnatprove --no-subprojects --level=1 --mode=stone --verbose cat obj/validation/gnatprove/gnatprove.out test_2: validation alr exec -P1 -- gnatprove --no-subprojects --level=2 --mode=bronze --verbose cat obj/validation/gnatprove/gnatprove.out test_3: validation alr exec -P1 -- gnatprove --no-subprojects --level=3 --mode=silver --verbose cat obj/validation/gnatprove/gnatprove.out test_4: validation alr exec -P1 -- gnatprove --no-subprojects --level=4 --mode=gold --verbose cat obj/validation/gnatprove/gnatprove.out ``` The test that is actually used by the Alire continues integration is than specified in _“adacl\_serial\_prove.gpr”_. What I noticed is that you can’t specify a level with `-no-subprojects`. Which makes Alire compatible proves using a child crate a bit more cumbersome. Regards Martin ---
**Author:** ![ksson](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/ksson/32/1082_2.png) [@ksson](https://forum.ada-lang.io/u/ksson)\ **Post date:** [September 3, 2026, 10:54pm UTC](https://forum.ada-lang.io/t/adacl-serial-is-on-alire-and-a-call-for-spark-eyes/4685/6 "2026-09-03T22:54:39Z")
> you can’t specify a level with `-no-subprojects` What do you mean by that? In any case, it’s strange as I could only ever reproduce it with `-u` or `-U`. Just to double check, you are using FSF 16? The problematic pattern is likely the generic subprogram parameter with post: ```ada generic with procedure Deleter (X : in out Pointer) is <> with Post => X = null; ``` I suggest you remove this postcondition here ---
**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:** [September 5, 2026, 2:19pm UTC](https://forum.ada-lang.io/t/adacl-serial-is-on-alire-and-a-call-for-spark-eyes/4685/7 "2026-09-05T14:19:49Z")
> [@ksson](#): > > he problematic pattern is likely the generic subprogram parameter with post: Interesting. But that generic subprogram is in the AdaCL base library and some of the code is 20 years old and not at all at the quality level of the new AdaCL\_Serial library. This is why I check with `--no-subprojects`. I’ll do have a look at it because I do want to improve the quality level of the base library. > [@ksson](#): > > What do you mean by that? When using Alire it is better to keep tests and proofs in separate nested crates, so that `aunit` and `gnatprove` do not leak into the published library crate. A prove crate then holds only dummy packages whose purpose is to drive GNATprove; the library under proof is a normal dependency of that crate. GNATprove is started on the prove crate, so that crate is the **root project**. The library is a **withed subproject**. - With `--no-subprojects`, only the root project is analysed. That is just the dummy packages, so nothing useful is proved. - Without `--no-subprojects`, GNATprove walks the whole project tree: the library **and** every project the library itself withs. Proof therefore spills into the next level of dependencies as well. What one actually wants is a single hop: prove the library that the prove crate depends on, but not that library’s own dependencies. GNATprove has no depth switch today; `--no-subprojects` is only on or off. A hypothetical `--no-subprojects=1` would mean “analyse the root project and its direct subprojects, then stop.” ---
**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:** [September 5, 2026, 2:51pm UTC](https://forum.ada-lang.io/t/adacl-serial-is-on-alire-and-a-call-for-spark-eyes/4685/8 "2026-09-05T14:51:53Z")
I also use dummy subcrates to contain my GNATprove dependencies, but you only need to use it to get the environment with GNATprove in it; you don’t need to use any dummy GPR file. For example, in my [libcrc](https://github.com/damaki/libcrc) library I have a subcrate under the `proof/` directory to hide the dependency on GNATprove. When I want to run GNATprove I point it at my main GPR file in the directory above. So the command I would use is: ```sh cd proof/ alr exec -- gnatprove -P ../libcrc.gpr -j0 ``` So in your case, where you have a command like: ```make test_1: validation alr exec -P1 -- gnatprove --no-subprojects --level=1 --mode=stone --verbose cat obj/validation/gnatprove/gnatprove.out ``` You can avoid `-P1` and pass the path to the GPR file you’re interested in: ```make test_1: validation alr exec -- gnatprove -P ../path/to/project.gpr --no-subprojects --level=1 --mode=stone --verbose cat obj/validation/gnatprove/gnatprove.out ``` ---
**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:** [September 6, 2026, 6:28pm UTC](https://forum.ada-lang.io/t/adacl-serial-is-on-alire-and-a-call-for-spark-eyes/4685/9 "2026-09-06T18:28:23Z")
Follow-up on the proof trouble. The hang was not in `adacl_serial`. GNATprove was walking into the old AdaCL base — the crate that will become `adacl_desktop`. That crate is built for programmer convenience: unbounded strings, controlled types, smart pointers. As @ksson pointed out, the smart-pointer `Deleter` contract is exactly the sort of thing SPARK will choke on. You do not get more SPARK-unfriendly than a smart pointer. For 8.0 the library will be split. `adacl` will be a small SPARK-gold core with no smart pointers and no desktop convenience layer. `adacl_serial` will depend only on that core. `adacl_desktop` will keep the old API for hosted applications and will no longer be on the proof path. Thank you to everyone who looked — and especially to @ksson for putting the finger on the smart pointer. ---
**Author:** ![ksson](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/ksson/32/1082_2.png) [@ksson](https://forum.ada-lang.io/u/ksson)\ **Post date:** [September 24, 2026, 11:22pm UTC](https://forum.ada-lang.io/t/adacl-serial-is-on-alire-and-a-call-for-spark-eyes/4685/10 "2026-09-24T23:22:39Z")
The underlying crash is fixed in gnatprove but only in the development version, so it will take a while until it lands in FSF version.