ilyakooo0/nixpkgs
1
0
Fork 0
mirror of https://github.com/ilyakooo0/nixpkgs.git synced 2024-10-01 01:57:37 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #100750 from arcz/boolector

Browse Source 
boolector: enable darwin build
This commit is contained in:
Austin Seipp 2020-12-02 03:19:54 -06:00 committed by GitHub
commit a3ae8a4fcf
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 33 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

54
pkgs/applications/science/logic/boolector/default.nix
View File

@ -1,4 +1,4 @@
{ stdenv, fetchFromGitHub, lib, python3
{ stdenv, fetchFromGitHub, fetchpatch, lib, python3
, cmake, lingeling, btor2tools, gtest, gmp
}:
@ -13,6 +13,14 @@ stdenv.mkDerivation rec {
sha256 = "0jkmaw678njqgkflzj9g374yk1mci8yqvsxkrqzlifn6bwhwb7ci";
};
# excludes development artifacts from install, will be included in next release
patches = [
(fetchpatch {
url = "https://github.com/Boolector/boolector/commit/4d240436e34e65096671099766344dd9126145b1.patch";
sha256 = "1girsbvlhkkl1hldl2gsjynwc3m92jskn798qhx0ydg6whrfgcgw";
})
];
postPatch = ''
sed s@REPLACEME@file://${gtest.src}@ ${./cmake-gtest.patch} | patch -p1
'';
@ -23,39 +31,39 @@ stdenv.mkDerivation rec {
cmakeFlags =
[ "-DBUILD_SHARED_LIBS=ON"
"-DUSE_LINGELING=YES"
"-DBtor2Tools_INCLUDE_DIR=${btor2tools.dev}/include"
"-DBtor2Tools_LIBRARIES=${btor2tools.lib}/lib/libbtor2parser.so"
] ++ (lib.optional (gmp != null) "-DUSE_GMP=YES");
installPhase = ''
mkdir -p $out/bin $lib/lib $dev/include
cp -vr bin/* $out/bin
cp -vr lib/* $lib/lib
rm -rf $out/bin/{examples,tests}
# we don't care about gtest related libs
rm -rf $lib/lib/libg*
cd ../src
find . -iname '*.h' -exec cp --parents '{}' $dev/include \;
rm -rf $dev/include/tests
'';
checkInputs = [ python3 ];
doCheck = true;
preCheck = ''
export LD_LIBRARY_PATH=$(readlink -f lib)
patchShebangs ..
preCheck =
let var = if stdenv.isDarwin then "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH";
in
# tests modelgen and modelgensmt2 spawn boolector in another processes and
# macOS strips DYLD_LIBRARY_PATH, hardcode it for testing
stdenv.lib.optionalString stdenv.isDarwin ''
cp -r bin bin.back
install_name_tool -change libboolector.dylib $(pwd)/lib/libboolector.dylib bin/boolector
'' + ''
export ${var}=$(readlink -f lib)
patchShebangs ..
'';
postCheck = stdenv.lib.optionalString stdenv.isDarwin ''
rm -rf bin
mv bin.back bin
'';
outputs = [ "out" "dev" "lib" ];
# this is what haskellPackages.boolector expects
postInstall = ''
cp $out/include/boolector/boolector.h $out/include/boolector.h
cp $out/include/boolector/btortypes.h $out/include/btortypes.h
'';
meta = with stdenv.lib; {
description = "An extremely fast SMT solver for bit-vectors and arrays";
homepage = "https://boolector.github.io";
license = licenses.mit;
platforms = platforms.linux;
platforms = with platforms; linux ++ darwin;
maintainers = with maintainers; [ thoughtpolice ];
};
}

4
pkgs/applications/science/logic/btor2tools/default.nix
View File

@ -1,4 +1,4 @@
{ stdenv, cmake, fetchFromGitHub }:
{ stdenv, cmake, fetchFromGitHub, fixDarwinDylibNames }:
stdenv.mkDerivation rec {
pname = "btor2tools";
@ -11,7 +11,7 @@ stdenv.mkDerivation rec {
sha256 = "0mfqmkgvyw8fa2c09kww107dmk180ch1hp98r5kv41vnc04iqb0s";
};
nativeBuildInputs = [ cmake ];
nativeBuildInputs = [ cmake ] ++ stdenv.lib.optional stdenv.isDarwin fixDarwinDylibNames;
installPhase = ''
mkdir -p $out $dev/include/btor2parser/ $lib/lib