4 ms·
> Is there any non-proprietary Ada/SPARK implementation? Yes, it's now available as part of GNAT. The integration in GNAT Studio is good and lets you prove a
by pyjarrett 5y ago
> Is there any non-proprietary Ada/SPARK implementation?
Yes, it's now available as part of GNAT. The integration in GNAT Studio is good and lets you prove a single line or entire file in the IDE.
I mostly write Ada for my projects and have only dabbled in SPARK. It's super interesting, but also ridiculously hard. I don't have any formal training in this, but to me, I found it at least as on par with C++ template metaprogramming in terms of difficulty.
- jeff-davis 5y agoIs there an easy way to get up and running with SPARK on ubuntu using just "apt install" from official package repositories?
- MaxBarraclough 5y agoI don't think so, last I checked you have to download the graphical installer from AdaCore. I'm not sure why it's this way. I've never had any trouble with the installer, at least.
- pyjarrett 5y agoAlire (https://alire.ada.dev/ https://alire.ada.dev/) can do the toolchain install now. It's pretty much like cargo, and can also be used to select from multiple toolchain versions.
- pyjarrett 5y agoGNAT is part of GCC, I'd look in your package manager for "Ada" and/or GCC. I'd recommend asking in https://gitter.im/ada-lang/Lobby https://gitter.im/ada-lang/Lobby
- Quekid5 5y agoAh, thanks. I guess this is also available with the command line tools? (I'm thinking for CI purposes.)
- pyjarrett 5y agoYes, a lot of GNAT studio behavior is actually written as command line tools that get called specifically so you can use them outside of the editor. The dialogs for builds/proofs even show the exact command line that's going to be used, and updates as you configure it in the editor dialog. It's a great way to learn how the GNAT tools actually work.