Add expression for Isabelle2009

svn path=/nixpkgs/trunk/; revision=18905

pkgs/applications/science/logic/isabelle/default.nix

@@ -0,0 +1,62 @@
+{ stdenv, fetchurl, perl, nettools, polyml, emacs, emacsPackages }:
+# nettools needed for hostname
+
+let
+  pname = "Isabelle";
+  version = "2009-1";
+  name = "${pname}${version}";
+  theories = ["HOL" "FOL" "ZF"];
+  proofgeneral = (emacsPackages emacs).proofgeneral;
+in
+
+stdenv.mkDerivation {
+  inherit name theories;
+
+  src = fetchurl {
+    url = "http://www.cl.cam.ac.uk/research/hvg/${pname}/dist/${name}.tar.gz";
+    sha256 = "43ad7794e8b4214b3ace49fc136a69ed6cc65ead02831ae6071f846ecbe56f68";
+  };
+
+  buildInputs = [ perl polyml nettools ];
+
+  sourceRoot = name;
+
+  patches = [ ./settings.patch ];
+
+  postPatch = ''
+    ENV=$(type -p env)
+    patchShebangs "."
+    substituteInPlace lib/Tools/env \
+      --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
+  '';
+
+  installPhase = ''
+    ensureDir $out/bin
+    mv $TMP/$name $out
+    cd $out/$name
+    bin/isabelle install -p $out/bin
+  '';
+
+  meta = {
+    description = "A generic proof assistant";
+
+    longDescription = ''
+      Isabelle is a generic proof assistant.  It allows mathematical formulas
+      to be expressed in a formal language and provides tools for proving those
+      formulas in a logical calculus.
+    '';
+    homepage = http://isabelle.in.tum.de/;
+    license = "LGPL";
+  };
+}

pkgs/applications/science/logic/isabelle/settings.patch

@@ -0,0 +1,35 @@
+diff -Naur Isabelle2009-1/etc/settings Isabelle2009-1-patched/etc/settings
+--- Isabelle2009-1/etc/settings	2009-12-02 12:04:07.000000000 +0100
++++ Isabelle2009-1-patched/etc/settings	2009-12-04 16:15:40.000000000 +0100
+@@ -16,15 +16,8 @@
+ # Only one of the sections below should be activated.
+ 
+ # Poly/ML 5.x (automated settings)
+-POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
+ ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform")
+-ML_HOME=$(choosefrom \
+-  "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
+-  "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
+-  "/usr/local/polyml/$ML_PLATFORM" \
+-  "/usr/share/polyml/$ML_PLATFORM" \
+-  "/opt/polyml/$ML_PLATFORM" \
+-  $POLY_HOME)
++ML_HOME=@ML_HOME@
+ ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
+ ML_OPTIONS="-H 200"
+ ML_SOURCES="$ML_HOME/../src"
+@@ -185,13 +178,7 @@
+ ###
+ 
+ # Proof General home, look in a variety of places
+-PROOFGENERAL_HOME=$(choosefrom \
+-  "$ISABELLE_HOME/contrib/ProofGeneral" \
+-  "$ISABELLE_HOME/../ProofGeneral" \
+-  "/usr/local/ProofGeneral" \
+-  "/usr/share/ProofGeneral" \
+-  "/opt/ProofGeneral" \
+-  "")
++PROOFGENERAL_HOME=@PROOFGENERAL_HOME@
+ 
+ PROOFGENERAL_OPTIONS=""
+ #PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"

pkgs/top-level/all-packages.nix

@@ -8173,6 +8173,10 @@ let
     camlp5 = camlp5_transitional;
   };
 
+  isabelle = import ../applications/science/logic/isabelle {
+    inherit (pkgs) stdenv fetchurl nettools perl polyml emacs emacsPackages;
+  };
+
   ssreflect = import ../applications/science/logic/ssreflect {
     inherit stdenv fetchurl ocaml coq;
     camlp5 = camlp5_transitional;