isabelle: 2013 -> 2014, plus add darwin support
This commit is contained in:
parent
f96684c71a
commit
db690f28a3
@ -2,24 +2,30 @@
|
||||
# nettools needed for hostname
|
||||
|
||||
let
|
||||
dirname = "Isabelle2013";
|
||||
dirname = "Isabelle2014";
|
||||
theories = ["HOL" "FOL" "ZF"];
|
||||
in
|
||||
|
||||
stdenv.mkDerivation {
|
||||
name = "isabelle-2013";
|
||||
name = "isabelle-2014";
|
||||
inherit dirname theories;
|
||||
|
||||
src = fetchurl {
|
||||
url = http://isabelle.in.tum.de/dist/Isabelle2013_linux.tar.gz;
|
||||
sha256 = "0l17s41hwzma0q2glpxrzic8i6mqd9b7awlpwhz0jkli7fj6ny7b";
|
||||
};
|
||||
src = if stdenv.isDarwin
|
||||
then fetchurl {
|
||||
url = http://isabelle.in.tum.de/dist/Isabelle2014_macos.tar.gz;
|
||||
sha256 = "1aa3vz2nnkkyd4mlsqbs69jqfxlll5h0k5fj9m1j9wqiddqwvwcf";
|
||||
}
|
||||
else fetchurl {
|
||||
url = http://isabelle.in.tum.de/dist/Isabelle2014_linux.tar.gz;
|
||||
sha256 = "0l17s41hwzma0q2glpxrzic8i6mqd9b7awlpwhz0jkli7fj6ny7b";
|
||||
};
|
||||
|
||||
buildInputs = [ perl polyml nettools ];
|
||||
buildInputs = [ perl polyml ]
|
||||
++ stdenv.lib.optional (!stdenv.isDarwin) nettools;
|
||||
|
||||
sourceRoot = dirname;
|
||||
|
||||
patches = [ ./settings.patch ];
|
||||
patches = stdenv.lib.optionals (!stdenv.isDarwin) [ ./settings.patch ];
|
||||
|
||||
postPatch = ''
|
||||
ENV=$(type -p env)
|
||||
@ -28,22 +34,20 @@ stdenv.mkDerivation {
|
||||
--replace /usr/bin/env $ENV
|
||||
substituteInPlace lib/Tools/install \
|
||||
--replace /usr/bin/env $ENV
|
||||
substituteInPlace src/Pure/IsaMakefile \
|
||||
--replace /bin/bash /bin/sh
|
||||
substituteInPlace etc/settings \
|
||||
--subst-var-by ML_HOME "${polyml}/bin" \
|
||||
--subst-var-by PROOFGENERAL_HOME "${proofgeneral}/share/emacs/site-lisp/ProofGeneral"
|
||||
'';
|
||||
|
||||
buildPhase = ''
|
||||
./build $theories
|
||||
./bin/isabelle build -s $theories
|
||||
'';
|
||||
|
||||
installPhase = ''
|
||||
mkdir -p $out/bin
|
||||
mv $TMP/$dirname $out
|
||||
cd $out/$dirname
|
||||
bin/isabelle install -p $out/bin
|
||||
bin/isabelle install $out/bin
|
||||
'';
|
||||
|
||||
meta = {
|
||||
@ -56,5 +60,6 @@ stdenv.mkDerivation {
|
||||
'';
|
||||
homepage = http://isabelle.in.tum.de/;
|
||||
license = "LGPL";
|
||||
maintainers = [ stdenv.lib.maintainers.jwiegley ];
|
||||
};
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user