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
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
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)
https://docs.adacore.com/spark2014-docs/html/ug/en/spark_mode.html#specifying-files-to-analyze
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
3 posts - 2 participants
1 post - 1 participant
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:
http://www2.seas.gwu.edu/~mfeldman/ada-project-summary.html
4 posts - 3 participants
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.
Loginstruct Vec3 {
float x, y, z;
};
uint32_t size = 10;
Vec3 points = new Vec3[size];
passArrayToFunc(&points[0], size);
7 posts - 5 participants
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:
https://docs.adacore.com/spark2014-docs/html/ug/en/source/manual_proof.html#manual-proof-using-coq
I then tried discharging all VCs with Coq in the SPARK Lab of this course:
https://www.inf.ed.ac.uk/teaching/courses/fv/spark/spark-lab.html
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,
Willard
4 posts - 2 participants
Hello,
I was browsing the site… Nice, content, design, nothing to complain about. Except that there is something that really bother me and becomes tiring after 3 minutes of reading…
The top navigation bar, wouldn’t it be more ergonomic to leave it fixed??? 
Thx.
5 posts - 4 participants
Does anyone else get this 0018 cancel character showing when pressing ctrl->c in view os shell?
4 posts - 3 participants
Programming in Ada 20xx by John Barnes
Ada Distilled by Richard Riehle
https://en.m.wikibooks.org/wiki/Ada_Programming
Please list any favourites or references that you personally turn to?
6 posts - 4 participants
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:
https://www.fsf.org/campaigns/priority-projects/
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
Hi,
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
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
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#);
begin
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:
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.6 posts - 5 participants
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
PATH.
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
gnat-lsp-server-exec.
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
backend.
To access the beta version via Gnu ELPA, add the devel archive to
package-archives:
(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
8.0.3.0.20221106.55317, 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*
./build.sh
./install.sh
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
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.
1 post - 1 participant
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
I recently published a new minor release, 1.3.1, of the ob-ada-spark.el package for Emacs org-babel in melpa.org.
Summary:
More details in GitHub - rocher/ob-ada-spark.
Comments and feedback are welcome.
1 post - 1 participant
