Merge pull request #13387 from gebner/isabelle2016
isabelle: 2015 -> 2016
This commit is contained in:
commit
960122179a
@ -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,7 +1,7 @@
|
|||||||
{stdenv, fetchurl, autoreconfHook}:
|
{stdenv, fetchurl, autoreconfHook}:
|
||||||
|
|
||||||
let
|
let
|
||||||
version = "5.5.2";
|
version = "5.6";
|
||||||
in
|
in
|
||||||
|
|
||||||
stdenv.mkDerivation {
|
stdenv.mkDerivation {
|
||||||
@ -15,7 +15,7 @@ stdenv.mkDerivation {
|
|||||||
|
|
||||||
src = fetchurl {
|
src = fetchurl {
|
||||||
url = "mirror://sourceforge/polyml/polyml.${version}.tar.gz";
|
url = "mirror://sourceforge/polyml/polyml.${version}.tar.gz";
|
||||||
sha256 = "10m680qdad6bd50bav9xjsgmsxw8yxg55vr7grbg0gvykzl2pzbk";
|
sha256 = "05d6l2a5m9jf32a8kahwg2p2ph4x9rjf1nsl83331q3gwn5bkmr0";
|
||||||
};
|
};
|
||||||
|
|
||||||
meta = {
|
meta = {
|
||||||
|
@ -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;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user