Commit 20fab5e2 authored by Thomas Heijligen's avatar Thomas Heijligen Committed by jopejoe1
Browse files

gnatPackages.gnatprove: Add fsf-15 version

parent e3089453

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

0 → 100644
+35 −0
Original line number Diff line number Diff line 
From fc15667c867a96887c8c37faf9cc7480f04e6bc5 Mon Sep 17 00:00:00 2001

From: Thomas Heijligen <src@posteo.de>

Date: Mon, 2 Jun 2025 14:52:57 +0200

Subject: [PATCH] fix install



---

 Makefile | 12 ++++++------

 1 file changed, 6 insertions(+), 6 deletions(-)



diff --git a/Makefile b/Makefile

index 03a1da5c31..b70fbec613 100644

--- a/Makefile

+++ b/Makefile

@@ -107,12 +107,12 @@ 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/*.gpr.templ $(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/*.gpr.templ $(LIBDIR)

+	#$(CP) include/proof $(LIBDIR)

 

 doc: $(DOC)

 

-- 

2.49.0

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

+19 −1
Original line number Diff line number Diff line
@@ -29,6 +29,10 @@ let 
        };

      });



  # TODO:

  # Build why3 (github.com/AdaCore/why3) as separate package and not as submodule.

  # The relevant tags on why3 may get changed without the submodule pointer being updated.



  fetchSpark2014 =

    { rev, hash }:

    fetchFromGitHub {
@@ -64,7 +68,7 @@ let 
      };

      patches = [

        # Disable Coq related targets which are missing in the fsf-14 branch

        ./0001-fix-install.patch

        ./0001-fix-install-fsf-14.patch



        # Suppress warnings on aarch64: https://github.com/AdaCore/spark2014/issues/54

        ./0002-mute-aarch64-warnings.patch
@@ -74,6 +78,17 @@ let 
      ];

      commit_date = "2024-01-11";

    };

    "15" = {

      src = fetchSpark2014 {

        rev = "22bf1510e0829ba74f9d8d686badb65c7365ee91";

        hash = "sha256-KjAWMgMT3Tp/s/DQ20ZZajty9Zrv8aPFocwgv5LkjSw=";

      };

      patches = [

        # Disable Coq related targets which are missing in the fsf-15 branch

        ./0001-fix-install-fsf-15.patch

      ];

      commit_date = "2025-06-10";

    };

  };



  thisSpark =
@@ -118,6 +133,9 @@ stdenv.mkDerivation { 
  ])

  ++ (lib.optionals (gnat_version == "14") [

    gpr2_24_2_next

  ])

  ++ (lib.optionals (gnat_version == "15") [

    gpr2

  ]);



  propagatedBuildInputs = [