summary refs log tree commit diff
path: root/pkgs/applications/science/logic/isabelle/default.nix
diff options
context:
space:
mode:
Diffstat (limited to 'pkgs/applications/science/logic/isabelle/default.nix')
-rw-r--r--pkgs/applications/science/logic/isabelle/default.nix36
1 files changed, 22 insertions, 14 deletions
diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix
index a7c1420cb54..88bbe820e2f 100644
--- a/pkgs/applications/science/logic/isabelle/default.nix
+++ b/pkgs/applications/science/logic/isabelle/default.nix
@@ -1,26 +1,30 @@
-{ stdenv, fetchurl, perl, nettools, polyml, proofgeneral }:
+{ stdenv, fetchurl, perl, nettools, java, polyml, proofgeneral }:
 # 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 = "0z81pwwllavka4r57fx6yi9kbpbb9xbanp8dsjix49qpyj2a72jy";
+    };
 
-  buildInputs = [ perl polyml nettools ];
+  buildInputs = [ perl polyml ]
+             ++ stdenv.lib.optionals (!stdenv.isDarwin) [ nettools java ];
 
   sourceRoot = dirname;
 
-  patches = [ ./settings.patch ];
-
   postPatch = ''
     ENV=$(type -p env)
     patchShebangs "."
@@ -28,22 +32,25 @@ 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"
+    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 = ''
-    ./build $theories
+    ISABELLE_JDK_HOME=${java} ./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 +63,6 @@ stdenv.mkDerivation {
     '';
     homepage = http://isabelle.in.tum.de/;
     license = "LGPL";
+    maintainers = [ stdenv.lib.maintainers.jwiegley ];
   };
 }