From c86efaec8157d6753c6b14c628a8d3c53a95532b Mon Sep 17 00:00:00 2001
From: Michael Raskin <7c6f434c@mail.ru>
Date: Sun, 7 Oct 2007 13:37:08 +0000
Subject: [PATCH] Added E authomated theorem prover and script eproof-tptp for
 TPTP syntax.

svn path=/nixpkgs/trunk/; revision=9418
---
 pkgs/tools/misc/eProver/default.nix | 27 +++++++++++++++++++++++++++
 pkgs/top-level/all-packages.nix     |  4 ++++
 2 files changed, 31 insertions(+)
 create mode 100644 pkgs/tools/misc/eProver/default.nix

diff --git a/pkgs/tools/misc/eProver/default.nix b/pkgs/tools/misc/eProver/default.nix
new file mode 100644
index 000000000000..1649a35004fc
--- /dev/null
+++ b/pkgs/tools/misc/eProver/default.nix
@@ -0,0 +1,27 @@
+args: with args;
+stdenv.mkDerivation {
+  name = "EProver-0.999";
+
+  src = 
+	fetchurl {
+		name = "E-0.999.tar.gz";
+		url = http://www4.informatik.tu-muenchen.de/~schulz/WORK/E_DOWNLOAD/V_0.999/E.tgz;
+		sha256 = "1zm1xip840hlam60kqk6xf0ikvyk7ch3ql1ac6wb68dx2l6hyhxv";
+	};
+
+  buildInputs =[which tetex];
+
+  preConfigure = "sed -e 's@^EXECPATH\\s.*@EXECPATH = '\$out'/bin@' -i Makefile.vars";
+
+  buildPhase = "make install";
+  installCommand = "mkdir -p \$out/bin; make install-exec; make documentation ; 
+		mkdir -p \$out/share/doc ; cp -r DOC \$out/share/doc/EProver;
+		echo eproof -xAuto --tstp-in --tstp-out '\"\$@\"' >\$out/bin/eproof-tptp; 
+		chmod a+x \$out/bin/eproof-tptp; ";
+
+  meta = {
+    description = "
+	E automated theorem prover.
+";
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 18334955a364..ad27dbf8689a 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -384,6 +384,10 @@ rec {
     inherit fetchurl stdenv;
   };
 
+  eprover = import ../tools/misc/eProver {
+    inherit fetchurl stdenv which tetex;
+  };
+
   exif = import ../tools/graphics/exif {
     inherit fetchurl stdenv pkgconfig libexif popt;
   };