forked from mirrors/nixpkgs
cvc3: reimplement using mkDerivation
This commit is contained in:
parent
f4c9d2f64e
commit
a228252b69
|
@ -1,48 +1,27 @@
|
||||||
x@{builderDefsPackage
|
{ stdenv, fetchurl, flex, bison, gmp, perl }:
|
||||||
, flex, bison, gmp, perl
|
|
||||||
, ...}:
|
|
||||||
builderDefsPackage
|
|
||||||
(a :
|
|
||||||
let
|
|
||||||
helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++
|
|
||||||
["gmp"];
|
|
||||||
|
|
||||||
buildInputs = (map (n: builtins.getAttr n x)
|
stdenv.mkDerivation rec {
|
||||||
(builtins.attrNames (builtins.removeAttrs x helperArgNames)))
|
name = "cvc3-${version}";
|
||||||
++ [(a.lib.overrideDerivation x.gmp (y: {dontDisableStatic=true;}))];
|
version = "2.4.1";
|
||||||
sourceInfo = rec {
|
|
||||||
baseName="cvc3";
|
|
||||||
version="2.4.1";
|
|
||||||
name="${baseName}-${version}";
|
|
||||||
url="http://www.cs.nyu.edu/acsys/cvc3/releases/${version}/${name}.tar.gz";
|
|
||||||
hash="1xxcwhz3y6djrycw8sm6xz83wb4hb12rd1n0skvc7fng0rh1snym";
|
|
||||||
};
|
|
||||||
in
|
|
||||||
rec {
|
|
||||||
src = a.fetchurl {
|
|
||||||
url = sourceInfo.url;
|
|
||||||
sha256 = sourceInfo.hash;
|
|
||||||
};
|
|
||||||
|
|
||||||
inherit (sourceInfo) name version;
|
src = fetchurl {
|
||||||
inherit buildInputs;
|
url = "http://www.cs.nyu.edu/acsys/cvc3/releases/${version}/${name}.tar.gz";
|
||||||
|
sha256 = "1xxcwhz3y6djrycw8sm6xz83wb4hb12rd1n0skvc7fng0rh1snym";
|
||||||
|
};
|
||||||
|
|
||||||
/* doConfigure should be removed if not needed */
|
buildInputs = [ gmp flex bison perl ];
|
||||||
phaseNames = ["fixPaths" "doConfigure" "doMakeInstall"];
|
|
||||||
fixPaths = a.fullDepEntry (''
|
preConfigure = ''
|
||||||
sed -e "s@ /bin/bash@bash@g" -i Makefile.std
|
sed -e "s@ /bin/bash@bash@g" -i Makefile.std
|
||||||
find . -exec sed -e "s@/usr/bin/perl@${perl}/bin/perl@g" -i '{}' ';'
|
find . -exec sed -e "s@/usr/bin/perl@${perl}/bin/perl@g" -i '{}' ';'
|
||||||
'') ["minInit" "doUnpack"];
|
'';
|
||||||
|
|
||||||
meta = {
|
meta = with stdenv.lib; {
|
||||||
description = "A prover for satisfiability modulo theory (SMT)";
|
description = "A prover for satisfiability modulo theory (SMT)";
|
||||||
maintainers = with a.lib.maintainers;
|
maintainers = with maintainers;
|
||||||
[
|
[ raskin ];
|
||||||
raskin
|
platforms = platforms.linux;
|
||||||
];
|
license = licenses.free;
|
||||||
platforms = with a.lib.platforms;
|
|
||||||
linux;
|
|
||||||
license = a.lib.licenses.free;
|
|
||||||
homepage = "http://www.cs.nyu.edu/acsys/cvc3/index.html";
|
homepage = "http://www.cs.nyu.edu/acsys/cvc3/index.html";
|
||||||
};
|
};
|
||||||
passthru = {
|
passthru = {
|
||||||
|
@ -50,4 +29,4 @@ rec {
|
||||||
downloadPage = "http://www.cs.nyu.edu/acsys/cvc3/download.html";
|
downloadPage = "http://www.cs.nyu.edu/acsys/cvc3/download.html";
|
||||||
};
|
};
|
||||||
};
|
};
|
||||||
}) x
|
}
|
||||||
|
|
|
@ -14809,7 +14809,9 @@ let
|
||||||
coqPackages = recurseIntoAttrs (mkCoqPackages_8_4 coqPackages);
|
coqPackages = recurseIntoAttrs (mkCoqPackages_8_4 coqPackages);
|
||||||
coqPackages_8_5 = recurseIntoAttrs (mkCoqPackages_8_5 coqPackages_8_5);
|
coqPackages_8_5 = recurseIntoAttrs (mkCoqPackages_8_5 coqPackages_8_5);
|
||||||
|
|
||||||
cvc3 = callPackage ../applications/science/logic/cvc3 {};
|
cvc3 = callPackage ../applications/science/logic/cvc3 {
|
||||||
|
gmp = lib.overrideDerivation gmp (a: { dontDisableStatic = true; });
|
||||||
|
};
|
||||||
cvc4 = callPackage ../applications/science/logic/cvc4 {};
|
cvc4 = callPackage ../applications/science/logic/cvc4 {};
|
||||||
|
|
||||||
ekrhyper = callPackage ../applications/science/logic/ekrhyper {};
|
ekrhyper = callPackage ../applications/science/logic/ekrhyper {};
|
||||||
|
|
Loading…
Reference in a new issue