tjh.dev
Clone of https://github.com/NixOS/nixpkgs.git (to stress-test knotserver)
1{
2 stdenv,
3 lib,
4 fetchFromGitHub,
5 gnat,
6 gnatcoll-core,
7 gprbuild,
8 python3,
9 ocamlPackages,
10 makeWrapper,
11 gpr2,
12}:
13let
14 gnat_version = lib.versions.major gnat.version;
15
16 # gnatprove fsf-14 requires gpr2 from a special branch
17 gpr2_24_2_next =
18 (gpr2.override {
19 # pregenerated kb db is not included
20 gpr2kbdir = "${gprbuild}/share/gprconfig";
21 }).overrideAttrs
22 (old: rec {
23 version = "24.2.0-next";
24 src = fetchFromGitHub {
25 owner = "AdaCore";
26 repo = "gpr";
27 rev = "v${version}";
28 hash = "sha256-Tp+N9VLKjVWs1VRPYE0mQY3rl4E5iGb8xDoNatEYBg4=";
29 };
30 });
31
32 fetchSpark2014 =
33 { rev, hash }:
34 fetchFromGitHub {
35 owner = "AdaCore";
36 repo = "spark2014";
37 fetchSubmodules = true;
38 inherit rev hash;
39 };
40
41 spark2014 = {
42 "12" = {
43 src = fetchSpark2014 {
44 rev = "ab34e07080a769b63beacc141707b5885c49d375"; # branch fsf-12
45 hash = "sha256-7pe3eWitpxmqzjW6qEIEuN0qr2IR+kJ7Ssc9pTBcCD8=";
46 };
47 commit_date = "2022-05-25";
48 };
49 "13" = {
50 src = fetchSpark2014 {
51 rev = "12db22e854defa9d1c993ef904af1e72330a68ca"; # branch fsf-13
52 hash = "sha256-mZWP9yF1O4knCiXx8CqolnS+93bM+hTQy40cd0HZmwI=";
53 };
54 commit_date = "2023-01-05";
55 };
56 "14" = {
57 src = fetchSpark2014 {
58 rev = "ce5fad038790d5dc18f9b5345dc604f1ccf45b06"; # branch fsf-14
59 hash = "sha256-WprJJIe/GpcdabzR2xC2dAV7kIYdNTaTpNYoR3UYTVo=";
60 };
61 patches = [
62 # Disable Coq related targets which are missing in the fsf-14 branch
63 ./0001-fix-install.patch
64
65 # Suppress warnings on aarch64: https://github.com/AdaCore/spark2014/issues/54
66 ./0002-mute-aarch64-warnings.patch
67
68 # Changes to the GNAT frontend: https://github.com/AdaCore/spark2014/issues/58
69 ./0003-Adjust-after-category-change-for-N_Formal_Package_De.patch
70 ];
71 commit_date = "2024-01-11";
72 };
73 };
74
75 thisSpark =
76 spark2014.${gnat_version}
77 or (builtins.throw "GNATprove depends on a specific GNAT version and can't be built using GNAT ${gnat_version}.");
78
79in
80stdenv.mkDerivation {
81 pname = "gnatprove";
82 version = "fsf-${gnat_version}_${thisSpark.commit_date}";
83
84 src = thisSpark.src;
85
86 patches = thisSpark.patches or [ ];
87
88 nativeBuildInputs = [
89 gnat
90 gprbuild
91 python3
92 makeWrapper
93 ]
94 ++ (with ocamlPackages; [
95 ocaml
96 findlib
97 menhir
98 ]);
99
100 buildInputs = [
101 gnatcoll-core
102 ]
103 ++ (with ocamlPackages; [
104 ocamlgraph
105 zarith
106 ppx_deriving
107 ppx_sexp_conv
108 camlzip
109 menhirLib
110 num
111 re
112 sexplib
113 yojson
114 ])
115 ++ (lib.optionals (gnat_version == "14") [
116 gpr2_24_2_next
117 ]);
118
119 propagatedBuildInputs = [
120 gprbuild
121 ];
122
123 postPatch = ''
124 # gnat2why/gnat_src points to the GNAT sources
125 tar xf ${gnat.cc.src} --wildcards 'gcc-*/gcc/ada'
126 mv gcc-*/gcc/ada gnat2why/gnat_src
127 '';
128
129 configurePhase = ''
130 runHook preConfigure
131 make setup
132 runHook postConfigure
133 '';
134
135 installPhase = ''
136 runHook preInstall
137 make install-all
138 cp -a ./install/. $out
139 mkdir $out/share/gpr
140 ln -s $out/lib/gnat/* $out/share/gpr/
141 runHook postInstall
142 '';
143
144 meta = with lib; {
145 description = "Software development technology specifically designed for engineering high-reliability applications";
146 homepage = "https://github.com/AdaCore/spark2014";
147 maintainers = [ maintainers.jiegec ];
148 license = licenses.gpl3;
149 platforms = platforms.all;
150 };
151}