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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
|
{ lib
, stdenv
, fetchurl
, coreutils
, nettools
, java
, scala_3
, polyml
, veriT
, vampire
, eprover-ho
, naproche
, rlwrap
, perl
, procps
, makeDesktopItem
, isabelle-components
, symlinkJoin
, fetchhg
}:
let
sha1 = stdenv.mkDerivation {
pname = "isabelle-sha1";
version = "2024";
src = fetchhg {
url = "https://isabelle.sketis.net/repos/sha1";
rev = "0ce12663fe76";
hash = "sha256-DB/ETVZhbT82IMZA97TmHG6gJcGpFavxDKDTwPzIF80=";
};
buildPhase = (if stdenv.hostPlatform.isDarwin then ''
LDFLAGS="-dynamic -undefined dynamic_lookup -lSystem"
'' else ''
LDFLAGS="-fPIC -shared"
'') + ''
CFLAGS="-fPIC -I."
$CC $CFLAGS -c sha1.c -o sha1.o
$LD $LDFLAGS sha1.o -o libsha1.so
'';
installPhase = ''
mkdir -p $out/lib
cp libsha1.so $out/lib/
'';
};
in stdenv.mkDerivation (finalAttrs: rec {
pname = "isabelle";
version = "2024";
dirname = "Isabelle${version}";
src =
if stdenv.hostPlatform.isDarwin
then
fetchurl
{
url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz";
hash = "sha256-IgNfmW9x6h8DBj9vFEGV62oEl01NkW7QdyzXlWmii8c=";
}
else if stdenv.hostPlatform.isx86
then
fetchurl {
url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz";
hash = "sha256-YDqq+KvqNll687BlHSwWKobAoN1EIHZvR+VyQDljkmc=";
}
else
fetchurl {
url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux_arm.tar.gz";
hash = "sha256-jXWVv18WwrVnqVX1s4Lnyf7DkOzPa3EdLXYxgtKD+YA=";
};
nativeBuildInputs = [ java ];
buildInputs = [ polyml veriT vampire eprover-ho nettools ]
++ lib.optionals (!stdenv.hostPlatform.isDarwin) [ java procps ];
sourceRoot = "${dirname}${lib.optionalString stdenv.hostPlatform.isDarwin ".app"}";
doCheck = stdenv.hostPlatform.system != "aarch64-linux";
checkPhase = "bin/isabelle build -v HOL-SMT_Examples";
postUnpack = lib.optionalString stdenv.hostPlatform.isDarwin ''
mv $sourceRoot ${dirname}
sourceRoot=${dirname}
'';
postPatch = ''
patchShebangs lib/Tools/ bin/
cat >contrib/verit-*/etc/settings <<EOF
ISABELLE_VERIT=${veriT}/bin/veriT
EOF
cat >contrib/e-*/etc/settings <<EOF
E_HOME=${eprover-ho}/bin
E_VERSION=${eprover-ho.version}
EOF
cat >contrib/vampire-*/etc/settings <<EOF
VAMPIRE_HOME=${vampire}/bin
VAMPIRE_VERSION=${vampire.version}
VAMPIRE_EXTRA_OPTIONS="--mode casc"
EOF
cat >contrib/polyml-*/etc/settings <<EOF
ML_SYSTEM_64=true
ML_SYSTEM=${polyml.name}
ML_PLATFORM=${stdenv.system}
ML_HOME=${polyml}/bin
ML_OPTIONS="--minheap 1000"
POLYML_HOME="\$COMPONENT"
ML_SOURCES="\$POLYML_HOME/src"
EOF
cat >contrib/jdk*/etc/settings <<EOF
ISABELLE_JAVA_PLATFORM=${stdenv.system}
ISABELLE_JDK_HOME=${java}
EOF
'' + lib.optionalString stdenv.hostPlatform.isx86 ''
rm contrib/naproche-*/x86*/Naproche-SAD
ln -s ${naproche}/bin/Naproche-SAD contrib/naproche-*/x86*/
'' + ''
echo ISABELLE_LINE_EDITOR=${rlwrap}/bin/rlwrap >>etc/settings
for comp in contrib/jdk* contrib/polyml-* contrib/verit-* contrib/vampire-* contrib/e-*; do
rm -rf $comp/${if stdenv.hostPlatform.isx86 then "x86" else "arm"}*
done
substituteInPlace lib/Tools/env \
--replace-fail /usr/bin/env ${coreutils}/bin/env
substituteInPlace src/Tools/Setup/src/Environment.java \
--replace-fail 'cmd.add("/usr/bin/env");' "" \
--replace-fail 'cmd.add("bash");' "cmd.add(\"$SHELL\");"
substituteInPlace src/Pure/General/sha1.ML \
--replace-fail '"$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so")' '"${sha1}/lib/libsha1.so"'
rm -r heaps
'' + lib.optionalString (stdenv.hostPlatform.system == "x86_64-darwin") ''
substituteInPlace lib/scripts/isabelle-platform \
--replace-fail 'ISABELLE_APPLE_PLATFORM64=arm64-darwin' ""
'' + lib.optionalString stdenv.hostPlatform.isLinux ''
arch=${if stdenv.hostPlatform.system == "aarch64-linux" then "arm64-linux" else stdenv.hostPlatform.system}
for f in contrib/*/$arch/{z3,nunchaku,spass,zipperposition}; do
patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f"${lib.optionalString stdenv.hostPlatform.isAarch64 " || true"}
done
patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) contrib/bash_process-*/$arch/bash_process
for d in contrib/kodkodi-*/jni/$arch; do
patchelf --set-rpath "${lib.concatStringsSep ":" [ "${java}/lib/openjdk/lib/server" "${stdenv.cc.cc.lib}/lib" ]}" $d/*.so
done
'' + lib.optionalString (stdenv.hostPlatform.system == "x86_64-linux") ''
patchelf --set-rpath "${stdenv.cc.cc.lib}/lib" contrib/z3-*/$arch/z3
'';
buildPhase = ''
export HOME=$TMP # The build fails if home is not set
setup_name=$(basename contrib/isabelle_setup*)
#The following is adapted from https://isabelle.sketis.net/repos/isabelle/file/Isabelle2021-1/Admin/lib/Tools/build_setup
TARGET_DIR="contrib/$setup_name/lib"
rm -rf "$TARGET_DIR"
mkdir -p "$TARGET_DIR/isabelle/setup"
declare -a ARGS=("-Xlint:unchecked")
SOURCES="$(${perl}/bin/perl -e 'while (<>) { if (m/(\S+\.java)/) { print "$1 "; } }' "src/Tools/Setup/etc/build.props")"
for SRC in $SOURCES
do
ARGS["''${#ARGS[@]}"]="src/Tools/Setup/$SRC"
done
echo "Building isabelle setup"
javac -d "$TARGET_DIR" -classpath "${scala_3.bare}/lib/scala3-interfaces-${scala_3.version}.jar:${scala_3.bare}/lib/scala3-compiler_3-${scala_3.version}.jar" "''${ARGS[@]}"
jar -c -f "$TARGET_DIR/isabelle_setup.jar" -e "isabelle.setup.Setup" -C "$TARGET_DIR" isabelle
rm -rf "$TARGET_DIR/isabelle"
echo "Building HOL heap"
bin/isabelle build -v -o system_heaps -b HOL
'';
installPhase = ''
mkdir -p $out/bin
mv $TMP/$dirname $out
cd $out/$dirname
bin/isabelle install $out/bin
# icon
mkdir -p "$out/share/icons/hicolor/isabelle/apps"
cp "$out/Isabelle${version}/lib/icons/isabelle.xpm" "$out/share/icons/hicolor/isabelle/apps/"
# desktop item
mkdir -p "$out/share"
cp -r "${desktopItem}/share/applications" "$out/share/applications"
'';
desktopItem = makeDesktopItem {
name = "isabelle";
exec = "isabelle jedit";
icon = "isabelle";
desktopName = "Isabelle";
comment = meta.description;
categories = [ "Education" "Science" "Math" ];
};
meta = with lib; {
description = "A generic proof assistant";
longDescription = ''
Isabelle is a generic proof assistant. It allows mathematical formulas
to be expressed in a formal language and provides tools for proving those
formulas in a logical calculus.
'';
homepage = "https://isabelle.in.tum.de/";
sourceProvenance = with sourceTypes; [
fromSource
binaryNativeCode # source bundles binary dependencies
];
license = licenses.bsd3;
maintainers = [ maintainers.jwiegley maintainers.jvanbruegge ];
platforms = platforms.unix;
broken = stdenv.hostPlatform.isDarwin;
};
passthru.withComponents = f:
let
isabelle = finalAttrs.finalPackage;
base = "$out/${isabelle.dirname}";
components = f isabelle-components;
in symlinkJoin {
name = "isabelle-with-components-${isabelle.version}";
paths = [ isabelle ] ++ (builtins.map (c: c.override { inherit isabelle; }) components);
postBuild = ''
rm $out/bin/*
cd ${base}
rm bin/*
cp ${isabelle}/${isabelle.dirname}/bin/* bin/
rm etc/components
cat ${isabelle}/${isabelle.dirname}/etc/components > etc/components
export HOME=$TMP
bin/isabelle install $out/bin
patchShebangs $out/bin
'' + lib.concatMapStringsSep "\n" (c: ''
echo contrib/${c.pname}-${c.version} >> ${base}/etc/components
'') components;
};
})
|
