From b946787204aea4d67126c31ac4851dee618125df Mon Sep 17 00:00:00 2001
From: Jiajie Chen <c@jia.je>
Date: Wed, 26 Oct 2022 23:11:52 +0800
Subject: [PATCH] spark2014: init at unstable-2022-05-25

---
 .../libraries/ada/spark2014/default.nix       | 71 +++++++++++++++++++
 pkgs/top-level/all-packages.nix               |  2 +
 2 files changed, 73 insertions(+)
 create mode 100644 pkgs/development/libraries/ada/spark2014/default.nix

diff --git a/pkgs/development/libraries/ada/spark2014/default.nix b/pkgs/development/libraries/ada/spark2014/default.nix
new file mode 100644
index 000000000000..1e6157cfb9a2
--- /dev/null
+++ b/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;
+  };
+}
+
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index ac655751e7c3..60745a224526 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -15850,6 +15850,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;
   };