diff options
-rw-r--r-- | pkgs/applications/science/logic/isabelle/default.nix | 62 | ||||
-rw-r--r-- | pkgs/applications/science/logic/isabelle/settings.patch | 35 | ||||
-rw-r--r-- | pkgs/top-level/all-packages.nix | 4 |
3 files changed, 101 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix new file mode 100644 index 00000000000..4d8df2f0880 --- /dev/null +++ b/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"; + }; +} diff --git a/pkgs/applications/science/logic/isabelle/settings.patch b/pkgs/applications/science/logic/isabelle/settings.patch new file mode 100644 index 00000000000..15a70944087 --- /dev/null +++ b/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" diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index dce82ecda96..bded1b4ea93 100644 --- a/pkgs/top-level/all-packages.nix +++ b/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; |