diff options
author | Marco Maggesi <maggesi@math.unifi.it> | 2009-12-11 17:00:52 +0000 |
---|---|---|
committer | Marco Maggesi <maggesi@math.unifi.it> | 2009-12-11 17:00:52 +0000 |
commit | 98aaa4421c5e4ce3e2d0db2d9b81e198d00b370b (patch) | |
tree | 607f5c8fc64fa753408cecdda5fad1b718b76ed8 /pkgs/applications/science/logic | |
parent | 218bdaf214b13cdd01de00ca00285e36a718e72a (diff) | |
download | nixlib-98aaa4421c5e4ce3e2d0db2d9b81e198d00b370b.tar nixlib-98aaa4421c5e4ce3e2d0db2d9b81e198d00b370b.tar.gz nixlib-98aaa4421c5e4ce3e2d0db2d9b81e198d00b370b.tar.bz2 nixlib-98aaa4421c5e4ce3e2d0db2d9b81e198d00b370b.tar.lz nixlib-98aaa4421c5e4ce3e2d0db2d9b81e198d00b370b.tar.xz nixlib-98aaa4421c5e4ce3e2d0db2d9b81e198d00b370b.tar.zst nixlib-98aaa4421c5e4ce3e2d0db2d9b81e198d00b370b.zip |
Add expression for Isabelle2009
svn path=/nixpkgs/trunk/; revision=18905
Diffstat (limited to 'pkgs/applications/science/logic')
-rw-r--r-- | pkgs/applications/science/logic/isabelle/default.nix | 62 | ||||
-rw-r--r-- | pkgs/applications/science/logic/isabelle/settings.patch | 35 |
2 files changed, 97 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 000000000000..4d8df2f08808 --- /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 000000000000..15a70944087b --- /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" |