The previous installPhase was only using `make install`, while the real
target needed is `make install-all`. This installs many missing tools
under `$out/libexec/`, such as the missing `gnatwhy3` binary, which was
the root cause of #208830.
With this, gnatprove can now successfully discharge and prove things
with solvers like Z3, etc.
And, because it also includes `why3server`, we don't need to use
wrapProgram on it anymore, either!
Closes#208830
Signed-off-by: Austin Seipp <aseipp@pobox.com>
gnatcoll-sql: init at 21.0.0
gnatcoll-sqlite: init at 21.0.0
gnatcoll-xref: init at 21.0.0
gnatcoll-postgres: init at 21.0.0
gnatcoll-db2ada: init at 21.0.0
gnatinspect: init at 21.0.0
Ada database interaction libraries and related tools which are managed
in the gnatcoll-db repository. The attribute and derivation names
don't include "db" since the GPR project files upstream also don't:
They are named `gnatcoll_${component}.gpr` usually, except for the
executables.
gnatcoll-gmp: init at 21.0.0
gnatcoll-iconv: init at 21.0.0
gnatcoll-lzma: init at 21.0.0
gnatcoll-omp: init at 21.0.0
gnatcoll-python3: init at 21.0.0
gnatcoll-readline: init at 21.0.0
gnatcoll-syslog: init at 21.0.0
gnatcoll-zlib: init at 21.0.0
This inits a bunch of gnatcoll-* packages which are managed in the
gnatcoll-bindings repository. I have chosen not to include "bindings"
in their derivation or attribute names, since the GPR project
definitions themselves all don't contain that as well, instead they
are name `gnatcoll_${component}.gpr`.
GPRbuild is a multi language build system developed by AdaCore which
is mostly used for build Ada-related projects using GNAT.
Since GPRbuild is used to build itself and its dependency library
XML/Ada we first build a bootstrap version of it using the provided
bash build script bootstrap.sh as the gprbuild-boot derivation.
gprbuild-boot is then used to build xmlada and the proper gprbuild
derivation.
GPRbuild has its own search path mechanism via GPR_PROJECT_PATH which
we address via a setupHook. It currently works quite similar to the
pkg-config one: It accumulates all inputs into GPR_PROJECT_PATH,
GPR_PROJECT_PATH_FOR_BUILD etc. However this is quite limited at the
moment as we don't have a gprbuild wrapper yet which understands the
_FOR_BUILD suffix. However, we'll need to address this in the future
as it is currently basically impossible to test since the distinction
only affects cross-compilation, but it is not possible to build a GNAT
cross-compiler in nixpkgs at the moment (I'm working on changing that,
however).
Another issue we had to solve was GPRbuild not finding the right GNAT
via its gprconfig tool: GPRbuild has a knowledge base with compiler
definitions which run some checks and collect info about binaries
which are in PATH. In the end the first compiler in PATH that supports
the desired language is selected.
We want GPRbuild to discover our wrapped GNAT since the unwrapped one
is incapable of producing working binaries since it won't find the
crt*.o objects distributed with libc. GPRbuild however needs to find
the Ada runtime distributed with GNAT which is not part of the wrapper
derivation, so it will skip the wrapper and select the unwrapped GNAT.
Symlinking the unwrapped's lib directory into the wrapper fixes this
problem, but breaks linking in some cases (e. g. when linking against
OMP from gcc, the runtime variant will shadow the problem dynamic lib
from buildInputs). Additionally it uses gnatls as an indicator it has
found GNAT which is not part of the wrapper.
The solution we opted to adopt here is to install a custom compiler
description into gprbuild's knowledge base which properly detects the
nixpkgs GNAT wrapper: It uses gnatmake to detect GNAT instead of
gnatls and discovers the runtime via a symlink we add to
`$out/nix-support`. This additional definition is enough to properly
detect GNAT, since the plain wrapped gcc detection works out of the
box. It may, however, be necessary to add special definitions for
other languages in the future where gprbuild also needs to discover
the runtime.
One future improvement would be to install libgpr into a separate
output or split it into a separate derivation (which would require to
link gprbuild statically always since otherwise we end up with a
cyclical dependency).
