From 7205e46c8055a2e6e09fa53f071c6dfb7d43ff39 Mon Sep 17 00:00:00 2001 From: Michael Raitza Date: Tue, 2 Oct 2018 14:06:21 +0200 Subject: [PATCH] Add Nix overlay that builds storm and its dependencies --- .../3rdparty/nix-scripts/carl/default.nix | 51 ++++++++++++++++++ .../3rdparty/nix-scripts/carl/gtest.cmake | 3 ++ resources/3rdparty/nix-scripts/default.nix | 14 +++++ .../nix-scripts/googletest/default.nix | 22 ++++++++ .../3rdparty/nix-scripts/l3pp/default.nix | 26 ++++++++++ .../3rdparty/nix-scripts/mathsat/default.nix | 46 ++++++++++++++++ .../nix-scripts/storm-checker/default.nix | 52 +++++++++++++++++++ resources/3rdparty/nix-scripts/z3/default.nix | 20 +++++++ 8 files changed, 234 insertions(+) create mode 100644 resources/3rdparty/nix-scripts/carl/default.nix create mode 100644 resources/3rdparty/nix-scripts/carl/gtest.cmake create mode 100644 resources/3rdparty/nix-scripts/default.nix create mode 100644 resources/3rdparty/nix-scripts/googletest/default.nix create mode 100644 resources/3rdparty/nix-scripts/l3pp/default.nix create mode 100644 resources/3rdparty/nix-scripts/mathsat/default.nix create mode 100644 resources/3rdparty/nix-scripts/storm-checker/default.nix create mode 100644 resources/3rdparty/nix-scripts/z3/default.nix diff --git a/resources/3rdparty/nix-scripts/carl/default.nix b/resources/3rdparty/nix-scripts/carl/default.nix new file mode 100644 index 000000000..69241252f --- /dev/null +++ b/resources/3rdparty/nix-scripts/carl/default.nix @@ -0,0 +1,51 @@ +{ stdenv, fetchFromGitHub, autoconf, pkgconfig, cmake +, cln, ginac, gmp, boost, eigen3_3, python2, googletest }: + +let + gtest-cmake = ./gtest.cmake; + +in stdenv.mkDerivation rec { + name = "carl-${version}"; + version = "17.12"; + + buildInputs = [ cln ginac gmp boost python2 googletest ]; + + nativeBuildInputs = [ autoconf pkgconfig cmake ]; + + propagatedBuildInputs = [ eigen3_3 ]; + + src = fetchFromGitHub { + owner = "smtrat"; + repo = "carl"; + rev = version; + sha256 = "1299i0b6w4v6s2a2kci3jrpdq1lpaw4j3p34gx6gmp9g3n1yp6xq"; + }; + + enableParallelBuilding = true; + + cmakeFlags = [ + "-DEXPORT_TO_CMAKE=off" + "-DUSE_CLN_NUMBERS=on" + "-DTHREAD_SAFE=on" + "-DUSE_GINAC=on" + "-DGINAC_FOUND=on" + "-DGINAC_INCLUDE_DIR=${ginac}/include/ginac" + "-DGINAC_LIBRARY=${ginac}/lib/libginac.so" + "-DGTEST_FOUND=on" + "-DGTEST_MAIN_LIBRARY=${googletest}/lib/libgtest_main.a" + "-DGTEST_LIBRARY=${googletest}/lib/libgtest.a" + ]; + + postPatch = '' + cp ${gtest-cmake} resources/gtest.cmake + substituteInPlace resources/gtest.cmake --subst-var-by googletest ${googletest} + sed -e '/set(GTEST/i include(resources/gtest.cmake)' -i resources/resources.cmake + ''; + + meta = with stdenv.lib; { + description = "Computer ARithmetic and Logic library"; + homepage = http://smtrat.github.io/carl; + mainainers = [ maintainers.spacefrogg ]; + platforms = platforms.all; + }; +} diff --git a/resources/3rdparty/nix-scripts/carl/gtest.cmake b/resources/3rdparty/nix-scripts/carl/gtest.cmake new file mode 100644 index 000000000..4f098157f --- /dev/null +++ b/resources/3rdparty/nix-scripts/carl/gtest.cmake @@ -0,0 +1,3 @@ +add_imported_library(GTESTCORE STATIC "@googletest@/lib/${CMAKE_FIND_LIBRARY_PREFIXES}gtest${STATIC_EXT}" "@googletest@/include") +add_imported_library(GTESTMAIN STATIC "@googletest@/lib/${CMAKE_FIND_LIBRARY_PREFIXES}gtest_main${STATIC_EXT}" "@googletest@/include") +set(GTEST_LIBRARIES GTESTCORE_STATIC GTESTMAIN_STATIC pthread dl) \ No newline at end of file diff --git a/resources/3rdparty/nix-scripts/default.nix b/resources/3rdparty/nix-scripts/default.nix new file mode 100644 index 000000000..9d4aae3cb --- /dev/null +++ b/resources/3rdparty/nix-scripts/default.nix @@ -0,0 +1,14 @@ +self: super: +with self; +with self.lib; +let + callPackage = super.lib.callPackageWith self; + _self = { + z3 = callPackage ./z3 { }; + stormChecker = callPackage ./storm-checker { ltoSupport = false; tbbSupport = false; mathsatSupport = false; z3Support = false; }; + carl = callPackage ./carl { }; + googletest = callPackage ./googletest { }; + l3pp = callPackage ./l3pp { }; + mathsat = callPackage ./mathsat { }; + }; +in _self diff --git a/resources/3rdparty/nix-scripts/googletest/default.nix b/resources/3rdparty/nix-scripts/googletest/default.nix new file mode 100644 index 000000000..b46d51765 --- /dev/null +++ b/resources/3rdparty/nix-scripts/googletest/default.nix @@ -0,0 +1,22 @@ +{ stdenv, fetchFromGitHub, cmake }: + +stdenv.mkDerivation rec { + name = "googletest-${version}"; + version = "1.8.0"; + + buildInputs = [ cmake ]; + + src = fetchFromGitHub { + owner = "google"; + repo = "googletest"; + rev = "release-${version}"; + sha256 = "0bjlljmbf8glnd9qjabx73w6pd7ibv43yiyngqvmvgxsabzr8399"; + }; + + meta = with stdenv.lib; { + description = "Google's C++ test framework"; + homepage = "https://github.com/google/googletest"; + maintainers = [ maintainers.spacefrogg ]; + platforms = platforms.all; + }; +} diff --git a/resources/3rdparty/nix-scripts/l3pp/default.nix b/resources/3rdparty/nix-scripts/l3pp/default.nix new file mode 100644 index 000000000..ac21c5f05 --- /dev/null +++ b/resources/3rdparty/nix-scripts/l3pp/default.nix @@ -0,0 +1,26 @@ +{ stdenv, fetchFromGitHub }: +stdenv.mkDerivation rec { + name = "l3pp-${version}"; + version = "git"; + + src = fetchFromGitHub { + owner = "hbruintjes"; + repo = "l3pp"; + rev = "e4f8d7fe6c328849aff34d2dfd6fd592c14070d5"; + sha256 = "0bd0m4hj7iy5y9546sr7d156hmq6q7d5jys495jd26ngvibkv9hp"; + }; + phases = "unpackPhase installPhase fixupPhase"; + + installPhase = '' + mkdir -p $out/include $out/share/doc/l3pp + cp LICENSE Readme.md $out/share/doc/l3pp + cp -r *.h impl $out/include + ''; + + meta = with stdenv.lib; { + description = "Lightweight Logging Library for C++"; + homepage = https://github.com/hbruintjes/l3pp; + maintainers = [ maintainers.spacefrogg ]; + platforms = platforms.all; + }; +} diff --git a/resources/3rdparty/nix-scripts/mathsat/default.nix b/resources/3rdparty/nix-scripts/mathsat/default.nix new file mode 100644 index 000000000..180e50a21 --- /dev/null +++ b/resources/3rdparty/nix-scripts/mathsat/default.nix @@ -0,0 +1,46 @@ +{ stdenv, fetchurl, file +, gmp +, reentrantBuild ? true +}: + +let + version = "5.5.1"; + name = "mathsat-${version}"; + genUrl = reentrant: "http://mathsat.fbk.eu/download.php?file=${name}-linux-x86_64${reentrant}.tar.gz"; + srcAttrs = if reentrantBuild then { + url = genUrl "-reentrant"; + sha256 = "10ng53nvxyyvml3gbzl87vj3c75fgb14zdlakwasz7zczn7hm978"; + } else { + url = genUrl ""; + sha256 = "0jnbiaq27hzdzavkr3sdh2ym0bc3ykamacj8k08pvyf7vil2hkdz"; + }; + +in stdenv.mkDerivation rec { + inherit name version; + + src = fetchurl srcAttrs; + + nativeBuildInputs = [ gmp ]; + + libPath = stdenv.lib.makeLibraryPath [ stdenv.cc.cc stdenv.cc.libc stdenv.glibc gmp ]; + phases = "unpackPhase installPhase fixupPhase"; + + installPhase = '' + mkdir -p $out/{bin,lib,include} + patchelf --set-rpath "$libPath" lib/libmathsat.so + cp bin/* $out/bin + cp lib/* $out/lib + cp -r include/* $out/include + ''; + + meta = with stdenv.lib; { + description = "Satisfiability modulo theories (SMT) solver"; + homepage = http://mathsat.fbk.eu; + license = { + fullName = "Unfree, redistributable for non-commercial applications"; + free = false; + }; + maintainer = [ maintainers.spacefrogg ]; + platforms = platforms.linux; + }; +} diff --git a/resources/3rdparty/nix-scripts/storm-checker/default.nix b/resources/3rdparty/nix-scripts/storm-checker/default.nix new file mode 100644 index 000000000..6c322500b --- /dev/null +++ b/resources/3rdparty/nix-scripts/storm-checker/default.nix @@ -0,0 +1,52 @@ +{ stdenv, fetchFromGitHub, writeText, autoconf, automake, cmake +, boost, carl, cln, doxygen, gmp, ginac, glpk, hwloc, l3pp, xercesc +, ltoSupport ? true +, mathsatSupport ? false, mathsat +, tbbSupport ? false, tbb +, z3Support ? true, z3 +}: + +let + l3ppCmakeSed = writeText "l3pp-sed" '' +8,27d +28i\ +set(l3pp_INCLUDE "${l3pp}/include/") +30d + ''; + inherit (stdenv.lib) optional singleton; + genCmakeOption = bool: name: + singleton "-D${name}=${if bool then "on" else "off"}"; + +in stdenv.mkDerivation { + name = "storm-git"; + + src = fetchFromGitHub { + owner = "moves-rwth"; + repo = "storm"; + rev = "4378279c6419541e7100270937c849e5c5d53fea"; + sha256 = "1yhz9642s09izy9qid0a03i4c29cdvrmrrx9wa35dw5vkv6gxp0f"; + }; + + buildInputs = [ boost carl cln doxygen gmp ginac glpk hwloc l3pp xercesc ] + ++ optional tbbSupport tbb + ++ optional z3Support z3; + + nativeBuildInputs = [ autoconf automake cmake ]; + + cmakeFlags = genCmakeOption tbbSupport "STORM_USE_INTELTBB" + ++ genCmakeOption ltoSupport "STORM_USE_LTO" + ++ optional mathsatSupport "-DMSAT_ROOT=${mathsat}" ; + + postPatch = '' + sed -f ${l3ppCmakeSed} -i resources/3rdparty/CMakeLists.txt + substituteInPlace CMakeLists.txt --replace "include(export)" "" + ''; + + meta = with stdenv.lib; { + description = "Probabilistic Model Checker"; + homepage = http://www.stormchecker.org; + license = licenses.gpl3; + maintainer = [ maintainers.spacefrogg ]; + platforms = platforms.all; + }; +} diff --git a/resources/3rdparty/nix-scripts/z3/default.nix b/resources/3rdparty/nix-scripts/z3/default.nix new file mode 100644 index 000000000..3bb9d1aec --- /dev/null +++ b/resources/3rdparty/nix-scripts/z3/default.nix @@ -0,0 +1,20 @@ +{ stdenv, fetchFromGitHub, python3 }: + +stdenv.mkDerivation rec { + name = "z3-${version}"; + version = "4.6.0"; + + src = fetchFromGitHub { + owner = "Z3Prover"; + repo = "z3"; + rev = "z3-${version}"; + sha256 = "1cgwlmjdbf4rsv2rriqi2sdpz9qxihxrcpm6a4s37ijy437xg78l"; + }; + + buildInputs = [ python3 ]; + phases = "unpackPhase buildPhase installPhase fixupPhase"; + preBuild = '' + python3 scripts/mk_make.py --prefix=$out + cd build + ''; +}