Merge pull request #197926 from jiegec/spark2014

pkgs/development/libraries/ada/spark2014/default.nix

@@ -0,0 +1,71 @@
+{ stdenv
+, lib
+, fetchFromGitHub
+, gnat12
+, gnatcoll-core
+, gprbuild
+, python3
+, why3
+, ocaml
+, ocamlPackages
+, makeWrapper
+}:
+
+stdenv.mkDerivation rec {
+  pname = "spark2014";
+  version = "unstable-2022-05-25";
+
+  src = fetchFromGitHub {
+    owner = "AdaCore";
+    repo = "spark2014";
+    # commit on fsf-12 branch
+    rev = "ab34e07080a769b63beacc141707b5885c49d375";
+    sha256 = "sha256-7pe3eWitpxmqzjW6qEIEuN0qr2IR+kJ7Ssc9pTBcCD8=";
+    fetchSubmodules = true;
+  };
+
+  nativeBuildInputs = [
+    gnat12
+    gprbuild
+    python3
+    ocaml
+    makeWrapper
+  ];
+
+  buildInputs = [
+    gnatcoll-core
+    ocamlPackages.camlzip
+    ocamlPackages.findlib
+    ocamlPackages.menhir
+    ocamlPackages.menhirLib
+    ocamlPackages.num
+    ocamlPackages.yojson
+    ocamlPackages.zarith
+  ];
+
+  postPatch = ''
+    # gnat2why/gnat_src points to the GNAT sources
+    tar xf ${gnat12.cc.src} gcc-12.2.0/gcc/ada
+    mv gcc-12.2.0/gcc/ada gnat2why/gnat_src
+  '';
+
+  configurePhase = ''
+    make setup
+  '';
+
+  postInstall = ''
+    cp -a ./install/. $out
+    # help gnatprove to locate why3server
+    wrapProgram "$out/bin/gnatprove" \
+        --prefix PATH : "${why3}/lib/why3"
+  '';
+
+  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;
+  };
+}
+

pkgs/top-level/all-packages.nix

@@ -15984,6 +15984,8 @@ with pkgs;
 
   sparkleshare = callPackage ../applications/version-management/sparkleshare { };
 
+  spark2014 = callPackage ../development/libraries/ada/spark2014 { };
+
   spidermonkey_78 = callPackage ../development/interpreters/spidermonkey/78.nix {
     inherit (darwin) libobjc;
   };