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
|
{ lib, stdenv, fetchurl, coreutils, nettools, java, scala, polyml, z3, veriT, vampire, eprover-ho, naproche, rlwrap, perl, makeDesktopItem, isabelle-components, isabelle, symlinkJoin }:
# nettools needed for hostname
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 ]
++ lib.optionals (!stdenv.isDarwin) [ nettools java ];
sourceRoot = dirname;
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\");"
rm -r heaps
'' + (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/";
license = licenses.bsd3;
maintainers = [ maintainers.jwiegley maintainers.jvanbruegge ];
platforms = platforms.linux;
};
} // {
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;
};
}
|