For those users of the GNAT GPL edition, we are pleased to announce the availability of the 2017 release of GNAT GPL and SPARK GPL.

SPARK GPL 17 offers improved automation of proofs, thanks to improvements in the underlying prover Alt-Ergo and a finer-grain splitting of conjunctions. Interaction during proof has been improved thanks to the new statistics, display and replay modes. Type invariants from Ada are now also supported in SPARK. Note that the optional provers CVC4 and Z3 are no longer distributed with SPARK GPL 2017, and should be installed separately.

This release also marks the first introduction of “future language” Ada 2020 features:

• delta aggregates (partial aggregate notation)
• AI12-0150-1 class-wide invariants now employ class-wide pre-/postcondition-like semantics (static call resolution).

This release supports the ARM ELF bare metal target, hosted on Windows and Linux, as well as the following native platforms:

• Mac OS (64 bits)
• Linux (64 bits)
• Windows (32 bits)

The GNATemulator technology has been added to the bare metal target, making it easier to develop and test on those platforms.

The compiler toolchain is now based on GCC 6. The native runtime comes with a Zero Foot Print runtime, and the ARM ELF compiler comes with runtimes for a variety of boards, including support for the Raspberry Pi 2.

The latest version of the GPS IDE comes with many bug fixes and enhancements, notably in the areas of debugger integration and support for bare-metal development.

The GPL 2017 release can be downloaded:

• from the "Download" section on GNAT Tracker for members of the GNAT Academic Program, at https://www.adacore.com/academia
• from the libre site https://libre.adacore.com/

Feeling inspired and want to start Making with Ada today? Check out the Make With Ada Competition! http://makewithada.org