diff --git a/pkgs/development/ada-modules/gnatprove/0002-mute-aarch64-warnings.patch b/pkgs/development/ada-modules/gnatprove/0002-mute-aarch64-warnings.patch
new file mode 100644
index 000000000000..febe5daab9a4
--- /dev/null
+++ b/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;
diff --git a/pkgs/development/ada-modules/gnatprove/default.nix b/pkgs/development/ada-modules/gnatprove/default.nix
index 405e3bc1e944..a7af40beae30 100644
--- a/pkgs/development/ada-modules/gnatprove/default.nix
+++ b/pkgs/development/ada-modules/gnatprove/default.nix
@@ -56,6 +56,9 @@ let
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
];
commit_date = "2024-01-11";
};
diff --git a/pkgs/development/ada-modules/gprbuild/nixpkgs-gnat.xml b/pkgs/development/ada-modules/gprbuild/nixpkgs-gnat.xml
index ead88dc365c1..b7e5d180dc5a 100644
--- a/pkgs/development/ada-modules/gprbuild/nixpkgs-gnat.xml
+++ b/pkgs/development/ada-modules/gprbuild/nixpkgs-gnat.xml
@@ -53,4 +53,37 @@
+
+
+
+
+
+
+
+
+
+ for Archive_Builder use ("ar", "cr");
+ for Archive_Builder_Append_Option use ("q");
+ for Archive_Indexer use ("ranlib");
+ for Archive_Suffix use ".a";
+
+
+
+
+
+
+
+
+
+
+
+ for Object_Lister use ("nm", "-g");
+ for Object_Lister_Matcher use " [TDRBSG] (.*)";
+
+ package Linker is
+ for Export_File_Format use "GNU";
+ for Export_File_Switch use "-Wl,--version-script=";
+ end Linker;
+
+