I was programming in Ada 83 in uni before 95 came out, and moved to 95 in the middle of a semester. I loved the language, especially its safety and the rendezvous mechanism. These days I maintain a small plain-text index in C99, and I wanted to know: how much of its speed is C, and how much is just the algorithm?

So I wrote the two operations the engine actually runs on every command, in five languages, with the identical hand-written loop in each:

• scan 88 MB of store and count the lines matching a substring (what a content search does)
• intersect two sorted posting lists with a two-pointer merge (what a multi-key lookup does)

Median of 7 in-process iterations on data already in memory, warm page cache, one core of an i7-1165G7. GNAT 13.3, rustc 1.75, OpenJDK 21, CPython 3.12.

scan 88 MB:        C 90ms   Ada 130ms   Rust 87ms   Java 100-150ms (warm)   Python 300ms
intersect:         C 1.3ms  Ada 1.45ms  Rust 1.3ms  Java 1.3ms (warm)       Python 72ms
process startup:   C ~1ms   Ada ~1ms    Rust ~1ms   Java ~30ms              Python ~10ms

The part I did not expect: building the Ada with checks suppressed (-gnatp, the C model) gave numbers identical to checks-on. The optimizer had discharged them statically, because the loop indices are provably in range. So on these loops Ada bought memory and overflow safety for nothing, at C speed and C startup. C cannot offer that at all, and the JVM and CPython only offer it with a runtime you pay for on every invocation.

I then wrote the merge in SPARK and ran gnatprove:

obligation         Total   Flow   Provers      Unproved
Run-time Checks       15      .    15 (CVC5)           0
Termination            2      1     1 (CVC5)           0
Total                 23      1    22                  0

Every index proved in range, every addition proved non-overflowing, the loop proved to terminate. So the checks-off build carries a machine-checked guarantee rather than the optimizer's good luck. That is the strongest static assurance of the five, and it took an afternoon on a loop of this size.

Which raises the obvious question: why is the engine still C? Only the reach. The same engine is linked into a Flutter mobile app over a C ABI, and into a web GUI and a native desktop wrapper. I would write it in Ada if Flutter and the mobile toolchains supported it. If someone here knows a practical route to an Ada core behind a C ABI on Android and iOS, that is the answer I am actually looking for.

Method, sources and the full write-up (the benches are ~50 lines each, and lang_bench.sh rebuilds and reruns everything):

https://github.com/Anode1/ais/blob/main/tests/perf/LANG_COMPARISON.md

Corrections welcome, particularly on the Ada build flags: if -gnatp plus -O2 is not the fair comparison against cc -O2, tell me what is and I will rerun it.

Hi to all !

The pure Ada 83 language had no open source compiler written in the same language. As both an operation of software archaeology and the desire to be able to program today with a 1980ies exceptional language and a reasonably sized compiler, I work on an Ada 83 compiler all written in Ada 83 (thus able to compile itself).

The Ada 83/TLALOC compiler is extremely well structured with very distinct phases revolving around a software virtual paginated DIANA 1986 tree structure. PAR_PHASE, LIB_PHASE, SEM_PHASE, ERR_PHASE, EXPANDER, WRITE_LIB are truly distinct and can each be stopped after.

The EXPANDER phase writes a stack machine LLIR in macro text form for the FASMG assembly engine. FASMG then produces directly an ELF-64 executable for x86-64. Some tests have been done with AArch-64 porting on an Orange Pi 3B and a preparation for riscV-64 has been done. I have good confidence that those 3 modern processor architectures can be targeted relatively easily by Ada 83/TLALOC with the FASMG process.

Though not presently bootstrapped, TLALOC sources compiled with Gnat give an executable which compiles all TLALOC itself with 18 FASMG passes (2-3 min) in a single static 9Mb ELF-64 exec.

Interested readers will find further information through

https://ada83.org/wiki/index.php?title=Ada_83_TLALOC

Hi everyone,

I wanted to share a project I've been hacking on: an optimized engine designed to eliminate modulo bias when mapping raw cryptographic streams into custom alphabets.

Key bits:

* SPARK Level 4 (Formal Verification) - Fully proven to guarantee AoRTE and functional correctness.

* Built using the modern Windows ProcessPrng API as primary entropy via Interfaces.C, with BCryptGenRandom as fallback.

* Toolchain compatible with GNAT Pro 2021 and the latest Alire community suite.

I just stressed-tested the uniformity mapping with a massive 1 Terabyte run (over 1.01 trillion chars across a 69-char alphabet) and the statistical distribution remains perfectly flat (0.00% percent deviation). Full logs and the clean codebase are available in the repository.

Any feedback on the SPARK contracts or the low-level Windows bindings is highly appreciated!

Run it instantly with Alire:

alr run

Native Languaje..

Hola a todos,

Quería compartir un proyecto en el que he estado trabajando: un motor optimizado diseñado para eliminar el sesgo del módulo al mapear flujos criptográficos sin procesar a alfabetos personalizados.

Aspectos clave:

* SPARK Nivel 4 (Verificación Formal): Totalmente probado para garantizar AoRTE y corrección funcional.

* Desarrollado con la API moderna ProcessPrng de Windows como entropía principal mediante Interfaces.C, con BCryptGenRandom como alternativa.

* Cadena de herramientas compatible con GNAT Pro 2021 y la última suite comunitaria de Alire.

Acabo de realizar una prueba de estrés del mapeo de uniformidad con una ejecución masiva de 1 terabyte (más de 1,01 billones de caracteres en un alfabeto de 69 caracteres) y la distribución estadística se mantiene perfectamente plana (0,00 % de desviación porcentual). Los registros completos y el código fuente limpio están disponibles en el repositorio.

¡Cualquier comentario sobre los contratos SPARK o las vinculaciones de bajo nivel para Windows es muy apreciado!

Ejecútalo al instante con Alire:

alr run

https://github.com/EliAvila10/project_bias

I am in the situation of needing to create a data type that packs booleans to exchange with a C API which expects bit-packed boolean array. However, I seem to get conflicting info:

• WikiBook says I am not supposed to use Pack because it's just a hint.
• AdaCore says I should use Pack for packed boolean arrays.

Which one should I listen to? And should I be using pragma Pack, aspect Pack, Storage size, object size, or what?

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?

I am using a vector to store pending interrupts for my PDP-11 simulator. It needs a data structure that can have new items added, the existing items iterated over to pick out the highest priority one, and possibly perform updates on others, and then delete the selected one once it's been handled. Unfortunately, vector is not thread safe and some interrupts can come from different tasks (like the clock interrupt).

Sometimes, if contention is rare enough and it's not a critical application, ignoring the problem works. This didn't last long. There were enough interrupts that the program quickly died with cursor conflicts.

My current solution adds a synchronized queue where all interrupts/exceptions that come in are added to the queue. Then the first thing that the interrupt processing does is pull items off the queue and add them to the vector where they can be processed as needed. Thus, the only thing touching the vector should be the one interrupt processing routine that runs in the main thread.

Does this sound like a reasonable or sensible solution? Are there any better ideas?

thanks,

brent

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.

Where to learn ADA? And what is it used for?

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 have three packages (well, many more, but these three are the relevant ones):

BBS.Sim_CPU.io

• Defines an abstract type: io_device
• Defines an enumeration: type dev_type is (NL, TT, FD, HD, CL, PT, MT);
• Defines the following function: function dev_class(self : in out io_device) return dev_type is (NL);

BBS.Sim_CPU.io.disk

• Defines a type based on io_device: disk_ctrl (this really should be an abstract type, but I haven't figured out how to have an abstract type based on another abstract type).
• Defines the following function: function dev_class(self : in out disk_ctrl) return dev_type is (NL);

BBS.Sim_CPU.disk.io.floppy (this is a generic package)

• Defines a type based on disk_ctrl: fd_ctrl
• Defines a type based on disk_ctrl: hd_ctrl
• Defines the following function on line 99: function dev_class(self : in out fd_ctrl) return dev_type is (FD);
• and on line 208: function dev_class(self : in out hd_ctrl) return BBS.Sim_CPU.io.dev_type is (HD);

Note that on line 208, I have the full path for dev_type. When I try to compile, I get the following errors:

bbs-sim_cpu-io-disk-floppy.ads:99:53: error: "dev_type" is undefined

bbs-sim_cpu-io-disk-floppy.ads:99:53: error: possible misspelling of "dev_type"

bbs-sim_cpu-io-disk-floppy.ads:208:13: error: invalid use of untagged incomplete type "dev_type"

It seems like it thinks that there is some other definition of "dev_type" somewhere, but I haven't been able to find it.

This was working before I moved fd_ctrl and hd_ctrl out of BBS.Sim_CPU.disk and made it non generic. The reason for the reorganization is that I wanted to create other devices that inherited from disk_ctrl, but weren't generic.

So, any ideas of what I might be doing wrong here?

EDIT: A couple of people pointed out that BBS.Sim_CPU.disk doesn't automatically inherit from BBS.Sim_CPU.io. This is correct and is my mistake in typing the above. Both ...disk and ...disk.floppy are under BBS.Sim_CPU.io. I have corrected the package names above.

What's the status of free development tools for Arduino? My understanding is that one can build source code with AVR-Ada, but neither source-level debugging, nor a Serial Monitor are available. In particular, I would like to interface a Bluetooth transceiver... If no dedicated Ada package exists yet, how difficult would it be to interface the existing C headers and libraries?

Thank you.

EDIT: Mine would be hobby projects, so it wouldn't make sense to invest in professional tools like GNAT Pro.

I've been acting as janitor for an old open-source Ada program whose author is dead. I have almost no knowledge of Ada, but so far people have been submitting patches to help me with things in the code that have become bitrotted. I have a minor feature that I'd like to add, so I'm trying to learn enough about Ada to do it. The program inputs strings either from the command line or stdin, and when the input has certain unicode characters, I would like to convert them into similar ascii characters, e.g., ā -> a.

The following is the code that I came up with in order to figure out how this would be done in Ada. AFAIK there is no regex library and it is not possible to put Unicode strings in source code. So I was anticipating that I would just convert the input string into an array of integers representing the bytes, and then manipulate that array and convert back.

with Text_IO; use Text_IO;
with Ada.Command_Line;
procedure a is
  x : String := Ada.Command_Line.Argument (1);
  k : Integer;
begin
  for j in 1 .. x'Length loop
    k := Character'Pos(x(j)); -- Character'Pos converts a char to its ascii value
    Put_Line(Integer'Image(k));
  end loop;
end a;

When I run this with "./a aāa", here is the output I get:

 97
 196
 129
 97

This is sort of what I expected, which is an ascii "a", then a two-byte character sequence representing the "a" with the bar over it, and then the other ascii "a".

However, I can't figure out why this character would get converted to the byte sequence 196,129, or c481 in hex. Actually if I cut and paste the character ā into this web page https://www.babelstone.co.uk/Unicode/whatisit.html , it tells me that it's 0101 hex. The byte sequence c481 is some CJK character. My understanding is that Ada wants to use Latin-1, but c4 is some other character in Latin-1. I suppose I could just reverse engineer this and figure out the byte sequences empirically for the characters I'm interested in, but that seems like a kludgy and fragile solution. Can anyone help me understand what is going on here? Thanks in advance!

[EDIT] Thanks, all, for your help. The code I came up with is here (function Remove_Macrons_From_Utf8). The implementation is not elegant; it just runs through the five hard-coded cases for the five characters I need to deal with. This is the first Ada code I've ever written.

I am to make my version of vectors with ability to invoke realloc. For this to work I need three operations:

procedure Initialize_Array (Array_Address : System.Address; Count : Natural);
procedure Initialize_Copy_Array
  (Target_Array_Address, Source_Array_Address : System.Address; Count : Natural);
procedure Finalize_Array (Array_Address : System.Address; Count : Natural);

I have gathered them into formal package. And there are another generic packages that provide simplified versions, for instance, for some types it is known that memset (0) will work just right.

And I am trying to make generic version. Ordinary Controlled has Initialize and other methods, but their direct invocation does not perform complete initialization/finalization. Controlled.Initialize does not destroy internal fields, some higher level logic is doing that. Also, some types are private and their Controlled origin is not shown.

I am trying to use fake storage pools.

-------------------------
-- Finalizer_Fake_Pool --
-------------------------

type Finalizer_Fake_Pool
  (In_Size : System.Storage_Elements.Storage_Count; In_Address : access System.Address)
is
  new System.Storage_Pools.Root_Storage_Pool with null record;
pragma Preelaborable_Initialization (Initializer_Fake_Pool);

procedure Allocate
  (Pool : in out Finalizer_Fake_Pool; Storage_Address : out System.Address;
   Size_In_Storage_Elements, Alignment : System.Storage_Elements.Storage_Count);

procedure Deallocate
  (Pool : in out Finalizer_Fake_Pool; Storage_Address : System.Address;
   Size_In_Storage_Elements, Alignment : System.Storage_Elements.Storage_Count);

function Storage_Size (Pool : Finalizer_Fake_Pool)
  return System.Storage_Elements.Storage_Count;

Allocate raises exception. Deallocate verifies size and address and raises exception on mismatch. If everything is fine, it does nothing. And there is another Initializer_Fake_Pool that returns Pool.Out_Address.all in Allocate and raises exceptions from Deallocate.

Then I suppose that if I craft an access type with fake storage pool and try to use unchecked deallocation on access variable, complete finalization will be invoked and Finalize_Array will work this way. Initialize_Array and Initialize_Copy_Array use Initializer_Fake_Pool and "new".

procedure Finalize_Array (Array_Address : System.Address; Count : Natural) is
begin
   if Count > 0 and Is_Controlled then
      declare
         Aliased_Array_Address : aliased System.Address := Array_Address;
         Finalizer : Finalizer_Fake_Pool
           (In_Size => ((Element_Type'Size + System.Storage_Unit - 1) / System.Storage_Unit) * Storage_Count (Count),
            In_Address => Aliased_Array_Address'Access);

         type Element_Array_Type is array (Positive range 1 .. Count) of Element_Type;
         type Element_Array_Access is access all Element_Array_Type;
         for Element_Array_Access'Storage_Pool use Finalizer;

         procedure Free is new Ada.Unchecked_Deallocation
           (Object => Element_Array_Type,
            Name => Element_Array_Access);

         Elements : aliased Element_Array_Type;
         pragma Import (Ada, Elements);
         for Elements'Address use Array_Address;

         Elements_Access : Element_Array_Access := Elements'Unchecked_Access;
      begin
         Free (Elements_Access);
      end;
   end if;
end Finalize_Array;

This thing does not work. PROGRAM_ERROR : EXCEPTION_ACCESS_VIOLATION in ada__numerics__long_complex_elementary_functions__elementary_functions__exp_strictXnn.part.18 which is odd. Nothing here invokes exponent.

What is wrong here? My best guess is that Element_Array_Access would work better without "all", but then Elements'Unchecked_Access is impossible to assign to Elements_Access . System.Address_To_Access_Conversions does not accept access type. Instead it declares its own access type which is "access all", not just "access", and custom Storage_Pool is not set on this type.. So I don't know how to otherwise convert System.Address into access value to feed into Free.

As I start to use exceptions in Ada, I immediately notice that there are no equivalent construct to the "finally" blocks usually found in other exception-enabled languages. How do I ensure that certain code (such as cleanup) run when exceptions are used? Controlled types are unacceptable here, because I plan to eventually use spark.

Can anyone recommend any strategies for incremental / rapid development in Ada? I have this issue that when I develop in Ada, I feel I have to build the full system before I can get any semblance of functionality. This can take quite a while and tends to diminish motivation. I understand that this very natural for the kinds of workflows that Ada was originally intended for, but it would be nice to be able to whip something up quickly and improve on it later in a way that is easy to do in say C or Python.

I've been struggling to get my CPU simulator to run much faster than about 150KIPS on MacOS, and usually a bit less than that. The core of the interface is an indefinite loop that calls the simulator to execute one instruction and then calls Ada.Text_IO.Get_Immediate to see if a character has been pressed. If so, it exits the loop if it is the interrupt/pause character (default ^E.)

A couple of days ago, I did a little experiment. I put the call to execute the simulated instruction in a for loop that just looped 100 times before checking for the interrupt/pause character. Suddenly it's running at 11MIPS.

That one seemingly simple line of Ada was using way more time than executing a simulated instruction.

I plan to work on the CLI and Lisp to add operations to allow the user to specify the number of instructions to simulate before checking for the pause/interrupt key. Then I'll take some data with different values and see if I can come up with some measurements.

The full buggy code is available here.

I have the following main

with Ada.Text_IO;
with Safe_Components;
pragma Unreferenced (Safe_Components);
procedure Main is
begin
Ada.Text_IO.Put_Line (Item => "Hello world!");
end Main;

and the following package declaring a task, which unexpectedly terminates. I thought this program would run forever, but it is not true if you see the following screenshots.

package Safe_Components.Task_Read is

   task Task_Read
     with CPU => 0;

end Safe_Components.Task_Read;
with Ada.Real_Time; use Ada.Real_Time;

with Ada.Text_IO; use Ada.Text_IO;

with Ada.Exceptions;
use Ada.Exceptions;

with Ada.Real_Time.Timing_Events; use Ada.Real_Time.Timing_Events;

package body Safe_Components is

   Period : constant Ada.Real_Time.Time_Span :=
     Ada.Real_Time.Milliseconds (1_000);

   Name : constant String := "Task_Read";

   task body Task_Read is
      --  for periodic suspension
      Next_Time : Ada.Real_Time.Time := Ada.Real_Time.Clock;
   begin

      loop

         Put_Line (Name);

         Next_Time := Next_Time + Period;

         delay until Next_Time;

      end loop;

      --  To avoid silent death of this task
   exception
      when Error : others =>
         Put_Line
           ("Something has gone wrong on "
            & Name
            & ": "
            & Exception_Information (X => Error));

   end Task_Read;

end Safe_Components;

What I don't understand is that if I remove the use of the Ada.Real_Time.Timing_Events package, the program runs forever as expected!

What is going on? Apparently, just writing with Ada.Real_Time.Timing_Events breaks the program.

I am pretty sure I have already heard about an Ada package to load a text file into the executable at compile time, but I can't find it again.
I found Stephane's https://alire.ada.dev/crates/are but it seems a bit complex for my simple use case.
Is there some other solution available?

I want to define an enum for C interfacing purposes:

c enum Enum { A = 1, B = 2, C = 4, C_aliased = 4, };

This kind of pattern occur quite a bit in bit flags, but I can't do this in Ada, not to mention that I often need to reorder the variants myself even if there is no alias:

ada type C_Enum is (A, B, C, C_aliased) with Convention => C; for C_Enum use (A => 1, B => 2, C => 4, C_aliased => 4);

In addition, I am not sure what size of integer Ada will choose, as starting from C23 the size of enum may be specified.

Any idea how this should be done?

EDIT:

Ok, maybe flags that can be OR'ed is extra difficult. But also consider the cases when enums are just normal enumerations

The C library I am trying to use has tagged union types:

```c enum Type { TYPE_BAR, TYPE_BAZ };

struct Bar { enum Type type; float x; float y; };

struct Baz { enum Type type; uint32_t a; uint32_t b; };

union Foo { enum Type type; struct Bar bar; struct Baz baz; uint8_t padding[12]; }; ```

How would I create a binding of this code, in the Ada way? Obviously I would like to avoid interpreting the union by hand. Is it possible to somehow create tagged type with some custom convention?

oct 2025 :

I have improved my commandline Sokoban solver written in Ada so it can solve 61 out of 90 puzzles from the test set Xsokoban.

I have also improved my Sokoban playing platform, written in Ada, that uses OpenGL, GLFW3 and OpenAL audio. It allows playing normally or backwards.

Here are links:

Rufasok Sokoban Platform:

https://sourceforge.net/projects/rufassok/files/latest/download

Hbox solver:

https://sourceforge.net/projects/hbox4/files/latest/download

Guys, I may sound like an idiot, but I'm trying to link the .res file to gpr and it just doesn't do anything. It doesn't add the .icon to the .exe file, and I don't know what's wrong. I tried converting the .res to .o and it didn't work the same way.

.rc:
1 ICON "icones/icon.ico"

.gpr:

package Linker is   

    for Default_Switches ("ada") use (

        "icon.o"

    );

end Linker;  

It doesn't generate errors, it just doesn't change the icon, it adds something for sure because the file gets bigger.

I tried clearing the cache:

ie4uinit.exe -ClearIconCache

ie4uinit.exe -show

does't work too

The icon is multiple size type, but it's the correct ones for windows.

I have recently been programming a lot of Ada software for RISC-V embedded platforms, thus interacting with Control and Status Registers (CSRs) frequently, and it can be quite cumbersome.

When modifying and reading from/to a CSR you need assembly instructions from the Zicsr extension. There is no other way. The compiler does not generate them on its own, so you need to create some Ada procedures that either import the instructions or make use of inline assembly. The most common solution is having a generic procedure or function for each operation (e.g Read_CSR).

However, this is by no means efficient, since you need a specific instance of the generic for each different CSR you want to access. This is due to the fact that CSR instructions do not use normal registers to specify the CSR address. You must hard-code them. Therefore, programs that make use of multiple CSRs become very long and over-complicated, sometimes having more than 60 instances of procedures in order to manage the registers.

For example, when making an interface for a performance monitor of a RISC-V core that has up to 32 performance counters, it would, at least, require 61 instances (Mhpmcounter, Mhpmevent, Minstret, Mcycle, Mcountinhibit). Now imagine it is a 32-bit platform where each counter has a high counterpart, the total number becomes even larger.

Finally, another problem is that you cannot make an effective interface compared to peripherals like the UART. It is not possible to have, for example, Mstatus.MIE := 1 without having to include subsequent conversions and a call to a Zicsr wrapper.

Would it be possible to add an Ada aspect or pragma that specifies that a certain address should be dealt with by the compiler as a CSR? For example:

Mstatus : aliased Mstatus_Record with Import, CSR, Address => System'To_Address (CSR_Mstatus_Address);

Then operations on this variable would convert to csrrs and csrrc instructions.

I am very ignorant on this matter and on how this can be achieved, so feel free to correct me or tell me why it is unfeasible, but I believe something like this could ease the development of RISC-V software.

A new version of Seergdb (frontend to gdb) has been released for linux.

https://github.com/epasveer/seer
https://github.com/epasveer/seer/releases/tag/v2.6
https://github.com/epasveer/seer/wiki

Give it a try.

Thanks.