From 9c954c604fe66acbb1b3f8f435514bff66e6bd7e Mon Sep 17 00:00:00 2001 From: jayay Date: Sun, 16 Mar 2025 17:53:51 +0100 Subject: [PATCH 1/2] gprbuild: add compiler configuration for aarch64-unknown-linux-gnu Fixes gprbuild to find `ar`, `cr` and `nm` for native aarch64-linux compilation of Ada projects. --- .../ada-modules/gprbuild/nixpkgs-gnat.xml | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) 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; + + From 5f7505bb23f6089f359979baa4bb1e520139f925 Mon Sep 17 00:00:00 2001 From: jayay Date: Sat, 22 Mar 2025 17:31:45 +0100 Subject: [PATCH 2/2] gnatprove: mute warnings about type conversion for aarch64 --- .../0002-mute-aarch64-warnings.patch | 22 +++++++++++++++++++ .../ada-modules/gnatprove/default.nix | 3 +++ 2 files changed, 25 insertions(+) create mode 100644 pkgs/development/ada-modules/gnatprove/0002-mute-aarch64-warnings.patch 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"; };