You can build gnat and gnatprove yourself, including runtime exception.

This is a bit painful (intentionally so) but it can be done.

> 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?

> 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?

Yes that's the case.

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.

Is the compiling part "a bit painful" as @tobiasu comments above? Because that is what I am trying to avoid.

Some source on this?

this is unclear to me, what source do you need?

That if you build ada yourself your binaries later either have the runtime exception or that they do not need it.

Take as an example the gnat.sockets package from upstream gcc:

https://github.com/gcc-mirror/gcc/blob/master/gcc/ada/libgna...

Compare with the same file from the GNAT 2021 CE install:

GNAT/2021/lib/gcc/x86_64-pc-linux-gnu/10.3.1/rts-native/adainclude/g-socket.ads

you will find there are a bunch of blank lines where the runtime exception was.

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(?)).

I might be ignorant, but you actually need the exception, otherwise it would be gpl, isnt it.