diff options
Diffstat (limited to 'pkgs/applications/science/logic/boolector/default.nix')
-rw-r--r-- | pkgs/applications/science/logic/boolector/default.nix | 67 |
1 files changed, 38 insertions, 29 deletions
diff --git a/pkgs/applications/science/logic/boolector/default.nix b/pkgs/applications/science/logic/boolector/default.nix index aa815e48db41..8e0ad22bba18 100644 --- a/pkgs/applications/science/logic/boolector/default.nix +++ b/pkgs/applications/science/logic/boolector/default.nix @@ -1,41 +1,50 @@ -{ stdenv, fetchurl, writeShellScriptBin }: +{ stdenv, fetchFromGitHub +, cmake, lingeling, btor2tools +}: stdenv.mkDerivation rec { name = "boolector-${version}"; - version = "2.4.1"; - src = fetchurl { - url = "http://fmv.jku.at/boolector/boolector-${version}-with-lingeling-bbc.tar.bz2"; - sha256 = "0mdf7hwix237pvknvrpazcx6s3ininj5k7vhysqjqgxa7lxgq045"; + version = "3.0.0"; + + src = fetchFromGitHub { + owner = "boolector"; + repo = "boolector"; + rev = "refs/tags/${version}"; + sha256 = "15i3ni5klss423m57wcy1gx0m5wfrjmglapwg85pm7fb3jj1y7sz"; }; - prePatch = - let - lingelingPatch = writeShellScriptBin "lingeling-patch" '' - sed -i -e "1i#include <stdint.h>" lingeling/lglib.h - - ${crossFix}/bin/crossFix lingeling - ''; - crossFix = writeShellScriptBin "crossFix" '' - # substituteInPlace not available here - sed -i $1/makefile.in \ - -e 's@ar rc@$(AR) rc@' \ - -e 's@ranlib@$(RANLIB)@' - ''; - in '' - sed -i -e 's@mv lingeling\* lingeling@\0 \&\& ${lingelingPatch}/bin/lingeling-patch@' makefile - sed -i -e 's@mv boolector\* boolector@\0 \&\& ${crossFix}/bin/crossFix boolector@' makefile - ''; + nativeBuildInputs = [ cmake ]; + buildInputs = [ lingeling btor2tools ]; + + cmakeFlags = + [ "-DSHARED=ON" + "-DUSE_LINGELING=YES" + "-DBTOR2_INCLUDE_DIR=${btor2tools.dev}/include" + "-DBTOR2_LIBRARIES=${btor2tools.lib}/lib/libbtor2parser.so" + "-DLINGELING_INCLUDE_DIR=${lingeling.dev}/include" + "-DLINGELING_LIBRARIES=${lingeling.lib}/lib/liblgl.a" + ]; installPhase = '' - mkdir $out - mv boolector/bin $out + mkdir -p $out/bin $lib/lib $dev/include + + cp -vr bin/* $out/bin + cp -vr lib/* $lib/lib + + rm -rf $out/bin/{examples,test} + + cd ../src + find . -iname '*.h' -exec cp --parents '{}' $dev/include \; + rm -rf $dev/include/tests ''; - meta = { - license = stdenv.lib.licenses.unfreeRedistributable; + outputs = [ "out" "dev" "lib" ]; + + meta = with stdenv.lib; { description = "An extremely fast SMT solver for bit-vectors and arrays"; - homepage = "http://fmv.jku.at/boolector"; - platforms = stdenv.lib.platforms.linux; - maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + homepage = https://boolector.github.io; + license = licenses.mit; + platforms = platforms.linux; + maintainers = with maintainers; [ thoughtpolice ]; }; } |