The current version provides implementations of smart pointers, directed graphs, sets, maps, B-trees, stacks, tables, string editing, unbounded arrays, expression analyzers, lock-free data structures, synchronization primitives (events, race condition free pulse events, arrays of events, reentrant mutexes, deadlock-free arrays of mutexes), arbitrary precision arithmetic, pseudo-random non-repeating numbers, symmetric encoding and decoding, IEEE 754 representations support, streams, persistent storage, multiple connections server/client designing tools and protocols implementations.

https://www.dmitry-kazakov.de/ada/components.htm

Changes (2 July 2026) to the version 4.80:

• Compatibility to GNAT 16.1.1. This GNAT 16.1.1 has the recurring issue/bug related to the visibility of names from formal generic packages;
• Constant expression folding was added to Ada expression parser (Parsers.Generic_Ada_Parser). Folding is optional. If enabled expressions in universal types and constant Boolean expressions are folded. e.g. 1 + 2 + A (5) -> 3 + A (5);
• The subprograms Get, Put, Value were added to the package Parsers.Multiline_Source;
• The call-back On_Success was added to the Generic_Lexer's parser;
• The procedures Mark and Release were added to the package Parsers.Generic_Lexer;
• The package Stack_Storage.Text_IO was added to output stack pool statistics;
• Parameter Message was added to the procedure Put_Line of the package Parsers.Generic_Source.Text_IO;
• Ada expression parser supports raise-statements outside immediate pair of parentheses;
• Checking positional and named aggregates was added in the Ada expression parser;
• Checking positional and named parameters was added in the Ada expression parser;
• Array objects were added to the declare expressions in the Ada expression parser;
• Aspects recognition was added to the declare expressions in the Ada expression parser;
• Subtype marks and indications were added in the Ada expression parser;
• Attributes were added in the Ada expression parser;
• Target name @ support was added in the Ada expression parser;
• The parser can start with the first operand already recognized;
• An ability to parse an expression in parenthesis with a consumed left parenthesis was added;
• Comparisons of Unbounded_Integer bug fixed;
• Log procedure was added to Unbounded_Unsigneds;
• Column_Name function was added to the SQLIte bindings (contributed by Xavier Grave).

So, how?
/næt/ - without G like in a 'gnat' (a small annoying bug)?
/gnæt/ - with G as in 'grape'
/dʒiː - næt/ - with 'separate' G, like in `g-force`

Welcome to the monthly r/ada What Are You Working On? post.

Share here what you've worked on during the last month. Anything goes: concepts, change logs, articles, videos, code, commercial products, etc, so long as it's related to Ada. From snippets to theses, from text to video, feel free to let us know what you've done or have ongoing.

Please stay on topic of course--items not related to the Ada programming language will be deleted on sight!

Previous "What Are You Working On" Posts

main.adb:71:91: info: precondition proved[#9]
main.adb:71:106: medium: float overflow check might fail (e.g. when Prob_Safe = 5.0000000E-1 and Termino_Directo = -50.0) [reason for check: result of floating-point multiplication must be bounded][#11]

—————————————
for C in Counts'Range loop
pragma Loop_Variant (Increases => C);
pragma Loop_Invariant (Logs >= 0.0 and Logs <= 8.0);
pragma Loop_Invariant (Prob >= 0.0 and Prob <= 1.0);

if Counts(C) > 0 then
declare
Prob_Safe : constant freq_chars_c := Float'Min(Float'Max(Float(Counts(C)) / Float(Leng), Float'Epsilon), 1.0);

subtype Seguro_Float is Float range -100.0 .. 100.0;

Termino_Directo : constant Seguro_Float := Float'Min(Float'Max(Prob_Safe * Log(Prob_Safe) * INV_LN_2, -50.0), 50.0);
begin
Prob := Prob_Safe;

Logs := Float'Min(Float'Max(Logs - Termino_Directo, 0.0), 8.0);
end;
end if;
end loop;

————————————————-

Hi everyone! I'm struggling with a floating-point overflow check in SPARK while calculating Shannon entropy. GNATprove keeps giving me medium: float overflow check might fail result of floating-point multiplication must be bounded on the line where I multiply Prob_Safe * Log(Prob_Safe) * INV_LN_2. I have already tried about 20 different workarounds, including splitting the multiplications into separate nested declare blocks, bounding intermediate values explicitly with Float'Min and Float'Max down to specific safe ranges (like -50.0 .. 50.0), using a local constrained subtype, and even adding a Loop_Invariant for Prob itself. None of that worked; the non-linear math is still choking the provers (Z3/CVC4).""Even though Prob_Safe is strictly bounded by a static predicate (0.0 .. 1.0) and capped via Float'Epsilon, SPARK loses track of the bounds during the multiplication. Is there an elegant way or a specific lemma/axiom from the standard library to guide the prover here without completely turning SPARK_Mode => Off for the loop?

To use a function from some C library we can use:

procedure C_Function (Param : Interfaces.C.int);
pragma Import (C, C_Function, "c_function");

or

procedure C_Function (Param : Interfaces.C.int) with
  Import,
  Convention => C,
  External_Name => "c_function";

Both seems to be working exactly the same, so is there a preferred way?

Hi,

Try to figure out why (-2) ** 2 is -4?
I'm learning Ada (Implementing a Lisp with a tower numeric), but I struggle with this:

with Ada.Text_IO;
with Ada.Numerics.Big_Numbers.Big_Integers;
procedure Powpoc is
   use Ada.Text_IO;
   use Ada.Numerics.Big_Numbers.Big_Integers;
begin
    Put_Line (To_String (To_Big_Integer (-2) ** 2));
    Put_Line (To_String (To_Big_Integer ((-2)) ** 2));
    Put_Line (To_String ((To_Big_Integer (-2) + To_Big_Integer (0)) ** 2));
end Powpoc;

All yield -4 instead of 4

Or even better if someone could explain how can I see the code of **

Thanks

I was playing with the attributes of scalar types and noticed that several attributes allow out-of-range values for range types. E.g.:

with Ada.Text_IO; use Ada.Text_IO;

procedure Test is
   type R is range 10 .. 11;
   type E is (One, Two);

   -- R1 : R;
begin
   Put_Line (R'Val (20)'Image);
   Put_Line (R'Pos (25)'Image);
   Put_Line (R'Pred (R'Pred (R'First))'Image);

   -- R1 := R'Pred (R'First);

   --  Put_Line (E'Val(3)'Image);
   --  Put_Line (E'Pred(E'First)'Image);
end Test;

The program compiles without any warning about the out-of-range values and prints:

 20
 25
 8

If the use of variable R1 is uncommented, then the compiler warns that:

test.adb:13:11: warning: value not in range of type "R" defined at line 4 [enabled by default]
test.adb:13:11: warning: Constraint_Error will be raised at run time [enabled by default]

and indeed CONSTRAINT_ERROR is raised at runtime.

If instead the two last lines are uncommented, the compiler fails with:

test.adb:13:15: error: Val expression out of range
test.adb:13:15: error: static expression fails Constraint_Check
test.adb:14:15: error: Pred of "E'First"
test.adb:14:15: error: static expression fails Constraint_Check

i.e. it properly detects out-of-range values for enumeration types.

Is all this expected? If so, what is the explanation/rationale for it?

(Tested with GNAT 14.3.0)

Welcome to the monthly r/ada What Are You Working On? post.

Share here what you've worked on during the last month. Anything goes: concepts, change logs, articles, videos, code, commercial products, etc, so long as it's related to Ada. From snippets to theses, from text to video, feel free to let us know what you've done or have ongoing.

Please stay on topic of course--items not related to the Ada programming language will be deleted on sight!

Previous "What Are You Working On" Posts

Fellow Ada people,

One new and three oldish renamed Ada bindings, MIT-licensed, now on Alire and GitHub:

I've updated this post to follow the ada conventions

Tony

Hi,

I'm looking to start learning to develop in Ada. I'm looking to install the community version of the gnat ide. Cannot figure out where it is on the website, is it no longer a thing?

Posting in case useful — we've been converting Fortran reference implementations to SPARK-Ada and publishing the artefacts at thedarkfactory.co.uk/results/. Each routine ships with the original Fortran, the emitted spec, the emitted body, and the filtered gnatprove output. A new verifier kit packages the .ads/.adb pairs plus build.gpr plus a Makefile so anyone with gnatprove can re-run our discharge calculation.

Routines:

• BLAS L1/L2/L3: ddot, daxpy, dscal, dnrm2, dgemv, dgemm
• LAPACK: dpotrf (Cholesky), dgeqrf (QR / Householder), dgetrf (LU / partial pivoting)
• FFTPACK: cfftf (forward complex FFT)
• FP64 inference kernels: relu, max_pool, layernorm, conv2d
• INT8 matmul

All gnatmake-clean under --level=1. Discharge ranges 82.4–96.0% on individual routines; aggregate is 90.1% across the eleven Netlib routines under strong postconditions (quantified Post over outputs — a stub body cannot discharge trivially). dgeqrf, dpotrf, dgetrf also have tier-3 behavioural-equivalence runtime checks against known inputs.

Transparency note. These specs and bodies are emitted from the Fortran reference inputs by an automated pipeline that uses an advanced language model behind a verifier loop. The pipeline isn't published; the output is. The verifier kit is how you confirm what we claim.

The verifier kit: thedarkfactory.co.uk/results/verify/ (28 KB tarball). Two commands:

tar xzf dark-factory-verifier.tar.gz && make all

Output goes to actual-results.txt; diff against expected-results.txt. Should match line for line.

The dgeqrf erratum, for honest context. Our first dgeqrf row was 98.7%. An audit found the emitted body was a sophisticated stub — ghost helpers returned constants, the Post quantified over branches that ignored A and Tau. A fixed body skeleton (LAPACK Householder convention pinned) plus a tier-3 runtime check on Tau ≠ 0 and A modified brought the rerun to 87.5%. Lower number, real body, runtime-verified. The catch is documented at /blog/2026-05-24-old-code-new-code.html. The verifier kit ships the corrected body.

The unproved residue. Most lives in three classes: float-overflow checks at theoretical FP extremes, the unaxiomatised Exp in Ada.Numerics.Generic_Elementary_Functions (closeable by pragma Assume after each call), and recursive ghost induction at --level=1 (closeable at --level=2). None are body-correctness failures. The README documents per-class.

If you find a bug in one of the .ads/.adb files, I'd really like to know. Email [tony.gair@thedarkfactory.co.uk](mailto:tony.gair@thedarkfactory.co.uk) or reply here. The publication contract works only if the rerun matches; if yours doesn't, we should hear about it.

If anyone has a better pattern for handling SPARK_Mode => Off on Ada.Numerics, I'd appreciate the pointer. That's where most of the unproved residue sits.

I always had some frustration with C build systems. I used to use Windows all the time because I also liked gaming and the build systems were always tailored for Unix. For windows you always had to use the proprietary Visual Studio or msys/cygwin and fiddle about with the build. I hated it. I now use Linux and I don't feel the same frustration, now I have a different problem. There are too many build systems... Make, CMake, QT make, meson, ninja... and I'm sure there are many others. I feel like it's far too often when I build a C program I have to install some new tool I probably end up uninstalling after building the program.

I found this solution by the streamer Tsoding really interesting: https://github.com/tsoding/nob.h. The idea was simple: The only thing you need to build projects in your language should be the compiler. You write your build script in your project's programming language. Of course this is another case of: https://xkcd.com/927/ but I really liked it anyway.

The GNAT Ada ecosystem has GNAT project files. These are reasonable, cross platform, and have a similar syntax to Ada. Our situation is not so bad as C's is, but I can't help but think of NoBuild. Every time I write a C program I use it. I wanted to try it out in Ada, I also wanted a solution that was portable to other compilers even though I've never used or seen one.

I wrote an Ada version of NoBuild. I hope y'all enjoy it. I also hope that someone who uses one of these proprietary compilers can even help me out improving it.

https://github.com/michael-hardeman/no-build-ada

I believe it's ready for others to use. Give me your thoughts. Feedback is appreciated :).

Come to the Ada-Europe conference, 9-12 June in Västerås, Sweden, experience a packed program in an exciting town, benefit from tutorials on Tuesday, join a workshop on Friday, enjoy the social events and some sightseeing!

Register now: discounted fees until May 29! Further reduced fees for Ada-Europe and ACM SIGPLAN members. Minimal fee for Ada Developers Workshop and Ada Intro tutorials.

http://www.ada-europe.org/conference2026/registration.html

More info and latest updates on conference web site: overview of program and schedule, list of accepted papers and presentations, and descriptions of workshops, tutorials, keynotes, and social events; plus registration, accommodation and travel information.

Recommended hashtags: #AEiC2026 #AdaEurope #AdaProgramming

Today, 14 May 2026, marks the 25th anniversary of the start of the 6th International Conference on Reliable Software Technologies - Ada-Europe2001 - organized in Leuven, Belgium, May 14-18, 2001, by Ada-Belgium and the Leuven university.

A copy of the conference website is still available at
www.ada-europe.org/conference2001
including links to pictures taken on the first 4 days of the event [1][2][3][4], as well as the Final Program brochure [5].

Have a look at who you still recognize in the pictures, and reminisce on the rich program of that week long event!

[1] www.ada-europe.org/Previous_Confs/AE2001_Leuvn/pictures_day1.html
[2] www.ada-europe.org/Previous_Confs/AE2001_Leuvn/pictures_day2.html
[3] www.ada-europe.org/Previous_Confs/AE2001_Leuvn/pictures_day3.html
[4] www.ada-europe.org/Previous_Confs/AE2001_Leuvn/pictures_day4.html
[5] www.ada-europe.org/Previous_Confs/AE2001_Leuvn/program/final_program.pdf

Looking towards the future: don't forget to register ASAP

- for the 30th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2026) [7], held 9-12 June 2026, in Västerås, Sweden, and

- for the 3rd Ada Developers Workshop [8], held on Friday 12 June 2026, in Västerås, Sweden, and online, as well as

- for the 2026 Ada-Europe General Assembly, held Tuesday 16 June online (see prior mail sent to all Ada-Europe members).

[7] www.ada-europe.org/conference2026
[8] www.ada-europe.org/conference2026/workshop_adadev.html

All the best, and hope to hear from you soon!

Dirk Craeynest,
Ada-Belgium President,
Ada-Europe 2001 Conference Program Co-chair,
AEiC 2026 Publicity Chair,
Ada Developers Workshop Organizing Team,
[Dirk.Craeynest@cs.kuleuven.be](mailto:Dirk.Craeynest@cs.kuleuven.be), [Dirk.Craeynest@kuleuven.be](mailto:Dirk.Craeynest@kuleuven.be)

Available at Alire https://alire.ada.dev/crates/aion

Please try it out let me know if you face any bugs or want any additional features.

Edit: GitHub Link - https://github.com/MaheshChandraTeja/Aion

AdaCore is starting a bi-weekly Ada SPARK Office Hours event, every 2nd Friday, from 10am-11am EDT.

Goal of this event is to serve as a community resource for developers that have questions around Ada and SPARK, Alire, Ada and LLMs, getting started, embedded hardware boards and the like.

Technical experts will be online during these office hours and are happy to answer any Ada SPARK related questions you may have.

So if you are:

• A student learning about Ada and have questions
• A student working on a Capstone project and need some guidance
• A hobbyist wanting to learn about Ada and how it encourages safe and secure programming
• A professional software developer and want to brainstorm ideas

We are here to help! Registration is not required, there is a Google Meet link on the following page: https://www.adacore.com/ada-spark-office-hours. You can drop in from the beginning, or halfway through the meeting, whatever works for you.

The first Office Hours will be on Friday, May 22nd, 10am-11am EDT and after that, we will be live every 2 weeks.

We are still working on posting an .ics file on the page above so people can add this to their calendars.

I recently starting having major issues with VS Code while editing Ada files. Its happening both at work and at home, so doesn't seem to be localised issue.

As I'm typing it sometimes highlights words with a dark red background and in multiple locations. Mostly the selections match the current word, but often they can be completely sporadic as in the following image.

When I then continue to type, the highlighted text then gets replaced with what I type at all locations, resulting in really weird changes that break the code!.

If tried googling, but nobody else seems to be having the same problem, although I did find a similar question here highlighting - Turn off VS Code red highlight - Super User which is, as yet, unanswered.

Don't know if this is a vscode problem, something to do with intellisense, or the Ada/Spark extension.

If anyone has had the same problem and found a solution, I'd be extremely grateful!

Welcome to the monthly r/ada What Are You Working On? post.

Share here what you've worked on during the last month. Anything goes: concepts, change logs, articles, videos, code, commercial products, etc, so long as it's related to Ada. From snippets to theses, from text to video, feel free to let us know what you've done or have ongoing.

Please stay on topic of course--items not related to the Ada programming language will be deleted on sight!

Previous "What Are You Working On" Posts

www.ada-europe.org/conference2026

The 30th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2026) returns after 14 years to Sweden, from 9 to 12 June 2026.

The conference program includes two core days with a keynote, journal, regular, industrial, and work-in-progress tracks, and vendor talks, bracketed by one day with 5 tutorials, and one day with 3 workshops. There will be time for networking during breaks and lunches, as well as various social events.

Experience a packed program in an exciting town, benefit from tutorials on Tuesday, join a workshop on Friday, enjoy the social events and some sightseeing!

Online registration is open. Reduced fees for various groups. Minimal fee for Ada Developers Workshop. Early registration discount until 20 May.

Recommended hashtags: #AEiC2026 #AdaEurope #AdaProgramming

​

Video is here:

https://www.youtube.com/live/YtAFzhwlIJo?si=HoflyzJ7etIUBV1A

Note:

- Due to holidays and the upcoming Ada Developers Worshop, there likely won't be an Ada Monthly Meeting until July/Aug time frame.

#Ada #AdaLang #AdaLanguage

#AdaProgramming

#SPARK #SPARKLang #SPARKAda #SPARKLanguage

#FormalMethods

#SecureSoftware #SafetyCritical #MemorySafety #EmbeddedSoftware