> You can build gnat and gnatprove yourself, including runtime exception.
How does that work? Are the binaries from Ada core (not FSF) intentionally distributed under GPL while the source for standardlib/run-time come with LGPL/run-time exceptions?
It was my understanding that the Ada core distribution is full GPL only, and the FSF one (lagging a few versions) was licensed more like gcc?
I am more of an end-user here trying to use SPARK2014 for applications, not doing any unnecessary software engineering or builds outside of using SPARK2014 and a compiler. It is this type of thing that makes it a bad choice for someone like me who doesn't have the time and sometimes the wherewithal to build my own compiler. Sure, a simple build of source without licensing restrictions, maybe, but not much above just using the PL to get a job done. This is why I will never give up C and the tools around it, well, maybe Zig or Rust, which I am playing with, but they are nowhere near SPARK2014/Ada for all that you get with them and the Gnat compiler. I was introduced to SPARK2014 with the book, "Building High Integrity Applications with Spark". I also read a fantastic book, "Analysable Real-Time Systems: Programmed in Ada" that put me on this vector. Great stuff and timely.
SPARK2014 is just a tool (gnatprove), which you don't distribute to others (would be rather pointless). Compiling can be done with gnat from your Linux distro, which usually has the Runtime Library Exception.
But if you're going to use the FSF version, why not use fsf/distro binaries? Getting the source from Ada core still leaves you without the runtime exception? (Ada core is upstream/newer, fsf is downstream, lagging a bit behind Ada core(?)).
This is a bit painful (intentionally so) but it can be done.