tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
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 # TODO:
33 # Build why3 (github.com/AdaCore/why3) as separate package and not as submodule.
34 # The relevant tags on why3 may get changed without the submodule pointer being updated.
35
36 fetchSpark2014 =
37 { rev, hash }:
38 fetchFromGitHub {
39 owner = "AdaCore";
40 repo = "spark2014";
41 fetchSubmodules = true;
42 inherit rev hash;
43 };
44
45 spark2014 = {
46 "12" = {
47 src = fetchSpark2014 {
48 rev = "ab34e07080a769b63beacc141707b5885c49d375"; # branch fsf-12
49 hash = "sha256-7pe3eWitpxmqzjW6qEIEuN0qr2IR+kJ7Ssc9pTBcCD8=";
50 };
51 commit_date = "2022-05-25";
52 };
53 "13" = {
54 src = fetchSpark2014 {
55 rev = "12db22e854defa9d1c993ef904af1e72330a68ca"; # branch fsf-13
56 hash = "sha256-mZWP9yF1O4knCiXx8CqolnS+93bM+hTQy40cd0HZmwI=";
57 };
58 commit_date = "2023-01-05";
59 patches = [
60 # Changes to the GNAT frontend: https://github.com/AdaCore/spark2014/issues/58
61 ./0003-Adjust-after-category-change-for-N_Formal_Package_De.patch
62 ];
63 };
64 "14" = {
65 src = fetchSpark2014 {
66 rev = "ce5fad038790d5dc18f9b5345dc604f1ccf45b06"; # branch fsf-14
67 hash = "sha256-WprJJIe/GpcdabzR2xC2dAV7kIYdNTaTpNYoR3UYTVo=";
68 };
69 patches = [
70 # Disable Coq related targets which are missing in the fsf-14 branch
71 ./0001-fix-install-fsf-14.patch
72
73 # Suppress warnings on aarch64: https://github.com/AdaCore/spark2014/issues/54
74 ./0002-mute-aarch64-warnings.patch
75
76 # Changes to the GNAT frontend: https://github.com/AdaCore/spark2014/issues/58
77 ./0003-Adjust-after-category-change-for-N_Formal_Package_De.patch
78 ];
79 commit_date = "2024-01-11";
80 };
81 "15" = {
82 src = fetchSpark2014 {
83 rev = "22bf1510e0829ba74f9d8d686badb65c7365ee91";
84 hash = "sha256-KjAWMgMT3Tp/s/DQ20ZZajty9Zrv8aPFocwgv5LkjSw=";
85 };
86 patches = [
87 # Disable Coq related targets which are missing in the fsf-15 branch
88 ./0001-fix-install-fsf-15.patch
89 ];
90 commit_date = "2025-06-10";
91 };
92 };
93
94 thisSpark =
95 spark2014.${gnat_version}
96 or (throw "GNATprove depends on a specific GNAT version and can't be built using GNAT ${gnat_version}.");
97
98in
99stdenv.mkDerivation {
100 pname = "gnatprove";
101 version = "fsf-${gnat_version}_${thisSpark.commit_date}";
102
103 src = thisSpark.src;
104
105 patches = thisSpark.patches or [ ];
106
107 nativeBuildInputs = [
108 gnat
109 gprbuild
110 python3
111 makeWrapper
112 ]
113 ++ (with ocamlPackages; [
114 ocaml
115 findlib
116 menhir
117 ]);
118
119 buildInputs = [
120 gnatcoll-core
121 ]
122 ++ (with ocamlPackages; [
123 ocamlgraph
124 zarith
125 ppx_deriving
126 ppx_sexp_conv
127 camlzip
128 menhirLib
129 num
130 re
131 sexplib
132 yojson_2
133 ])
134 ++ (lib.optionals (gnat_version == "14") [
135 gpr2_24_2_next
136 ])
137 ++ (lib.optionals (gnat_version == "15") [
138 gpr2
139 ]);
140
141 propagatedBuildInputs = [
142 gprbuild
143 ];
144
145 postPatch = ''
146 # gnat2why/gnat_src points to the GNAT sources
147 tar xf ${gnat.cc.src} --wildcards 'gcc-*/gcc/ada'
148 mv gcc-*/gcc/ada gnat2why/gnat_src
149 '';
150
151 configurePhase = ''
152 runHook preConfigure
153 make setup
154 runHook postConfigure
155 '';
156
157 installPhase = ''
158 runHook preInstall
159 make install-all
160 cp -a ./install/. $out
161 mkdir $out/share/gpr
162 ln -s $out/lib/gnat/* $out/share/gpr/
163 runHook postInstall
164 '';
165
166 meta = {
167 description = "Software development technology specifically designed for engineering high-reliability applications";
168 homepage = "https://github.com/AdaCore/spark2014";
169 maintainers = [ lib.maintainers.jiegec ];
170 license = lib.licenses.gpl3;
171 platforms = lib.platforms.all;
172 };
173}