As far as I'm aware, the compiler AdaCore sells is just GCC. You can install GCC built with Ada support from your distros package manager and it will just work. You can also download builds from here: https://github.com/alire-project/GNAT-FSF-builds
> As far as I'm aware, the compiler AdaCore sells is just GCC.
The compiler yes, but I'm convinced FOSS gnatprove must be outdated in some way: Last time I tried following AdaCore's SPARK manuals, certain basic aspects and pragmas didn't work correctly on the latest version.
Not to mention when SPARK aspects sometimes broke the LSP and formatter.
If something hasn't changed, FSF builds are a year behind libre version (by design), and libre version is GPL3 cancer which is not suitable for commercial development. You're then stuck either with a year old version or buy into AdaCore Pro version of it. Not great, not terrible.. but that's kind of the only game out in the open, which is what makes it different from most of other languages out there.
GNAT CE isn't a thing anymore, only FSF and Pro exist. And AdaCore now sponsors Alire, which installs FSF GNAT, and relicensed some of their tools more permissively.