Adding E-KRHyper theorem prover

This commit is contained in:
Michael Raskin 2013-05-09 17:47:40 +04:00
parent c82d9b6169
commit a453e49511
3 changed files with 37 additions and 0 deletions

View File

@ -0,0 +1,32 @@
{stdenv, fetchurl, ocaml, perl}:
let
s = # Generated upstream information
rec {
baseName="ekrhyper";
version="1_4_08022013";
name="${baseName}-${version}";
hash="0vni5pq1p99428ii3g13chiqxcs8k1fm6jlvg1jqh4qdcs42w7yb";
url="http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/ekrh_1_4_08022013.tar.gz";
sha256="0vni5pq1p99428ii3g13chiqxcs8k1fm6jlvg1jqh4qdcs42w7yb";
};
buildInputs = [
ocaml perl
];
in
stdenv.mkDerivation {
inherit (s) name version;
inherit buildInputs;
src = fetchurl {
inherit (s) url sha256;
};
setSourceRoot = "export sourceRoot=$(echo */ekrh/src/)";
preInstall = "export INSTALLDIR=$out";
postInstall = ''for i in "$out/casc"/*; do ln -s "$i" "$out/bin/ekrh-casc-$(basename $i)"; done '';
meta = {
inherit (s) version;
description = "Automated first-order theorem prover";
license = stdenv.lib.licenses.gpl2 ;
maintainers = [stdenv.lib.maintainers.raskin];
platforms = stdenv.lib.platforms.linux;
};
}

View File

@ -0,0 +1,3 @@
url http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/
ensure_choice
version '.*[^0-9]_([-0-9_]+)[.].*' '\1'

View File

@ -8838,6 +8838,8 @@ let
cvc3 = callPackage ../applications/science/logic/cvc3 {};
ekrhyper = callPackage ../applications/science/logic/ekrhyper {};
eprover = callPackage ../applications/science/logic/eprover {
texLive = texLiveAggregationFun {
paths = [