Merge pull request #301348 from symphorien/update_bitwuzla

bitwuzla: unstable-2022-10-03 -> 0.4.0

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

@@ -1,70 +1,72 @@
 { stdenv
 , fetchFromGitHub
+, fetchpatch
 , lib
 , python3
-, cmake
+, meson
-, lingeling
+, ninja
+, git
 , btor2tools
 , symfpu
 , gtest
 , gmp
 , cadical
-, minisat
-, picosat
 , cryptominisat
 , zlib
 , pkg-config
-  # "*** internal error in 'lglib.c': watcher stack overflow" on aarch64-linux
-, withLingeling ? !stdenv.hostPlatform.isAarch64
 }:
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation (finalAttrs: {
   pname = "bitwuzla";
-  version = "unstable-2022-10-03";
+  version = "0.4.0";
 
   src = fetchFromGitHub {
     owner = "bitwuzla";
     repo = "bitwuzla";
-    rev = "3bc0f9f1aca04afabe1aff53dd0937924618b2ad";
+    rev = finalAttrs.version;
-    hash = "sha256-UXZERl7Nedwex/oUrcf6/GkDSgOQ537WDYm117RfvWo=";
+    hash = "sha256-ZEdV4ml1LwrYwscgOcL2gLx/ijPYqRktXMQH/Njh8OI=";
   };
 
-  nativeBuildInputs = [ cmake pkg-config ];
+  patches = [
+    # fix parser on aarch64
+    # remove on next release
+    (fetchpatch {
+      url = "https://github.com/bitwuzla/bitwuzla/commit/4d914aa5ec34076c37749f0cf6dce976ea510386.patch";
+      hash = "sha256-gp+HEamOySjPXCC39tt5DIMdQqEew26a+M15sNdCmTM=";
+    })
+  ];
+
+  strictDeps = true;
+
+  nativeBuildInputs = [ meson pkg-config git ninja ];
   buildInputs = [
     cadical
     cryptominisat
-    picosat
-    minisat
     btor2tools
     symfpu
     gmp
     zlib
-  ] ++ lib.optional withLingeling lingeling;
+  ];
 
-  cmakeFlags = [
+  mesonFlags = [
-    "-DBUILD_SHARED_LIBS=ON"
+    # note: the default value for default_library fails to link dynamic dependencies
-    "-DPicoSAT_INCLUDE_DIR=${lib.getDev picosat}/include/picosat"
+    # but setting it to shared works even in pkgsStatic
-    "-DBtor2Tools_INCLUDE_DIR=${lib.getDev btor2tools}/include/btor2parser"
+    "-Ddefault_library=shared"
-    "-DBtor2Tools_LIBRARIES=${lib.getLib btor2tools}/lib/libbtor2parser${stdenv.hostPlatform.extensions.sharedLibrary}"
-  ] ++ lib.optional doCheck "-DTESTING=YES";
 
-  nativeCheckInputs = [ python3 gtest ];
+    (lib.strings.mesonEnable "testing" finalAttrs.doCheck)
-  # two tests fail on darwin and 3 on aarch64-linux
+  ];
-  doCheck = stdenv.hostPlatform.isLinux && (!stdenv.hostPlatform.isAarch64);
-  preCheck = let
-    var = if stdenv.isDarwin then "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH";
-  in
-    ''
-      export ${var}=$(readlink -f lib)
-      patchShebangs ..
-    '';
 
-  meta = with lib; {
+  nativeCheckInputs = [ python3 ];
+  checkInputs = [ gtest ];
+  # two tests fail on darwin
+  doCheck = stdenv.hostPlatform.isLinux;
+
+  meta = {
     description = "A SMT solver for fixed-size bit-vectors, floating-point arithmetic, arrays, and uninterpreted functions";
     mainProgram = "bitwuzla";
     homepage = "https://bitwuzla.github.io";
-    license = licenses.mit;
+    license = lib.licenses.mit;
-    platforms = platforms.unix;
+    platforms = lib.platforms.unix;
-    maintainers = with maintainers; [ symphorien ];
+    maintainers = with lib.maintainers; [ symphorien ];
   };
-}
+})

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

@@ -1,4 +1,4 @@
-{ lib, stdenv, fetchFromGitHub }:
+{ lib, stdenv, fetchFromGitHub, copyPkgconfigItems, makePkgconfigItem }:
 
 stdenv.mkDerivation rec {
   pname = "cadical";
@@ -14,6 +14,35 @@ stdenv.mkDerivation rec {
   outputs = [ "out" "dev" "lib" ];
   doCheck = true;
 
+  nativeBuildInputs = [ copyPkgconfigItems ];
+
+  pkgconfigItems = [
+    (makePkgconfigItem {
+      name = "cadical";
+      inherit version;
+      cflags = [ "-I\${includedir}" ];
+      libs = [ "-L\${libdir}" "-lcadical" ];
+      variables = {
+        includedir = "@includedir@";
+        libdir = "@libdir@";
+      };
+      inherit (meta) description;
+    })
+  ];
+
+  env = {
+    # copyPkgconfigItems will substitute these in the pkg-config file
+    includedir = "${placeholder "dev"}/include";
+    libdir = "${placeholder "lib"}/lib";
+  };
+
+  enableParallelBuilding = true;
+
+  # fix static build
+  postPatch = ''
+    substituteInPlace makefile.in --replace-fail "ar rc" '$(AR) rc'
+  '';
+
   # the configure script is not generated by autotools and does not accept the
   # arguments that the default configurePhase passes like --prefix and --libdir
   configurePhase = ''

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

@@ -17,8 +17,14 @@ stdenv.mkDerivation rec {
     hash = "sha256-8oH9moMjQEWnQXKmKcqmXuXcYkEyvr4hwC1bC4l26mo=";
   };
 
-  buildInputs = [ python3 boost ];
+  strictDeps = true;
-  nativeBuildInputs = [ cmake ];
+  buildInputs = [ boost ];
+  nativeBuildInputs = [ python3 cmake ];
+
+  # musl does not have sys/unistd.h
+  postPatch = ''
+    substituteInPlace src/picosat/picosat.c --replace-fail '<sys/unistd.h>' '<unistd.h>'
+  '';
 
   meta = with lib; {
     description = "An advanced SAT Solver";

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

@@ -1,4 +1,4 @@
-{ lib, stdenv, fetchFromGitHub }:
+{ lib, stdenv, fetchFromGitHub, copyPkgconfigItems, makePkgconfigItem }:
 
 stdenv.mkDerivation rec {
   pname = "symfpu";
@@ -11,9 +11,32 @@ stdenv.mkDerivation rec {
     sha256 = "1jf5lkn67q136ppfacw3lsry369v7mdr1rhidzjpbz18jfy9zl9q";
   };
 
+  nativeBuildInputs = [ copyPkgconfigItems ];
+
+  pkgconfigItems = [
+    (makePkgconfigItem {
+      name = "symfpu";
+      inherit version;
+      cflags = [ "-I\${includedir}" ];
+      variables = {
+        includedir = "@includedir@";
+      };
+      inherit (meta) description;
+    })
+  ];
+
+  env = {
+    # copyPkgconfigItems will substitute this in the pkg-config file
+    includedir = "${placeholder "out"}/include";
+  };
+
   installPhase = ''
-    mkdir -p $out/symfpu
+    runHook preInstall
-    cp -r * $out/symfpu/
+
+    mkdir -p $out/include/symfpu
+    cp -r * $out/include/symfpu/
+
+    runHook postInstall
   '';
 
   meta = with lib; {