Add Nix overlay that builds storm and its dependencies

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;
+  };
+}

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)

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

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;
+  };
+}

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;
+  };
+}

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;
+  };
+}

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;
+  };
+}

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
+  '';
+}