❌ About FreshRSS

Normal view

There are new articles available, click to refresh the page.
Before yesterdayAda Forum - Latest topics

Gateway to comp.lang.ada

By: mgrojo
4 October 2022 at 19:11

It would be nice to have a category in the forum synchronizing with Usenet’s comp.lang.ada.

I found it should be possible using this gateway: GitHub - sman591/discourse-nntp-bridge: Discourse plugin to keep NNTP & Discourse in sync
Unfortunately, currently not in a known deployment: Still supported? · Issue #33 · sman591/discourse-nntp-bridge · GitHub

Running a spam filter would be indispensable.

1 post - 1 participant

Read full topic

Upcoming Ada-Related Conferences and Workshops

By: sttaft
4 October 2022 at 21:10

The seventh ACM SIGAda workshop on High Integrity Language Technology (ACM SIGAda HILT 2022) is being held on October 14, 2022 in Detroit, MI in conjunction with the 2022 Automated Software Engineering conference (ASE’22), sponsored by SIGAda. This year’s HILT theme is Language and Tool Support for Rigorous Software Development.

We have 9 presentations plus two keynotes related to this theme, including presentations on SPARK containers, and adding pattern matching as a language feature to Ada. Our keynote speakers are K. Rustan M. Leino, the creator of the Dafny verifiable language and the Boogie system supporting major industrial uses of formal methods, and Niko Matsakis, one of the original members of the Rust design team, talking about a-mir-formality, a more formal model of Rust.

There is now an online option for attending the ACM SIGAda HILT’22 workshop featuring Niko Matsakis and Rustan Leino. Anyone registered for the workshop will receive a link allowing use of Zoom and/or the “Whova” app to attend the workshop remotely.

The organizers of the associated conference (ASE’22) have indicated that remote attendees may register at the lowest attendee price (“Student Member”). So if you or a colleague might be interested in participating in the workshop remotely, please register soon for the October 14th workshop, at:

and indicate “Student Member” as your category of attendee.

For more information see:

#formalmethods #softwareengineering #ada #rust #spark #dafny #ACM #ASE

1 post - 1 participant

Read full topic

Spark SVD warnings

By: kevlar700
6 October 2022 at 19:20

When SVD files are a subproject you get a lot of warnings when running gnatprove on the base address.

Address => NVIC_Base

‘writing to “NVIC_Periph” is assumed to have no effects on other non-volatile objects.’

Is there a good way to quieten those. Such as exclude the SVD sub project or ideally just silence that particular warning?

If I use the --no-subprojects flag then I get some .ali incorrectly formatted fatal errors.

Perhaps I should use this for faster contract generation anyway. However, I believe case statements in .gpr files prevent gnat studio from being able to edit automatically (I can always comment and uncomment the case statements as needed though)


project My_Project is

type Modes is (“Compile”, “Analyze”);
Mode : Modes := External (“MODE”, “Compile”);

case Mode is
when “Compile” =>
for Source_Dirs use (…);
when “Analyze” =>
for Source_Dirs use (“dir1”, “dir2”);
for Source_Files use (“file1.ads”, “file2.ads”, “file1.adb”, “file2.adb”);
end case;

end My_Project;

2 posts - 1 participant

Read full topic

Where are the Ada gigs these days? (worldwide)

By: codeTripr
12 October 2022 at 19:23

I’m struggling to find job listings for Ada lately. In principle I’ll go anywhere in the world but I’m a bit tired of the US and Europe.

I’m most interested in New Zealand but after searching 72 job sites, there was nothing for Ada. There were 42 other NZ job sites (incl. seek & trademe.co.nz) I did not search due to Tor hostility & I won’t touch MS LinkedIn (yes I’m fussy about ethics / human rights / civil liberties issues). IIRC Thales had some Ada jobs in NZ for the rail industry ~15 yrs ago.

Japan would also be interesting but only if it doesn’t involve an extreme 50+ hrs/wk work schedule. Brazil would interest me too.

We could really use some kind of heat map showing Ada jobs worldwide (not necessarily just vacancies), so we can at least easily know where to look. The only resource that I’ve found that can give a clue is this (possibly unmaintained) website from 2014:


4 posts - 3 participants

Read full topic

Right way to pass arrays to interface with C

By: pyj
13 October 2022 at 00:37

I often find myself needing to do arrays of things to interface with C.

What’s the Ada way of doing this?

It seems like passing an array with An_Array'Address seems to work, but I’m not sure how the array’s bounds are stored and affect the layout of that array. This is particular importance since I’m looking at trying to store multiple arrays of potentially difference sizes allocated in memory sequentially.

struct Vec3 {
    float x, y, z;

uint32_t size = 10;
Vec3 points = new Vec3[size];
passArrayToFunc(&points[0], size);

7 posts - 5 participants

Read full topic

SPARK: Discharge verification conditions (VC) with Coq?

14 October 2022 at 13:19

Hi all,

I intend to teach students how to discharge SPARK VCs with Coq.

The motivation is that sometimes, you need interactive theorem proving to prove the properties you’d like to prove.

I started with this from the SPARK User’s Guide:

I then tried discharging all VCs with Coq in the SPARK Lab of this course:

This was reasonably easy for swap.adb and search_arr_zero.adb , but got real ugly real fast for the other ones. While I am not very experienced with Coq (I did Vol. 1-2 of Software Foundations, but that was a long time ago), it seems to me that proving VCs in Coq does not scale; they get really hard to discharge in Coq.

Notably, the VCs in Coq make no sense to me. I know they are something that SPARK needs to finish a proof (and therefore, the VC does not need to make sense, provided we trust SPARK). But still; if the VC made more sense, then it would be easier to come up with a proof idea, to then implement in Coq.

I then looked around the Internet to see if anyone actually has used Coq to discharge VCs, and I did not find anyone who has done so. Even the VerifyThis! SPARK solution does not do so (thus leaving the challenges that need interactive proofs, unsolved).

Finally, I needed to install an older version of Coq to do this exercise (since this feature only worked for that version of Coq). Setting that up was (very doable, albeit) a bit painful.

Is this something that people just don’t do? Do people use other features in SPARK (e.g. ghost code), or just turn to other tools, when automated theorem proving fails? Is this ability to discharge SPARK VCs with Coq more of a “proof of concept” / “fun demo” / “in case anyone needs it”?

If this feature is really meant for proving properties of software in industry, then I would very much value any comments, hints, pointers, or reading, on how to do this. For instance, are there certain Coq libraries / tactics that makes discharging the VCs in Coq easier? Is there some rule-of-thumb / paradigm I should follow to make whatever SPARK cannot discharge automatically as small and simple as possible?

Kind regards,

4 posts - 2 participants

Read full topic

Favourite books about Ada/Spark

By: kevlar700
16 October 2022 at 18:35

Programming in Ada 20xx by John Barnes
Ada Distilled by Richard Riehle


Please list any favourites or references that you personally turn to?

6 posts - 4 participants

Read full topic

Ada advocacy ­— Ada promoting missions — any proposals?

By: codeTripr
17 October 2022 at 08:58

It seems Ada’s unpopularity and borderline abandonment is unmerited. The problem is in part this “newer is better” (“latest and greatest”) mentality/fallacy that causes the masses to embrace anything new even if it is garbage, and treat all old tech as obsolete. This zombie thinking is part of what’s killing Ada.

What is being done to counter Ada losing ground? Ada never even took ground that it should have had in the first place. E.g. safety critical medical devices are still developed in C (last I checked).

If you go to fsf.org, there’s a “campaigns” page where they’ve organized projects to promote the FSF ideology. FSF also has a “High Priority Free Software Projects” list that gets updated annually:


That list presents projects needed to most significantly advance the FOSS movement. Is there such a list to advocate & advance the Ada language? One item on the FSF list is “Free drivers, firmware, and hardware designs”. What if there were projects to code firmware, drivers, and libraries in Ada? This would do more to promote the language than an application because it would force/coerce app developers into contact with Ada code when they develop apps. Shouldn’t something like libreboot/coreboot be a high-priority Ada project? Ada is also most suitable for low-level hardware tasks anyway, no? Would it make sense for Adacore and FSF to combine forces and mutually promote FOSS & Ada together? In principle both FSF & Adacore would benefit from filling the gap in FOSS f/w & drivers.

27 posts - 11 participants

Read full topic

IDE, your alternative to gnatstudio?

17 October 2022 at 16:28


I’m most of the time under windows when experimenting with Ada. But i’ve a lot of problems with gnatstudio, like the keyboard shortcuts with alt-gr Key that doesn’t work at all… impossible with m’y french keyboard to use #&{}[]@ etc… Notepad crt+c, ctrl-v is not really a good solution and i’m unsuccessful at building gnatstudio from source.

Some of Ada dev’s seems working with vscode, but none of the extensions for ada in this IDE seems, working… Neither for intellij plugin from adacore unmaintained from years.

Do you have some alternative ? What Do you use ?

18 posts - 10 participants

Read full topic

[Ada FOSDEM] No Ada DevRoom for 2023, alternative rooms and Ada-Europe support

By: Irvise
8 November 2022 at 11:54

Dear Ada community,

Our proposal for an Ada Developer Room for FOSDEM 2023 has been declined. I asked whether we could have a virtual DevRoom just like in FOSDEM 2022, but it seems unlikely. This means Ada will (most likely) not take part in the new edition of FOSDEM. We are saddened by this decision, but the amount of proposals was indeed very large: 88 DevRoom proposals were submitted!

Nonetheless, we would like to encourage Ada developers to submit presentations to other DevRooms that may fit your interests! You can find the accepted DevRooms in [1]. I think the rooms that could be of interests to the Ada community are “Confidential Computing”, “Embedded, Mobile and Automotive”, “FOSS Educational Programming Languages”, “Microkernel and Component-based OS”, “Open Source Firmware, BMC and Bootloader” and “Security”. However, take a look at all the proposals! Maybe you are writing some RISC-V or networking software in Ada, and there is a DevRoom just for it! Please keep the AdaFOSDEM mailing list [2] informed about submissions and definitely about accepted proposals: we’ll build a consolidated list of Ada-related talks at FOSDEM 2023, as we did before [3]. If you have any questions or issues, we will gladly help you where we can.

We are also happy to announce that Ada-Europe [4], after learning that there would be no Ada DevRoom in FOSDEM, has opened the possibility of adding a new “DevRoom like” track in their 2023 conference [5]. The Ada-Europe conference will take place in Lisbon between the 13 and 16 of June, 2023. If you are interested in this possibility, please, contact Dirk Craeynest <[email protected]> to let him know.

Best regards,
The Ada FOSDEM team

[1] FOSDEM 2023 - Accepted developer rooms
[2] http://listserv.cc.kuleuven.be/archives/adafosdem.html
[3] Ada at the Free and Open source Software Developers' European Meeting (FOSDEM'2021)
[4] http://www.ada-europe.org/
[5] Ada-Europe 2023 - Call for Contributions

2 posts - 2 participants

Read full topic

Unusual hardware register behavior

9 November 2022 at 17:47

On the RP2040, each GPIO pin can trigger four different interrupts: high level, low level, rising edge, and falling edge. Each pin has a 4-bit field for selecting which of these interrupts is enabled. I modeled it as an array of records.

with System;

procedure Main is
    type INT_Field is record
        Low_Level, High_Level, Falling_Edge, Rising_Edge : Boolean := False;
    end record
        with Size => 4;
    for INT_Field use record
        Low_Level    at 0 range 0 .. 0;
        High_Level   at 0 range 1 .. 1;
        Falling_Edge at 0 range 2 .. 2;
        Rising_Edge  at 0 range 3 .. 3;
    end record;

    type GPIO_Pin is range 0 .. 30;
    type INT_Register is array (GPIO_Pin) of INT_Field
        with Component_Size => 4;

    type GPIO_Peripheral is record
        INTE : INT_Register; --  Write to enable interrupts
        INTS : INT_Register; --  Masked status of enabled interrupts
        INTR : INT_Register; --  Unmasked interrupt status, write to clear
    end record;

    GPIO : GPIO_Peripheral
        with Import, Address => System'To_Address (16#4001_40F0#);
    GPIO.INTE (7).Rising_Edge := True;
end Main;

I’m simplifying things a bit here for clarity. You can find the actual implementation on GitHub

On the surface, this looks like it should work. Compiling with GNAT, this results in a strb (Store Byte) instruction after shifting some bits around.

Now this is where the bug comes in… The RP2040 datasheet explains:

2.1.4. Narrow IO Register Writes

Memory-mapped IO registers on RP2040 ignore the width of bus read/write accesses. They treat all writes as though they were 32 bits in size. This means software can not use byte or halfword writes to modify part of an IO register: any write to an address where the 30 address MSBs match the register address will affect the contents of the entire register.

By “affect the contents of the entire register,” it means that an 8-bit write to a 32-bit register will change all of the bytes of the register to the same value.

If our register value is 16#0000_0000# and the strb instruction is setting bit 8 so that we have 16#0000_0100#, the resulting value is 16#0101_0101# instead.

My solution is to add another array to group fields into 32-bit array elements, so that we can use the Volatile_Full_Access aspect to guarantee that the whole word is written using the str instruction.

    type INT_Register is array (0 .. 7) of INT_Field
        with Volatile_Full_Access, Component_Size => 4, Size => 32;

    type INT_Group is array (0 .. 3) of INT_Register
        with Component_Size => 32;

This solution works, but has left me wondering how we can prevent this from happening again in the future. This is not the first bug I’ve encountered caused by the narrow write behavior of the I/O memory.

I have a few questions for discussion:

  • Is there a way to tell the compiler that a memory range only supports writes of a specific size?
  • If not, can we at least generate a warning?
  • SPARK has the Async_Writers aspect, which indicates that some external process can modify the register value. If we were to verify this code, it seems like every register would need this aspect due to this narrow write behavior.
  • Philosophically, is it possible to make any guarantees about the software without access to the hardware HDL sources? It seems like there’s a bit too much human error possible in the process of writing and interpreting documentation about hardware behavior.

6 posts - 5 participants

Read full topic

Gnu Emacs Ada mode 8.0 beta released

9 November 2022 at 18:36

Gnu Emacs Ada mode 8.0 beta is now available in GNU ELPA devel for
beta testing.

All Ada mode executables can now be built with Alire
(https://alire.ada.dev/); this greatly simplifies that process.

gpr-query and gpr-mode are split out into separate GNU ELPA packages.
You must install them separately (Emacs install-package doesn’t
support “recommended packages” like Debian does).

Ada mode can now be used with Eglot; this is controlled by new variables:

ada-face-backend - one of wisi, eglot, none

ada-xref-backend - one of gnat, gpr_query, eglot, none

ada-indent-backend - one of wisi, eglot, none

The the indent and face backends default to wisi if the wisi parser is
found in PATH, to eglot if the Ada LSP server is found, and none
otherwise. The xref backend also looks for the gpr_query executable in

The current AdaCore language server (23) support face but not indent.
The current version of eglot (19) does not support face. So for now,
eglot + ada_language_server only provides xref.

The AdaCore language server ada_language_server is installed with
GNATStudio (which ada-mode will find by default), or can be built with
Alire. If you build it with Alire, either put it in PATH, or set

I have not tested ada-mode with lsp-mode. You can set ada-*-backend to
'other to expermiment with that, or tree-sitter, or some other

To access the beta version via Gnu ELPA, add the devel archive to

(add-to-list 'package-archives (cons “gnu-devel” “GNU-devel ELPA Packages”))

Then M-x list-packages; the beta release shows as ada-mode version, wisi version similarly.

Please report success and issues to the Emacs ada-mode mailing list
Ada-mode-users Info Page.

The required Ada code requires a manual compile step, after the normal
list-packages installation:

cd ~/.emacs.d/elpa/ada-mode-7.3beta*

If you have Alire installed, these scripts use it. Otherwise, this
requires AdaCore gnatcoll packages which you may not have installed;
see ada-mode.info Installation for help in installing them.

1 post - 1 participant

Read full topic

About the Advent of Code category

15 November 2022 at 03:09

Advent of Code is a series of daily programming puzzles from December 1st to 25th, becoming progressively more difficult each day.

I’d like to encourage conversation about the problems and solutions in Ada and SPARK on this forum.

I’ve created a new Advent of Code category. If you don’t see a topic for today’s puzzle, feel free to create one. Discussion of general techniques and tools not tied to a specific puzzle is also welcome.

I’ve installed the “Spoiler Alert” plugin, you should use this when posting completed solutions. See below for an example of how to use this feature, along with syntax highlighting.

Screenshot 2022-11-14 19.39.12

1 post - 1 participant

Read full topic

Gnat Studio highlight occurences

By: kevlar700
15 November 2022 at 13:29

Many IDEs highlight occurences of the current selection. I have seen the Occurences plugin. Is there an automated option upon mouse double click?

Edit: I shall just add a keyboard shortcut for find all references.

Edit 2: I thought I had tried setting the ephemeral highlighting colour and restarting Gnat Studio. Perhaps I didn’t restart as it is working today.

1 post - 1 participant

Read full topic

Ada/SPARK support for Emacs org-babel

By: rocher
16 November 2022 at 16:28

I recently published a new minor release, 1.3.1, of the ob-ada-spark.el package for Emacs org-babel in melpa.org.


  1. It now works fine with latest release of Ada mode (7.3.1) and Emacs 28
  2. New custom variable to add arbitrary compiler switches
  3. New header argument to add arbitrary compiler switches to a block of code; these are appended after the switches in the custom variable (if any)
  4. Updated documentation and examples

More details in GitHub - rocher/ob-ada-spark.
Comments and feedback are welcome.

1 post - 1 participant

Read full topic