I am pleased to announce that AdaCL.Serial has been accepted into the Alire index as crate 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_ArrayandCharacter/String; - the familiar
Get/Put/Get_Line/Put_Lineoperations; - high-level
Expectprocedures 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
Depends on: adacl ^7.2
Licence: GPL-3.0-or-later
Project: https://adacl.sourceforge.net/
Repository: https://git.code.sf.net/p/adacl/git
Martin Krischik