petrinizer: fix build by pinning the neccessary library versions

3 files changed, 58 insertions, 2 deletions

diff --git a/pkgs/applications/science/logic/petrinizer/default.nix b/pkgs/applications/science/logic/petrinizer/default.nix
index cb35b9f27d5..d277e0e1521 100644
--- a/pkgs/applications/science/logic/petrinizer/default.nix
+++ b/pkgs/applications/science/logic/petrinizer/default.nix
@@ -1,6 +1,12 @@
-{ mkDerivation, async, base, bytestring, containers, fetchFromGitLab, mtl
-, parallel-io, parsec, sbv, stdenv, stm, transformers
+{ mkDerivation, callPackage, buildPackages
+, async, base, bytestring, containers, fetchFromGitLab, mtl
+, parallel-io, parsec, stdenv, stm, transformers
 }:
+let
+  z3 = callPackage ./z3.nix { gomp = null; z3 = buildPackages.z3; };
+in let
+  sbv = callPackage ./sbv-7.13.nix { inherit z3; };
+in
 mkDerivation rec {
   pname = "petrinizer";
   version = "0.9.1.1";
diff --git a/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix b/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix
new file mode 100644
index 00000000000..ed10e9f3db1
--- /dev/null
+++ b/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix
@@ -0,0 +1,26 @@
+{ mkDerivation, array, async, base, bytestring, containers
+, crackNum, deepseq, directory, doctest, filepath, generic-deriving
+, ghc, Glob, hlint, mtl, pretty, process, QuickCheck, random
+, stdenv, syb, tasty, tasty-golden, tasty-hunit, tasty-quickcheck
+, template-haskell, time, z3
+}:
+mkDerivation {
+  pname = "sbv";
+  version = "7.13";
+  sha256 = "0bk400swnb4s98c5p71ml1px6jndaiqhf5dj7zmnliyplqcgpfik";
+  enableSeparateDataOutput = true;
+  libraryHaskellDepends = [
+    array async base containers crackNum deepseq directory filepath
+    generic-deriving ghc mtl pretty process QuickCheck random syb
+    template-haskell time
+  ];
+  testHaskellDepends = [
+    base bytestring containers crackNum directory doctest filepath Glob
+    hlint mtl QuickCheck random syb tasty tasty-golden tasty-hunit
+    tasty-quickcheck template-haskell
+  ];
+  testSystemDepends = [ z3 ];
+  homepage = "http://leventerkok.github.com/sbv/";
+  description = "SMT Based Verification: Symbolic Haskell theorem prover using SMT solving";
+  license = stdenv.lib.licenses.bsd3;
+}
diff --git a/pkgs/applications/science/logic/petrinizer/z3.nix b/pkgs/applications/science/logic/petrinizer/z3.nix
new file mode 100644
index 00000000000..4d868054c09
--- /dev/null
+++ b/pkgs/applications/science/logic/petrinizer/z3.nix
@@ -0,0 +1,24 @@
+{ mkDerivation, fetchpatch
+, base, containers, gomp, hspec, QuickCheck, stdenv
+, transformers, z3
+}:
+mkDerivation {
+  pname = "z3";
+  version = "408.0";
+  sha256 = "13qkzy9wc17rm60i24fa9sx15ywbxq4a80g33w20887gvqyc0q53";
+  isLibrary = true;
+  isExecutable = true;
+  libraryHaskellDepends = [ base containers transformers ];
+  librarySystemDepends = [ gomp z3 ];
+  testHaskellDepends = [ base hspec QuickCheck ];
+  homepage = "https://github.com/IagoAbal/haskell-z3";
+  description = "Bindings for the Z3 Theorem Prover";
+  license = stdenv.lib.licenses.bsd3;
+  doCheck = false;
+  patches = [
+    (fetchpatch {
+      url = "https://github.com/IagoAbal/haskell-z3/commit/b10e09b8a809fb5bbbb1ef86aeb62109ece99cae.patch";
+      sha256 = "13fnrs27mg3985r3lwks8fxfxr5inrayy2cyx2867d92pnl3yry4";
+    })
+  ];
+}