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