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
|
{ lib, stdenv, fetchurl, coreutils, nettools, java, scala, polyml, z3, veriT, vampire, eprover-ho, naproche, rlwrap, perl, makeDesktopItem, isabelle-components, isabelle, symlinkJoin, fetchhg }:
# nettools needed for hostname
let
sha1 = stdenv.mkDerivation {
pname = "isabelle-sha1";
version = "2021-1";
src = fetchhg {
url = "https://isabelle.sketis.net/repos/sha1";
rev = "e0239faa6f42";
sha256 = "sha256-4sxHzU/ixMAkSo67FiE6/ZqWJq9Nb9OMNhMoXH2bEy4=";
};
buildPhase = (if stdenv.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 rec {
pname = "isabelle";
version = "2021-1";
dirname = "Isabelle${version}";
src =
if stdenv.isDarwin
then
fetchurl
{
url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz";
sha256 = "0n1ls9vwf0ps1x8zpb7c1xz1wkasgvc34h5bz280hy2z6iqwmwbc";
}
else
fetchurl {
url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz";
sha256 = "0jfaqckhg388jh9b4msrpkv6wrd6xzlw18m0bngbby8k8ywalp9i";
};
buildInputs = [ polyml z3 veriT vampire eprover-ho nettools ]
++ lib.optionals (!stdenv.isDarwin) [ java ];
sourceRoot = "${dirname}${lib.optionalString stdenv.isDarwin ".app"}";
postUnpack = if stdenv.isDarwin then ''
mv $sourceRoot ${dirname}
sourceRoot=${dirname}
'' else null;
postPatch = ''
patchShebangs .
cat >contrib/z3*/etc/settings <<EOF
Z3_HOME=${z3}
Z3_VERSION=${z3.version}
Z3_SOLVER=${z3}/bin/z3
Z3_INSTALLED=yes
EOF
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
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/z3-* contrib/verit-* contrib/vampire-* contrib/e-*; do
rm -rf $comp/x86*
done
substituteInPlace lib/Tools/env \
--replace /usr/bin/env ${coreutils}/bin/env
substituteInPlace src/Tools/Setup/src/Environment.java \
--replace 'cmd.add("/usr/bin/env");' "" \
--replace 'cmd.add("bash");' "cmd.add(\"$SHELL\");"
substituteInPlace src/Pure/General/sha1.ML \
--replace '"$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 'ISABELLE_APPLE_PLATFORM64=arm64-darwin' ""
'' + (if ! stdenv.isLinux then "" else ''
arch=${if stdenv.hostPlatform.system == "x86_64-linux" then "x86_64-linux" else "x86-linux"}
for f in contrib/*/$arch/{bash_process,epclextract,nunchaku,SPASS,zipperposition}; do
patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f"
done
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
'');
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
${java}/bin/javac -d "$TARGET_DIR" -classpath ${scala}/lib/scala-compiler.jar "''${ARGS[@]}"
${java}/bin/jar -c -f "$TARGET_DIR/isabelle_setup.jar" -e "isabelle.setup.Setup" -C "$TARGET_DIR" isabelle
rm -rf "$TARGET_DIR/isabelle"
# Prebuild HOL Session
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;
};
} // {
withComponents = f:
let
base = "$out/${isabelle.dirname}";
components = f isabelle-components;
in symlinkJoin {
name = "isabelle-with-components-${isabelle.version}";
paths = [ 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;
};
}
|