public/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

isabelle: 2015 -> 2016

Browse Source
This commit is contained in:
Gabriel Ebner 2016-02-23 14:19:13 +01:00
parent 151fd89ba0
commit 87b0a41ac5
2 changed files with 12 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
pkgs/applications/science/logic/isabelle/default.nix
View File

@ -1,23 +1,23 @@
{ stdenv, fetchurl, perl, nettools, java, polyml, proofgeneral }: { stdenv, fetchurl, perl, nettools, java, polyml }:
# nettools needed for hostname # nettools needed for hostname
let let
dirname = "Isabelle2015"; dirname = "Isabelle2016";
theories = ["HOL" "FOL" "ZF"]; theories = ["HOL" "FOL" "ZF"];
in in
stdenv.mkDerivation { stdenv.mkDerivation {
name = "isabelle-2015"; name = "isabelle-2016";
inherit dirname theories; inherit dirname theories;
src = if stdenv.isDarwin src = if stdenv.isDarwin
then fetchurl { then fetchurl {
url = http://isabelle.in.tum.de/dist/Isabelle2015.dmg; url = "http://isabelle.in.tum.de/website-${dirname}/dist/${dirname}.dmg";
sha256 = "1vhm10qc1rn3wy9r12clrl33p64h3q1aj41mcnxkbnsyg2bx03im"; sha256 = "0wawf0cjc52h8hif1867p33qhlh6qz0fy5i2kr1gbf7psickd6iw";
} }
else fetchurl { else fetchurl {
url = http://isabelle.in.tum.de/dist/Isabelle2015_linux.tar.gz; url = "http://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz";
sha256 = "13kqm458d8mw7il1zg5bdb1nfbb869p331d75xzlm2v9xgjxx862"; sha256 = "0jh1qrsyib13fycymwvw7dq7xfy4iyplwq0s65ash842cdzkbxb4";
}; };
buildInputs = [ perl polyml ] buildInputs = [ perl polyml ]
@ -34,17 +34,14 @@ stdenv.mkDerivation {
--replace /usr/bin/env $ENV --replace /usr/bin/env $ENV
sed -i 's|isabelle_java java|${java}/bin/java|g' lib/Tools/java sed -i 's|isabelle_java java|${java}/bin/java|g' lib/Tools/java
substituteInPlace etc/settings \ substituteInPlace etc/settings \
--subst-var-by ML_HOME "${polyml}/bin" \ --subst-var-by ML_HOME "${polyml}/bin"
--subst-var-by PROOFGENERAL_HOME "${proofgeneral}/share/emacs/site-lisp/ProofGeneral"
substituteInPlace contrib/jdk/etc/settings \ substituteInPlace contrib/jdk/etc/settings \
--replace ISABELLE_JDK_HOME= '#ISABELLE_JDK_HOME=' --replace ISABELLE_JDK_HOME= '#ISABELLE_JDK_HOME='
substituteInPlace contrib/polyml-*/etc/settings \ substituteInPlace contrib/polyml-*/etc/settings \
--replace 'ML_HOME="$POLYML_HOME/$ML_PLATFORM"' \ --replace '$POLYML_HOME/$ML_PLATFORM' ${polyml}/bin \
"ML_HOME=\"${polyml}/bin\"" --replace '$POLYML_HOME/$PLATFORM/polyml' ${polyml}/bin/poly
''; substituteInPlace lib/scripts/run-polyml* lib/scripts/polyml-version \
--replace '$ML_HOME/poly' ${polyml}/bin/poly
buildPhase = ''
ISABELLE_JDK_HOME=${java} ./bin/isabelle build -s $theories
''; '';
installPhase = '' installPhase = ''

1
pkgs/top-level/all-packages.nix
View File

@ -15384,7 +15384,6 @@ let
tini = callPackage ../applications/virtualization/tini {}; tini = callPackage ../applications/virtualization/tini {};
isabelle = callPackage ../applications/science/logic/isabelle { isabelle = callPackage ../applications/science/logic/isabelle {
inherit (pkgs.emacs24Packages) proofgeneral;
java = if stdenv.isLinux then jre else jdk; java = if stdenv.isLinux then jre else jdk;
}; };