E prover: do not build the manual
This commit is contained in:
parent
f5f24dd95a
commit
715f78be7e
@ -1,4 +1,4 @@
|
|||||||
{ stdenv, fetchurl, which, texLive }:
|
{ stdenv, fetchurl, which }:
|
||||||
let
|
let
|
||||||
s = # Generated upstream information
|
s = # Generated upstream information
|
||||||
rec {
|
rec {
|
||||||
@ -18,26 +18,22 @@ stdenv.mkDerivation {
|
|||||||
inherit (s) url sha256;
|
inherit (s) url sha256;
|
||||||
};
|
};
|
||||||
|
|
||||||
buildInputs = [which texLive];
|
buildInputs = [ which ];
|
||||||
|
|
||||||
preConfigure = "sed -e 's@^EXECPATH\\s.*@EXECPATH = '\$out'/bin@' -i Makefile.vars";
|
preConfigure = "sed -e 's@^EXECPATH\\s.*@EXECPATH = '\$out'/bin@' -i Makefile.vars";
|
||||||
|
|
||||||
buildPhase = "make install";
|
buildPhase = "make install";
|
||||||
|
|
||||||
# HOME=. allows to build missing TeX formats
|
|
||||||
installPhase = ''
|
installPhase = ''
|
||||||
mkdir -p $out/bin
|
mkdir -p $out/bin
|
||||||
make install
|
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
|
echo eproof -xAuto --tstp-in --tstp-out '"$@"' > $out/bin/eproof-tptp
|
||||||
chmod a+x $out/bin/eproof-tptp
|
chmod a+x $out/bin/eproof-tptp
|
||||||
'';
|
'';
|
||||||
|
|
||||||
meta = {
|
meta = {
|
||||||
inherit (s) version;
|
inherit (s) version;
|
||||||
description = "E automated theorem prover";
|
description = "Automated theorem prover for full first-order logic with equality";
|
||||||
maintainers = [stdenv.lib.maintainers.raskin];
|
maintainers = [stdenv.lib.maintainers.raskin];
|
||||||
platforms = stdenv.lib.platforms.all;
|
platforms = stdenv.lib.platforms.all;
|
||||||
};
|
};
|
||||||
|
@ -14159,13 +14159,7 @@ let
|
|||||||
|
|
||||||
ekrhyper = callPackage ../applications/science/logic/ekrhyper {};
|
ekrhyper = callPackage ../applications/science/logic/ekrhyper {};
|
||||||
|
|
||||||
eprover = callPackage ../applications/science/logic/eprover {
|
eprover = callPackage ../applications/science/logic/eprover { };
|
||||||
texLive = texLiveAggregationFun {
|
|
||||||
paths = [
|
|
||||||
texLive texLiveExtra
|
|
||||||
];
|
|
||||||
};
|
|
||||||
};
|
|
||||||
|
|
||||||
gappa = callPackage ../applications/science/logic/gappa { };
|
gappa = callPackage ../applications/science/logic/gappa { };
|
||||||
|
|
||||||
|
Loading…
x
Reference in New Issue
Block a user