gnatPackages: Add scope for all ada packages

Ada depencencies musst be build with the same gnat version as the
project. Use a namespace as preperation to build with different gnat
versions.

gprbuild and gnatprove are still globaly visable.

1 files changed, 96 insertions, 0 deletions

diff --git a/pkgs/development/ada-modules/gnatprove/default.nix b/pkgs/development/ada-modules/gnatprove/default.nix
new file mode 100644
index 0000000000000..884406d3342e2
--- /dev/null
+++ b/pkgs/development/ada-modules/gnatprove/default.nix
@@ -0,0 +1,96 @@
+{ stdenv
+, lib
+, fetchFromGitHub
+, gnat
+, gnatcoll-core
+, gprbuild
+, python3
+, ocamlPackages
+, makeWrapper
+}:
+let
+  gnat_version = lib.versions.major gnat.version;
+
+  fetchSpark2014 = { rev, sha256 } : fetchFromGitHub {
+    owner = "AdaCore";
+    repo = "spark2014";
+    fetchSubmodules = true;
+    inherit rev sha256;
+  };
+
+  spark2014 = {
+    "12" = {
+      src = fetchSpark2014 {
+        rev = "ab34e07080a769b63beacc141707b5885c49d375"; # branch fsf-12
+        sha256 = "sha256-7pe3eWitpxmqzjW6qEIEuN0qr2IR+kJ7Ssc9pTBcCD8=";
+      };
+      commit_date = "2022-05-25";
+    };
+    "13" = {
+      src = fetchSpark2014 {
+        rev = "12db22e854defa9d1c993ef904af1e72330a68ca"; # branch fsf-13
+        sha256 = "sha256-mZWP9yF1O4knCiXx8CqolnS+93bM+hTQy40cd0HZmwI=";
+      };
+      commit_date = "2023-01-05";
+    };
+  };
+
+  thisSpark = spark2014.${gnat_version} or
+    (builtins.throw "GNATprove depend on a specific GNAT version and can't be built using GNAT ${gnat_version}.");
+
+in
+stdenv.mkDerivation rec {
+  pname = "gnatprove";
+  version = "fsf-${gnat_version}_${thisSpark.commit_date}";
+
+  src = thisSpark.src;
+
+  nativeBuildInputs = [
+    gnat
+    gprbuild
+    python3
+    ocamlPackages.ocaml
+    makeWrapper
+  ];
+
+  buildInputs = [
+    gnatcoll-core
+    ocamlPackages.camlzip
+    ocamlPackages.findlib
+    ocamlPackages.menhir
+    ocamlPackages.menhirLib
+    ocamlPackages.num
+    ocamlPackages.yojson
+    ocamlPackages.zarith
+  ];
+
+  propagatedBuildInputs = [
+    gprbuild
+  ];
+
+  postPatch = ''
+    # gnat2why/gnat_src points to the GNAT sources
+    tar xf ${gnat.cc.src} gcc-${gnat.cc.version}/gcc/ada
+    mv gcc-${gnat.cc.version}/gcc/ada gnat2why/gnat_src
+  '';
+
+  configurePhase = ''
+    make setup
+  '';
+
+  installPhase = ''
+    make install-all
+    cp -a ./install/. $out
+    mkdir $out/share/gpr
+    ln -s $out/lib/gnat/* $out/share/gpr/
+  '';
+
+  meta = with lib; {
+    description = "a software development technology specifically designed for engineering high-reliability applications";
+    homepage = "https://github.com/AdaCore/spark2014";
+    maintainers = [ maintainers.jiegec ];
+    license = licenses.gpl3;
+    platforms = platforms.all;
+  };
+}
+