Ada

https://www.youtube.com/live/i_bVoiDlw5E

We just finished the Ada Monthly Meetup and here are the topics that were discussed: - The recording of the presentations given during the Ada Developers Workshop 1 with their slides are now available - Stemming from (@jgrivera67) J. German Rivera’s talk about HiRTOS and him working the Renode hardware emulation tool, @ohenley did a nice article about getting started with Renode and Ada programs! Check it out! - And actually, since the last stable version of Renode, v1.15.2, released 3 weeks ago, there is a built-in demo/example of HiRTOS! - @simonjwright created a PR for SVD2Ada for it to support dimensioned register ports! - @Max has been working on creating an Ada toolchain for the XTENSA architecture. It is now officially part of Alire! Check the forum post for more info. - A reminder that the Ada Crate of the Year Award is still taking place! - We had a discussion on whether there should be a proposal for an Ada Devroom for next year’s FOSDEM. - There will be a forum thread about this topic “shortly”. - With the “demise” of SIGAda, the proposal of the creation of the Ada Users Society is moving along, which was approved in the General Assembly (GA) of Ada-Europe this past month of June. - The next GA of Ada-Europe will be taking place in a couple of weeks, the next 26th of September. Remember to ask for the meetup link if you would like to join! - We had a couple of discussions during the meetup and afterwards regarding some doubts and timeline/availability of the new Ada Users Society. - A complete working Alire manifest has been created for the WolfSSL library 2. - Though it is not in Alire’s index! It still needs some work, but you can already start using it! - @stcarrez and @Max have been working on Ada-Enet, an embedded network stack written in Ada. - It is now available in Alire and it has a few STM32 drivers already! - @Max also has an ethernet stack written in Ada, which has also been added ot Alire - @simonjwright updated us on the state (and struggles) of the Ada support on the newly released RP 2350 CPU 1. - Progress is good and small examples are already running on the chip. Interrupts are still a problem to be solved :slight_smile: - @AJ-Ianozi reminded us about the latest Yet Another Static Site (Generator) and its features, which recently had its 3.1.0 release That is all that was discussed today!

2
0
blog.adacore.com

The competition has three prizes of $2,000 each!

2
0
opencollective.com

Just came across a donation site for the Alire project. > Contributing to the Ada open source ecosystem through the Alire package manager for Ada/SPARK

2
0
https://www.ada-europe.org/conference2024/adadev.html

Online participation in the Ada Developers Workshop will be **free of charge**! It is still a requirement to register. As a reminder, the Workshop's programe has been available for a while, so go ahead an take a look! 🤩

4
0

GNAT FSF 14 is now available in a special index branch. Use this command to add the index branch: ``` alr index "--add=git+https://github.com/alire-project/alire-index#gnat-fsf-14.1" --name=gnat_fsf_14 --before=community ``` And then `alr index --del=gnat_fsf_14` to remove it once your done playing with it. If you have some time to give it a try and give me some feedback that would be great 👍️ #gcc #alire

5
0
https://gcc.gnu.org/gcc-14/changes.html

- New implementation-defined aspects and pragmas: - `Local_Restrictions`, which specifies that a particular subprogram does not violate one or more local restrictions, nor can it call a subprogram that is not subject to the same requirements. - `User_Aspect_Definition` and `User_Aspect`, which provide a mechanism for avoiding textual duplication if some set of aspect specifications is needed in multiple places. - New implementation-defined aspects and pragmas for verification of the SPARK 2014 subset of Ada: - `Always_Terminates`, which provides a condition for a subprogram to necessarily complete (either return normally or raise an exception). - `Ghost_Predicate`, which introduces a subtype predicate that can reference Ghost entities. - `Exceptional_Cases`, which lists exceptions that might be propagated by the subprogram with side effects in the context of its precondition and associates them with a specific postcondition. - `Side_Effects`, which indicates that a function should be handled like a procedure with respect to parameter modes, `Global` contract, exceptional contract and termination: it may have output parameters, write global variables, raise exceptions and not terminate. - The new attributes and contracts have been applied to the relevant parts of the Ada runtime library, which has been subsequently proven to be correct with SPARK 2014. - Support for the LoongArch architecture. - Support for vxWorks 7 Cert RTP has been removed. - Additional hardening improvements. For more information reltated to hardening options, refer to the GCC Instrumentation Options and the GNAT Reference Manual, Security and Hardening Features. - Improve style checking for redundant parentheses with `-gnatyz` - New switch `-gnateH` to force reverse Bit_Order threshold to 64. - Experimental features: - **Storage Model**: this feature proposes to redesign the concepts of Storage Pools into a more efficient model allowing higher performances and easier integration with low footprint embedded run-times. - **String Interpolation**: allows for easier string formatting. Further clean up and improvements to the GNAT code.

8
0
https://www.getada.dev/

This site provides a simple way to install Ada's toolchain Alire using GetAda.

2
0
https://packages.debian.org/bookworm/alire

Did you know that Debian has Aiire packages?!

3
0
www.crowdsupply.com

Fabien is starting a crowdfunding campaign for a pocket groovebox he has been developing on his spare time. Of course the firmware is in Ada 🤩 The sources are [on GitHub](https://github.com/wee-noise-makers/WNM-PGB1-firmware) if you want to have a look. If you can subscribe on CrowdSupply and send this link to anyone that could be interested, that would help a lot.

8
0
https://groups.google.com/g/muen-dev/c/jn9fb2A6X8o

A new Muen version with a long change log! 🤩

2
0
forum.ada-lang.io

🔥 Hot news! Thanks to AdaCore sponsoring the Ada Developer Workshop in Barcelona, the early registration fee for in-person participation will be only **10 EUR**, including 🥪 lunch and ☕ coffee breaks. That’s as low-cost as attending an Ada Developer Room at FOSDEM in Brussels, as you easily spend 10 EUR on food and drinks there… 😉 Registration info, for the conference, tutorials, workshops, social events, will shortly be added to the [conference website](http://www.ada-europe.org/conference2024) at Ada-Europe 2024 1. Hope to see many of you there! And remember, submissions are still welcome!

4
0
forum.ada-lang.io

The March 2024 Meetup just finished! Thanks to everybody who participated. Quite a few topics were discussed, here is a list of topics and references to them: - WolfSSL and its Ada binding - [FOSDEM](https://fosdem.org/2024/) - [Ada Developer Workshop](http://www.ada-europe.org/conference2024/adadev.html) taking place in Barcelona the 14th of June. - The (current) submission deadline for presentations is the 31st of March! - Online participation is expected. We will try and have a setup to let people participate online! - It was created in order to let the wider Ada community have a home to meet and talk about Ada. This is a "response" to the lack of an Ada DevRoom @ FOSDEM the past couple of years. - [Alire v2.0 is around the corner](https://forum.ada-lang.io/t/ada-monthly-meeting/384/30) - Help test the new [Release Candidate 1](https://github.com/alire-project/alire/releases) - Mac M1 (ARM64) support is in the works. Thanks Simon and Maxim! - There is now a list of [projects to work on](https://ada-lang.io/docs/projects-to-work-on/) in the main Ada-Lang webpage. - It focuses of projects that would help the wider Ada community. - [Ada support for org-mode code blocks (babel) is now going to be part of the official org-mode distribution of Emacs!](https://list.orgmode.org/orgmode/87cyskn7xa.fsf@localhost/T/#mb5774149b4b90712e4bccc0f936ebbbbe138e065) - Thanks Francesc for the work! - The [NSA published a list of memory safe languages](https://www.cisa.gov/sites/default/files/2023-12/The-Case-for-Memory-Safe-Roadmaps-508c.pdf) - Ada was not mentioned in the list of programming languages. Nonetheless Ada/SPARK are listed in the references. - Ada needs better visibility and "marketing". - The GCC 14's Ada changelog section is on its way, stay tuned!

4
0
www.adacore.com

LatenceTech leverages Ada's capabilities to develop innovative network tools. They successfully implemented patented LIFBE process, reducing data volume for bandwidth testing by 90%. Ada's low-level memory management and concurrency features were crucial for this project. GNAT Pro's real-time capabilities also ensured timely delivery. This collaboration highlights Ada's suitability for energy-efficient network software and complex real-time systems. Join the Ada community and empower the next generation of reliable, high-performance software!

1
2
https://www.ada-europe.org/archive/auj/auj-43-4-withcovers.pdf

TOC: - J. P. Rosen. “Report on the ASIS BoF Session: The Future of ASIS and Vendor Independent Tools” 221 - C. Dross. “Containers for Specification in SPARK” 249 - S. Tucker Taft. “Rigorous Pattern Matching as a Language Feature” 255 - L. Humphrey. “Basic Formal Verification of a Waypoint Manager for Unmanned Air Vehicles in SPARK”

1
0
ada
Ada ada Now 100%
Ada on NetBSD!

🎉 NetBSD has got [GNAT 13](https://pkgsrc.se/wip/gcc13-gnat), [gprbuild](https://pkgsrc.se/wip/gprbuild) and [Alire](https://pkgsrc.se/wip/alire)!

1
0
github.com

LibMLKEM: a brand new, formally verified implementation of the post-quantum key exchange algorithm ML-KEM, built with the Ada & SPARK. # Why LibMLKEM? - Rock-solid security: SPARK's formal verification guarantees no errors, leaks, or type issues. - Independent & transparent: a completely new take on ML-KEM, free from existing code biases. - Pushing the boundaries: a benchmark for formal verification tools like SPARK, CBMC, and Kani. # Not production-ready yet! LibMLKEM is for research and demonstration purposes only. It prioritizes security and verifiability over optimization. The constant time property hasn't verified yet.

1
0
forum.ada-lang.io

📆 I would like to announce the March (2024) Ada Monthly Meetup which will be taking place on the 9th of March at 14:00 UTC time (15:00 CET). As always the meetup will take place over at [Jitsi](https://meet.jit.si/AdaMonthlyMeetup). The Meetup will also be livestreamed to [Youtube](https://www.youtube.com/@ada-maximized). If someone would like to propose a talk or a topic, feel free to do so! We currently have no topics 😉

1
0