push sheeet

pkgs/development/ada-modules/gnatprove/0001-fix-install.patch

@@ -0,0 +1,33 @@
+From 7458110cc50d91cb7833b2abd232faca52865566 Mon Sep 17 00:00:00 2001
+From: Thomas Heijligen <src@posteo.de>
+Date: Tue, 21 May 2024 22:02:09 +0000
+Subject: [PATCH] fix install
+
+---
+ Makefile | 10 +++++-----
+ 1 file changed, 5 insertions(+), 5 deletions(-)
+
+diff --git a/Makefile b/Makefile
+index 4950b2d5cc..9d9358ad08 100644
+--- a/Makefile
++++ b/Makefile
+@@ -106,11 +106,11 @@ install:
+ 	$(CP) share/spark/theories/*why $(THEORIESDIR)
+ 	$(CP) share/spark/theories/*mlw $(THEORIESDIR)
+ 	$(CP) share/spark/runtimes/README $(RUNTIMESDIR)
+-	@echo "Generate Coq files by preprocessing context files:"
+-	$(MAKE) -C include generate
+-	$(CP) include/src/*.ad? $(INCLUDEDIR)
+-	$(CP) include/*.gpr $(LIBDIR)
+-	$(CP) include/proof $(LIBDIR)
++	#@echo "Generate Coq files by preprocessing context files:"
++	#$(MAKE) -C include generate
++	#$(CP) include/src/*.ad? $(INCLUDEDIR)
++	#$(CP) include/*.gpr $(LIBDIR)
++	#$(CP) include/proof $(LIBDIR)
+ 
+ doc: $(DOC)
+ 
+-- 
+2.44.0
+

pkgs/development/ada-modules/gnatprove/0002-mute-aarch64-warnings.patch

@@ -0,0 +1,22 @@
+--- a/src/counterexamples/ce_parsing.adb	2025-03-14 21:48:15.657409808 +0100
++++ b/src/counterexamples/ce_parsing.adb	2025-03-14 22:04:32.114664704 +0100
+@@ -975,6 +975,9 @@
+                elsif Is_Extended_Precision_Floating_Point_Type (Ty) then
+                   pragma Assert (Size (Exp) = 15);
+                   pragma Assert (Size (Significand) = 63);
++                  pragma Warnings (Off, "assertion will fail at run time");
++                  pragma Warnings (Off,
++                      "types for unchecked conversion have different sizes");
+                   declare
+                      package P is new Parse_Conversion
+                        (Interfaces.Unsigned_128, Long_Long_Float);
+@@ -983,6 +986,9 @@
+                   begin
+                      return (Float_K, (Extended_K, F));
+                   end;
++                  pragma Warnings (On,
++                      "types for unchecked conversion have different sizes");
++                  pragma Warnings (On, "assertion will fail at run time");
+                else
+                   raise Program_Error;
+                end if;

pkgs/development/ada-modules/gnatprove/0003-Adjust-after-category-change-for-N_Formal_Package_De.patch

@@ -0,0 +1,33 @@
+From 3c06fb993ae628b5069c1f3e23f11c53815e1cbe Mon Sep 17 00:00:00 2001
+From: Eric Botcazou <ebotcazou@adacore.com>
+Date: Sat, 8 Mar 2025 00:09:57 +0100
+Subject: [PATCH] Adjust after category change for N_Formal_Package_Declaration
+
+Issue: eng/toolchain/gnat#1354
+---
+ src/why/gnat2why-borrow_checker.adb | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/src/why/gnat2why-borrow_checker.adb b/src/why/gnat2why-borrow_checker.adb
+index a97f225b06..f3ab8be3e9 100644
+--- a/src/why/gnat2why-borrow_checker.adb
++++ b/src/why/gnat2why-borrow_checker.adb
+@@ -1693,6 +1693,7 @@ procedure Check_Declaration (Decl : Node_Id) is
+          --  Ignored constructs for pointer checking
+ 
+          when N_Formal_Object_Declaration
++            | N_Formal_Package_Declaration
+             | N_Formal_Type_Declaration
+             | N_Incomplete_Type_Declaration
+             | N_Private_Extension_Declaration
+@@ -3326,7 +3327,6 @@ procedure Check_Node (N : Node_Id) is
+             | N_Empty
+             | N_Enumeration_Representation_Clause
+             | N_Exception_Renaming_Declaration
+-            | N_Formal_Package_Declaration
+             | N_Formal_Subprogram_Declaration
+             | N_Freeze_Entity
+             | N_Freeze_Generic_Entity
+-- 
+2.48.1
+

pkgs/development/ada-modules/gnatprove/default.nix

@@ -0,0 +1,155 @@
+{
+  stdenv,
+  lib,
+  fetchFromGitHub,
+  gnat,
+  gnatcoll-core,
+  gprbuild,
+  python3,
+  ocamlPackages,
+  makeWrapper,
+  gpr2,
+}:
+let
+  gnat_version = lib.versions.major gnat.version;
+
+  # gnatprove fsf-14 requires gpr2 from a special branch
+  gpr2_24_2_next =
+    (gpr2.override {
+      # pregenerated kb db is not included
+      gpr2kbdir = "${gprbuild}/share/gprconfig";
+    }).overrideAttrs
+      (old: rec {
+        version = "24.2.0-next";
+        src = fetchFromGitHub {
+          owner = "AdaCore";
+          repo = "gpr";
+          rev = "v${version}";
+          hash = "sha256-Tp+N9VLKjVWs1VRPYE0mQY3rl4E5iGb8xDoNatEYBg4=";
+        };
+      });
+
+  fetchSpark2014 =
+    { rev, hash }:
+    fetchFromGitHub {
+      owner = "AdaCore";
+      repo = "spark2014";
+      fetchSubmodules = true;
+      inherit rev hash;
+    };
+
+  spark2014 = {
+    "12" = {
+      src = fetchSpark2014 {
+        rev = "ab34e07080a769b63beacc141707b5885c49d375"; # branch fsf-12
+        hash = "sha256-7pe3eWitpxmqzjW6qEIEuN0qr2IR+kJ7Ssc9pTBcCD8=";
+      };
+      commit_date = "2022-05-25";
+    };
+    "13" = {
+      src = fetchSpark2014 {
+        rev = "12db22e854defa9d1c993ef904af1e72330a68ca"; # branch fsf-13
+        hash = "sha256-mZWP9yF1O4knCiXx8CqolnS+93bM+hTQy40cd0HZmwI=";
+      };
+      commit_date = "2023-01-05";
+      patches = [
+        # Changes to the GNAT frontend: https://github.com/AdaCore/spark2014/issues/58
+        ./0003-Adjust-after-category-change-for-N_Formal_Package_De.patch
+      ];
+    };
+    "14" = {
+      src = fetchSpark2014 {
+        rev = "ce5fad038790d5dc18f9b5345dc604f1ccf45b06"; # branch fsf-14
+        hash = "sha256-WprJJIe/GpcdabzR2xC2dAV7kIYdNTaTpNYoR3UYTVo=";
+      };
+      patches = [
+        # Disable Coq related targets which are missing in the fsf-14 branch
+        ./0001-fix-install.patch
+
+        # Suppress warnings on aarch64: https://github.com/AdaCore/spark2014/issues/54
+        ./0002-mute-aarch64-warnings.patch
+
+        # Changes to the GNAT frontend: https://github.com/AdaCore/spark2014/issues/58
+        ./0003-Adjust-after-category-change-for-N_Formal_Package_De.patch
+      ];
+      commit_date = "2024-01-11";
+    };
+  };
+
+  thisSpark =
+    spark2014.${gnat_version}
+      or (throw "GNATprove depends on a specific GNAT version and can't be built using GNAT ${gnat_version}.");
+
+in
+stdenv.mkDerivation {
+  pname = "gnatprove";
+  version = "fsf-${gnat_version}_${thisSpark.commit_date}";
+
+  src = thisSpark.src;
+
+  patches = thisSpark.patches or [ ];
+
+  nativeBuildInputs = [
+    gnat
+    gprbuild
+    python3
+    makeWrapper
+  ]
+  ++ (with ocamlPackages; [
+    ocaml
+    findlib
+    menhir
+  ]);
+
+  buildInputs = [
+    gnatcoll-core
+  ]
+  ++ (with ocamlPackages; [
+    ocamlgraph
+    zarith
+    ppx_deriving
+    ppx_sexp_conv
+    camlzip
+    menhirLib
+    num
+    re
+    sexplib
+    yojson
+  ])
+  ++ (lib.optionals (gnat_version == "14") [
+    gpr2_24_2_next
+  ]);
+
+  propagatedBuildInputs = [
+    gprbuild
+  ];
+
+  postPatch = ''
+    # gnat2why/gnat_src points to the GNAT sources
+    tar xf ${gnat.cc.src} --wildcards 'gcc-*/gcc/ada'
+    mv gcc-*/gcc/ada gnat2why/gnat_src
+  '';
+
+  configurePhase = ''
+    runHook preConfigure
+    make setup
+    runHook postConfigure
+  '';
+
+  installPhase = ''
+    runHook preInstall
+    make install-all
+    cp -a ./install/. $out
+    mkdir $out/share/gpr
+    ln -s $out/lib/gnat/* $out/share/gpr/
+    runHook postInstall
+  '';
+
+  meta = with lib; {
+    description = "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;
+  };
+}