about summary refs log tree commit diff
path: root/pkgs/applications/science/logic/eprover/default.nix
diff options
context:
space:
mode:
Diffstat (limited to 'pkgs/applications/science/logic/eprover/default.nix')
-rw-r--r--pkgs/applications/science/logic/eprover/default.nix10
1 files changed, 3 insertions, 7 deletions
diff --git a/pkgs/applications/science/logic/eprover/default.nix b/pkgs/applications/science/logic/eprover/default.nix
index 35e70a4b0d73..bb0e34d45bc9 100644
--- a/pkgs/applications/science/logic/eprover/default.nix
+++ b/pkgs/applications/science/logic/eprover/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, which, texLive }:
+{ stdenv, fetchurl, which }:
 let
   s = # Generated upstream information
   rec {
@@ -18,26 +18,22 @@ stdenv.mkDerivation {
     inherit (s) url sha256;
   };
 
-  buildInputs = [which texLive];
+  buildInputs = [ which ];
 
   preConfigure = "sed -e 's@^EXECPATH\\s.*@EXECPATH = '\$out'/bin@' -i Makefile.vars";
 
   buildPhase = "make install";
 
-  # HOME=. allows to build missing TeX formats
   installPhase = ''
     mkdir -p $out/bin
     make install
-    HOME=. 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 = {
     inherit (s) version;
-    description = "E automated theorem prover";
+    description = "Automated theorem prover for full first-order logic with equality";
     maintainers = [stdenv.lib.maintainers.raskin];
     platforms = stdenv.lib.platforms.all;
   };