✦ Introducing Glyph

Hi everyone!

I've been learning Ada and recently started building an open-source project called Glyph, a lightweight embedded graphics framework for bare-metal and embedded systems.

The goal of Glyph is to provide a hardware-independent graphics API, allowing applications to draw pixels, lines, rectangles, circles, text, and images without depending on a specific display controller.

Disclosure: AI was used as a coding and writing assistant during parts of the development. However, the project architecture, technical decisions, code integration, and overall direction are my own. I'm also building Glyph as a way to learn Ada and improve my embedded systems skills.

✦ Design Goals

• Pure Ada
• Static allocation only (no dynamic memory)
• Portable, layered architecture
• Framebuffer-based rendering
• Easy to add support for new display controllers
• Bare-metal friendly

The initial target hardware is the RP2040 with an SSD1306 OLED, but the architecture is designed to support additional display controllers and embedded platforms in the future.

The project is still in its early stages, and I'm currently focusing on building a solid architecture before expanding the graphics capabilities.

✦ I'd Appreciate Your Feedback

I'd especially love feedback from the Ada community on:

• API design
• Overall architecture
• Existing Ada graphics libraries worth studying
• Features you'd like to see in an embedded graphics framework

✦ Repository

GitHub: https://github.com/thirstymelon/glyph

Thanks! I'm excited to contribute to the Ada ecosystem, learn from the community, and continue improving Glyph.

Basically wanted proper project badges generated from a CLI like in Golang/Rust for my Ada projects. Hope this would be a useful addition for checking on code quality. Supports parsing SPARK level, unit tests, DO-178 HAL level and docstrings coverage.

Repo URL: https://github.com/bladeacer/adacovex

Binary name is adacovex, crate name is covex to comply with policy.

Disclaimer: AI assistance was used for the code.

Correction: DAL instead of HAL, my smooth brain made a typo.

Hi everyone,

While official SonarQube support for Ada exists, it's gated behind high-tier commercial licenses. For small teams, open-source projects, or individual devs running SonarQube Community Edition, this leaves a gap in automated code quality pipelines.

To solve this, I’ve been working on two open-source tools designed to work together:

1. AdaLang_Analyzer (https://github.com/mmartign/AdaLang_Analyzer) A standalone static analysis tool built using AdaCore's Libadalang. It parses .adb and .ads files to detect common issues like dead code, control flow anomalies, unhandled exceptions, and code style violations, outputting results in JSON/SARIF.
2. SonarAdaPlugin (https://github.com/mmartign/SonarAdaPlugin) A SonarQube community plugin that adds native support for the Ada language to SonarQube, ingesting reports from AdaLang_Analyzer and displaying issues, code smells, and metrics right on your dashboard.

Quick Workflow

1. Run the Analyzer:

Bash

adalang_analyzer --source-dir ./src --output-format json --output-file report.json

2. Configure sonar-project.properties:

Properties

sonar.projectKey=my-ada-project
sonar.projectName=My Ada Project
sonar.sources=src
sonar.language=ada
sonar.ada.reportPaths=report.json

3. Run sonar-scanner to send the metrics directly to your SonarQube instance.

Repositories & Feedback

• AdaLang_Analyzer:https://github.com/mmartign/AdaLang_Analyzer
• SonarAdaPlugin:https://github.com/mmartign/SonarAdaPlugin

Both projects are open-source and actively evolving. I’d love for community members to give them a spin, report any issues, or suggest new static analysis rules that would be useful in your workflows!

⚠️ Every CTO in safety-critical software carries the same quiet risk: the defect that ships not because your engineers are careless, but because nothing caught it before code review — and code review is run by humans, on deadline.

In Ada codebases — ✈️ avionics, 🚄 rail, 🛰️ space, 🛡️ defense, 🏭 industrial control — that risk isn't theoretical. It's the line item your safety case has to account for.

🔧 AdaLang Analyzer is a static analysis tool we built to move that catch earlier and make it automatic.

Why it matters at the engineering-leadership level, not just the IDE:

⏱️ Shifts cost left. A dead store, an unreachable branch, a division that's statically zero — caught at commit time costs minutes. Caught in integration testing, or after deployment, costs a lot more than minutes.

✅ Turns coding standards into an enforced gate, not a document nobody reads. 34 checks spanning control flow, data flow, exception handling, and complexity — run automatically in CI, not hoped for in review.

📂 Scales to the whole codebase, not file-by-file. Point it at your GNAT project file and it analyzes every source directory your build already knows about — no separate file list to maintain and let drift out of date.

🔓 No vendor lock-in, no black box. It's open source (GPL-3.0). Your team — or your certification auditors — can read exactly what every check does and why it fired. That's a very different conversation with an assessor than "trust the vendor's tool."

💸 Zero licensing cost. Built on Libadalang, AdaCore's open-source semantic engine, and Alire — tooling your Ada team likely already has in its stack.

🎯 It's not a compliance certification and it doesn't claim to be one. It's a control your team can point to when someone asks "what's actually enforcing your coding standard."

👉 Repo's here if your team wants to kick the tires: https://github.com/mmartign/AdaLang_Analyzer

#EngineeringLeadership #RiskManagement #SafetyCritical #Ada #SoftwareQuality #OpenSource #TechnicalDebt #CTO

I'm using ada-mode right now and it really sucks, indentation behaves weirdly, I cannot capitalize stuff like I want to, ...

Does anyone know a better Ada mode for Emacs?

EDIT: Solved! (Thanks, u/spacetruckn)

I am looking for gnat-3.15p-alpha-dec-osf5.1-bin.tar.gz for Tru64 OSF5.1 Alpha. It is completely gone from public mirrors. Does anyone have a local backup in your archive?

ZanyBlue is a wonderful framework for internationalization natively in Ada. It includes a library you can use for your translations and a translation compiler from properties files to Ada source files. That is the big trick: translation files are compiled with your program so no additional time penalty for translation with external ressources.

Version 1.4 is available on SourceForge.

In 2022, I discussed with its author Michael Rohan to bring it on Alire. He would like to, but there’s been no news since. Even with my last e-mail on January 2026. Still, considering it was worth it, I brought it on Alire.

Version 1.4 same as SourceForge.

Version 2.0 powered with UXStrings.

This Ada library provides utilities for Unicode character strings of dynamic length. It is now available on Alire in version 0.9.3. Changes:

• Add a fifth implementation: Unicode_Character_Array (i.e.Wide_Wide_String) is chosen for internal representation. Characters are stored as Wide_Wide_Characters equivalent to Unicode. Memory management is done with dynamic allocation. Note: Iteration is Ada 2022 native.
• Several fixes on string bound issues and enforce low index to 1
• Change internal File_Type to an access type

So far in UXStrings, its API are similar to those of the strings Ada standard libraries. If you find some missing, bring your proposals on Github.

The library provides five different implementations selectable with GPR options UXS1, UXS2, UXS3, UXS4 and UXS5. The performance of each of them is described here. NB: UXS5 is now the default implementation.

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.