Commit 6af36c50 authored by Thomas Heijligen's avatar Thomas Heijligen Committed by sternenseemann
Browse files

gnatPackages.gnatprove: Add fsf-14 version 



- gpr2 is required as buildInput, but in a special version
- fsf-14 drops SPARKlib from the tree, but the Makefile still expect it, patch it out

Co-authored-by: default avatarsternenseemann <sternenseemann@systemli.org>
parent 066b51bf

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

0 → 100644
+33 −0
Original line number Diff line number Diff line 
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/default.nix

+27 −0
Original line number Diff line number Diff line
@@ -7,10 +7,22 @@ 
, 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.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";
@@ -33,6 +45,17 @@ let 
      };

      commit_date = "2023-01-05";

    };

    "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

      ];

      commit_date = "2024-01-11";

    };

  };



  thisSpark = spark2014.${gnat_version} or
@@ -45,6 +68,8 @@ stdenv.mkDerivation rec { 


  src = thisSpark.src;



  patches = thisSpark.patches or [];



  nativeBuildInputs = [

    gnat

    gprbuild
@@ -69,6 +94,8 @@ stdenv.mkDerivation rec { 
    re

    sexplib

    yojson

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

    gpr2_24_2_next

  ]);



  propagatedBuildInputs = [