From d22ba0a2a71cb6136115ca91999409d6498c9936 Mon Sep 17 00:00:00 2001
From: Thomas Heijligen <src@posteo.de>
Date: Mon, 19 Feb 2024 20:03:13 +0000
Subject: [PATCH] gnatprove: Make src dependend on gcc version

Gnatprove is tightly bound to a specific gcc version. Use the gcc input
version to determin which gnatprove/spark2014 sources should be used.
For now gcc 12 is the only working option. gcc 13 will work as soon as
all ada buildInputs can be provided as gcc 13 build.
---
 .../libraries/ada/gnatprove/default.nix       | 47 ++++++++++++++-----
 1 file changed, 35 insertions(+), 12 deletions(-)

diff --git a/pkgs/development/libraries/ada/gnatprove/default.nix b/pkgs/development/libraries/ada/gnatprove/default.nix
index ce0f3cc432c1..4e7c4d964af6 100644
--- a/pkgs/development/libraries/ada/gnatprove/default.nix
+++ b/pkgs/development/libraries/ada/gnatprove/default.nix
@@ -1,29 +1,52 @@
 { stdenv
 , lib
 , fetchFromGitHub
-, gnat12
+, gnat
 , gnatcoll-core
 , gprbuild
 , python3
 , ocamlPackages
 , makeWrapper
 }:
+let
+  gnat_version = lib.versions.major gnat.version;
 
-stdenv.mkDerivation rec {
-  pname = "gnatprove";
-  version = "unstable-2022-05-25";
-
-  src = fetchFromGitHub {
+  fetchSpark2014 = { rev, sha256 } : fetchFromGitHub {
     owner = "AdaCore";
     repo = "spark2014";
-    # commit on fsf-12 branch
-    rev = "ab34e07080a769b63beacc141707b5885c49d375";
-    sha256 = "sha256-7pe3eWitpxmqzjW6qEIEuN0qr2IR+kJ7Ssc9pTBcCD8=";
     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 = [
-    gnat12
+    gnat
     gprbuild
     python3
     ocamlPackages.ocaml
@@ -43,8 +66,8 @@ stdenv.mkDerivation rec {
 
   postPatch = ''
     # gnat2why/gnat_src points to the GNAT sources
-    tar xf ${gnat12.cc.src} gcc-${gnat12.cc.version}/gcc/ada
-    mv gcc-${gnat12.cc.version}/gcc/ada gnat2why/gnat_src
+    tar xf ${gnat.cc.src} gcc-${gnat.cc.version}/gcc/ada
+    mv gcc-${gnat.cc.version}/gcc/ada gnat2why/gnat_src
   '';
 
   configurePhase = ''