isabelle: Version 2014 building on Linux and Darwin
This commit is contained in:
parent
272c44f1a5
commit
10e215a3ae
@ -1,4 +1,4 @@
|
|||||||
{ stdenv, fetchurl, perl, nettools, polyml, proofgeneral }:
|
{ stdenv, fetchurl, perl, nettools, java, polyml, proofgeneral }:
|
||||||
# nettools needed for hostname
|
# nettools needed for hostname
|
||||||
|
|
||||||
let
|
let
|
||||||
@ -21,7 +21,7 @@ stdenv.mkDerivation {
|
|||||||
};
|
};
|
||||||
|
|
||||||
buildInputs = [ perl polyml ]
|
buildInputs = [ perl polyml ]
|
||||||
++ stdenv.lib.optional (!stdenv.isDarwin) nettools;
|
++ stdenv.lib.optionals (!stdenv.isDarwin) [ nettools java ];
|
||||||
|
|
||||||
sourceRoot = dirname;
|
sourceRoot = dirname;
|
||||||
|
|
||||||
@ -35,10 +35,15 @@ stdenv.mkDerivation {
|
|||||||
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"
|
--subst-var-by PROOFGENERAL_HOME "${proofgeneral}/share/emacs/site-lisp/ProofGeneral"
|
||||||
|
substituteInPlace contrib/jdk/etc/settings \
|
||||||
|
--replace ISABELLE_JDK_HOME= '#ISABELLE_JDK_HOME='
|
||||||
|
substituteInPlace contrib/polyml-5.5.2-1/etc/settings \
|
||||||
|
--replace 'ML_HOME="$POLYML_HOME/$ML_PLATFORM"' \
|
||||||
|
"ML_HOME=\"${polyml}/bin\""
|
||||||
'';
|
'';
|
||||||
|
|
||||||
buildPhase = ''
|
buildPhase = ''
|
||||||
./bin/isabelle build -s $theories
|
ISABELLE_JDK_HOME=${java} ./bin/isabelle build -s $theories
|
||||||
'';
|
'';
|
||||||
|
|
||||||
installPhase = ''
|
installPhase = ''
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
{stdenv, fetchurl}:
|
{stdenv, fetchurl}:
|
||||||
|
|
||||||
let
|
let
|
||||||
version = "5.5.1";
|
version = "5.5.2";
|
||||||
in
|
in
|
||||||
|
|
||||||
stdenv.mkDerivation {
|
stdenv.mkDerivation {
|
||||||
@ -9,7 +9,7 @@ stdenv.mkDerivation {
|
|||||||
|
|
||||||
src = fetchurl {
|
src = fetchurl {
|
||||||
url = "mirror://sourceforge/polyml/polyml.${version}.tar.gz";
|
url = "mirror://sourceforge/polyml/polyml.${version}.tar.gz";
|
||||||
sha256 = "16i0ir5mydl7381aijihkll19khp3z8dq0g2ja6k0pcbpkd0k06g";
|
sha256 = "10m680qdad6bd50bav9xjsgmsxw8yxg55vr7grbg0gvykzl2pzbk";
|
||||||
};
|
};
|
||||||
|
|
||||||
meta = {
|
meta = {
|
||||||
|
@ -11506,6 +11506,7 @@ let
|
|||||||
isabelle = import ../applications/science/logic/isabelle {
|
isabelle = import ../applications/science/logic/isabelle {
|
||||||
inherit (pkgs) stdenv fetchurl nettools perl polyml;
|
inherit (pkgs) stdenv fetchurl nettools perl polyml;
|
||||||
inherit (pkgs.emacs24Packages) proofgeneral;
|
inherit (pkgs.emacs24Packages) proofgeneral;
|
||||||
|
java = if stdenv.isLinux then jre else jdk;
|
||||||
};
|
};
|
||||||
|
|
||||||
iprover = callPackage ../applications/science/logic/iprover {};
|
iprover = callPackage ../applications/science/logic/iprover {};
|
||||||
|
Loading…
x
Reference in New Issue
Block a user