petrinizer: fix build

* take z3 haskell package from haskellPackages
* take sbv 7.13 from haskellPackages, apply patch fixing build
  with GHC >= 8.8.8

pkgs/applications/science/logic/petrinizer/default.nix

@@ -1,12 +1,8 @@
-{ mkDerivation, callPackage, buildPackages
+{ mkDerivation
 , async, base, bytestring, containers, fetchFromGitLab, mtl
-, parallel-io, parsec, lib, stm, transformers
+, parallel-io, parsec, lib, stm, transformers, sbv_7_13, z3
 }:
-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";
@@ -22,7 +18,7 @@ mkDerivation rec {
   isLibrary = false;
   isExecutable = true;
   executableHaskellDepends = [
-    async base bytestring containers mtl parallel-io parsec sbv stm
+    async base bytestring containers mtl parallel-io parsec sbv_7_13 stm
     transformers
   ];
   description = "Safety and Liveness Analysis of Petri Nets with SMT solvers";

pkgs/applications/science/logic/petrinizer/sbv-7.13.nix

@@ -1,26 +0,0 @@
-{ mkDerivation, array, async, base, bytestring, containers
-, crackNum, deepseq, directory, doctest, filepath, generic-deriving
-, ghc, Glob, hlint, mtl, pretty, process, QuickCheck, random
-, lib, 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 = lib.licenses.bsd3;
-}

pkgs/applications/science/logic/petrinizer/z3.nix

@@ -1,24 +0,0 @@
-{ mkDerivation, fetchpatch
-, base, containers, gomp, hspec, QuickCheck, lib
-, 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 = lib.licenses.bsd3;
-  doCheck = false;
-  patches = [
-    (fetchpatch {
-      url = "https://github.com/IagoAbal/haskell-z3/commit/b10e09b8a809fb5bbbb1ef86aeb62109ece99cae.patch";
-      sha256 = "13fnrs27mg3985r3lwks8fxfxr5inrayy2cyx2867d92pnl3yry4";
-    })
-  ];
-}

pkgs/development/haskell-modules/configuration-common.nix

@@ -1852,4 +1852,12 @@ self: super: {
     doCheck = pkgs.stdenv.targetPlatform.system == "x86_64-linux";
   };
 
+  # Fix build failure by picking patch from 8.5,
+  # we need this version of sbv for petrinizer
+  sbv_7_13 = appendPatch super.sbv_7_13
+    (pkgs.fetchpatch {
+      url = "https://github.com/LeventErkok/sbv/commit/57014b9c7c67dd9b63619a996e2c66e32c33c958.patch";
+      sha256 = "10npa8nh2413n6p6qld795qfkbld08icm02bspmk93y0kabpgmgm";
+    });
+
 } // import ./configuration-tensorflow.nix {inherit pkgs haskellLib;} self super

pkgs/development/haskell-modules/configuration-hackage2nix.yaml

@@ -2818,6 +2818,7 @@ extra-packages:
   - optparse-applicative < 0.16         # needed for niv-0.2.19
   - refinery == 0.3.*                   # required by hls-tactics-plugin-1.0.0.0
   - resolv == 0.1.1.2                   # required to build cabal-install-3.0.0.0 with pre ghc-8.8.x
+  - sbv == 7.13                         # required for pkgs.petrinizer
 
 package-maintainers:
   peti:

pkgs/development/haskell-modules/hackage-packages.nix

@@ -229602,6 +229602,37 @@ self: {
        license = lib.licenses.bsd3;
      }) {};
 
+  "sbv_7_13" = callPackage
+    ({ mkDerivation, array, async, base, bytestring, containers
+     , crackNum, deepseq, directory, doctest, filepath, generic-deriving
+     , ghc, Glob, hlint, mtl, pretty, process, QuickCheck, random, 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 ];
+       description = "SMT Based Verification: Symbolic Haskell theorem prover using SMT solving";
+       license = lib.licenses.bsd3;
+       platforms = [
+         "armv7l-linux" "i686-linux" "x86_64-darwin" "x86_64-linux"
+       ];
+       hydraPlatforms = lib.platforms.none;
+     }) {inherit (pkgs) z3;};
+
   "sbv" = callPackage
     ({ mkDerivation, array, async, base, bench-show, bytestring
      , containers, deepseq, directory, doctest, filepath, gauge, Glob