boolector: 2.4.1 -> 3.0.0, relicensed to MIT

Signed-off-by: Austin Seipp <aseipp@pobox.com>

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";
+  version = "3.0.0";
-  src = fetchurl {
+
-    url    = "http://fmv.jku.at/boolector/boolector-${version}-with-lingeling-bbc.tar.bz2";
+  src = fetchFromGitHub {
-    sha256 = "0mdf7hwix237pvknvrpazcx6s3ininj5k7vhysqjqgxa7lxgq045";
+    owner  = "boolector";
+    repo   = "boolector";
+    rev    = "refs/tags/${version}";
+    sha256 = "15i3ni5klss423m57wcy1gx0m5wfrjmglapwg85pm7fb3jj1y7sz";
   };
 
-  prePatch =
+  nativeBuildInputs = [ cmake ];
-    let
+  buildInputs = [ lingeling btor2tools ];
-      lingelingPatch = writeShellScriptBin "lingeling-patch" ''
-        sed -i -e "1i#include <stdint.h>" lingeling/lglib.h
 
-        ${crossFix}/bin/crossFix lingeling
+  cmakeFlags =
-      '';
+    [ "-DSHARED=ON"
-      crossFix = writeShellScriptBin "crossFix" ''
+      "-DUSE_LINGELING=YES"
-        # substituteInPlace not available here
+      "-DBTOR2_INCLUDE_DIR=${btor2tools.dev}/include"
-        sed -i $1/makefile.in \
+      "-DBTOR2_LIBRARIES=${btor2tools.lib}/lib/libbtor2parser.so"
-          -e 's@ar rc@$(AR) rc@' \
+      "-DLINGELING_INCLUDE_DIR=${lingeling.dev}/include"
-          -e 's@ranlib@$(RANLIB)@'
+      "-DLINGELING_LIBRARIES=${lingeling.lib}/lib/liblgl.a"
-      '';
+    ];
-    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
-  '';
 
   installPhase = ''
-    mkdir $out
+    mkdir -p $out/bin $lib/lib $dev/include
-    mv boolector/bin $out
+
+    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 = {
+  outputs = [ "out" "dev" "lib" ];
-    license = stdenv.lib.licenses.unfreeRedistributable;
+
+  meta = with stdenv.lib; {
     description = "An extremely fast SMT solver for bit-vectors and arrays";
-    homepage    = "http://fmv.jku.at/boolector";
+    homepage    = https://boolector.github.io;
-    platforms   = stdenv.lib.platforms.linux;
+    license     = licenses.mit;
-    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+    platforms   = platforms.linux;
+    maintainers = with maintainers; [ thoughtpolice ];
   };
 }