stp: 2.3.3 -> 2.3.4; fix tests; fix aarch64 compatibility; fix Python bindings; fix Darwin compatibility (#348447)

Author: RossComputerGuy

pkgs/by-name/st/stp/package.nix

@@ -1,71 +1,186 @@
-{ lib
-, stdenv
-, cmake
-, boost
-, bison
-, flex
-, fetchFromGitHub
-, fetchpatch
-, perl
-, python3
-, zlib
-, minisat
-, cryptominisat
+{
+  lib,
+  stdenv,
+  cmake,
+  boost,
+  bison,
+  flex,
+  pkg-config,
+  fetchFromGitHub,
+  fetchpatch,
+  symlinkJoin,
+  perl,
+  python3,
+  zlib,
+  minisat,
+  cryptominisat,
+  gmp,
+  cadical,
+  gtest,
+  lit,
+  outputcheck,
+  nix-update-script,
+  useCadical ? true,
 }:
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation (finalAttrs: {
   pname = "stp";
-  version = "2.3.3";
+  version = "2.3.4";
 
   src = fetchFromGitHub {
     owner = "stp";
     repo = "stp";
-    rev = version;
-    hash = "sha256-B+HQF4TJPkYrpodE4qo4JHvlu+a5HTJf1AFyXTnZ4vk=";
+    tag = "${finalAttrs.version}_cadical";
+    hash = "sha256-fNx3/VS2bimlVwCejEZtNGDqVKnwBm0O2YkIUQm6eDM=";
   };
   patches = [
-    # Fix missing type declaration
-    # due to undeterminisitic compilation
-    # of circularly dependent headers
-    ./stdint.patch
-
     # Python 3.12+ compatibility for build: https://github.com/stp/stp/pull/450
     (fetchpatch {
       url = "https://github.com/stp/stp/commit/fb185479e760b6ff163512cb6c30ac9561aadc0e.patch";
       hash = "sha256-guFgeWOrxRrxkU7kMvd5+nmML0rwLYW196m1usE2qiA=";
     })
   ];
+  postPatch =
+    ''
+      substituteInPlace CMakeLists.txt \
+        --replace-fail GIT-hash-notfound "$version"
 
-  postPatch = ''
-    # Upstream fix for gcc-13 support:
-    #   https://github.com/stp/stp/pull/462
-    # Can't apply it as is as patch context changed in ither patches.
-    # TODO: remove me on 2.4 release
-    sed -e '1i #include <cstdint>' -i include/stp/AST/ASTNode.h
-  '';
+      # We want to use the Nix wrapper for the output check tool instead of running it through Python.
+      substituteInPlace tests/query-files/lit.cfg \
+        --replace-fail "pythonExec + ' ' +OutputCheckTool" "OutputCheckTool"
+
+      # Results in duplication of Nix store paths and trouble finding the Python library at runtime
+      substituteInPlace bindings/python/stp/library_path.py.in_install \
+        --replace-fail "@CMAKE_INSTALL_PREFIX@/" ""
+    ''
+    + lib.optionalString useCadical ''
+      # Fix up Cadical paths.
+      substituteInPlace include/stp/Sat/Cadical.h \
+        --replace-fail "src/cadical.hpp" "cadical.hpp"
+
+      substituteInPlace CMakeLists.txt \
+        --replace-fail "build/libcadical.a" "lib/libcadical.a" \
+        --replace-fail 'include_directories(''${CADICAL_DIR}/)' 'include_directories(''${CADICAL_DIR}/include)'
+    '';
 
   buildInputs = [
     boost
     zlib
-    minisat
-    cryptominisat
     python3
+    gmp
+    minisat
+  ] ++ lib.optional (!useCadical) cryptominisat;
+
+  nativeBuildInputs = [
+    cmake
+    bison
+    flex
+    perl
+    pkg-config
+  ];
+
+  cmakeFlags =
+    let
+      # STP expects Cadical dependencies to all be in the same place.
+      cadicalDependency = symlinkJoin {
+        name = "stp-${finalAttrs.version}-cadical";
+        paths = [
+          cadical.lib
+          cadical.dev
+        ];
+      };
+    in
+    [
+      (lib.cmakeBool "BUILD_SHARED_LIBS" true)
+      (lib.cmakeBool "USE_CADICAL" useCadical)
+      (lib.cmakeBool "NOCRYPTOMINISAT" useCadical)
+      (lib.cmakeBool "FORCE_CMS" (!useCadical))
+      (lib.cmakeBool "ENABLE_TESTING" finalAttrs.doCheck)
+    ]
+    ++ lib.optional finalAttrs.doCheck (lib.cmakeFeature "LIT_ARGS" "-v")
+    ++ lib.optional useCadical (lib.cmakeFeature "CADICAL_DIR" (toString cadicalDependency));
+
+  # Fixes the following warning in the aarch64 build on Linux:
+  # lib/extlib-abc/aig/cnf/cnfData.c:4591:25: warning: result of comparison of
+  # constant 255 with expression of type 'signed char' is always false [-Wtautological-constant-out-of-range-compare]
+  # 4591 |         if ( pMemory[k] == (char)(-1) )
+  #
+  # This seems to cause an infinite loop in tests on aarch64-linux platforms.
+  #
+  # TODO: Remove these CFLAGS when they update to the version that pulls `abc` in with a submodule.
+  # https://github.com/stp/stp/issues/498#issuecomment-2611251631
+  CFLAGS = [ "-fsigned-char" ];
+
+  outputs = [
+    "dev"
+    "out"
   ];
-  nativeBuildInputs = [ cmake bison flex perl ];
-  preConfigure = ''
-    python_install_dir=$out/${python3.sitePackages}
-    mkdir -p $python_install_dir
-    cmakeFlagsArray=(
-      $cmakeFlagsArray
-      "-DBUILD_SHARED_LIBS=ON"
-      "-DPYTHON_LIB_INSTALL_DIR=$python_install_dir"
-    )
+
+  preConfigure =
+    ''
+      python_install_dir=$out/${python3.sitePackages}
+      mkdir -p $python_install_dir
+      cmakeFlagsArray+=(
+        "-DPYTHON_LIB_INSTALL_DIR=$python_install_dir"
+      )
+    ''
+    + lib.optionalString finalAttrs.doCheck ''
+      # Link in gtest and the output check utility.
+      mkdir -p deps
+      ln -s ${gtest.src} deps/gtest
+      ln -s ${outputcheck} deps/OutputCheck
+    '';
+
+  nativeCheckInputs = [
+    gtest
+    lit
+    outputcheck
+  ];
+
+  doCheck = true;
+
+  postInstall = ''
+    # Clean up installed gtest/gmock files that shouldn't be there.
+    shopt -s globstar nocaseglob
+    rm -rf $out/**/*g{test,mock}*
+
+    # Some of the gtest/gmock files were in the pkgconfig folders, which may now be empty.
+    find $out/ -name pkgconfig -type d -empty -delete
+
+    # Python bindings are broken:
+    substituteInPlace $python_install_dir/**/stp.py \
+      --replace-fail "from library_path import PATHS" "from .library_path import PATHS"
   '';
 
-  meta = with lib; {
+  doInstallCheck = true;
+  postInstallCheck = ''
+    $out/bin/stp --version | tee /dev/stderr | grep -F "STP version $version"
+
+    # Run the examples from the docs: https://stp.readthedocs.io/en/latest/#python-usage
+    for binary in stp stp_simple; do
+      echo "(set-logic QF_BV) (assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2))) (check-sat) (exit)" | tee /dev/stderr | $out/bin/$binary | grep "^sat$"
+    done
+    PYTHONPATH=$out/${python3.sitePackages} ${lib.getExe python3} -c \
+      "import stp; s = stp.Solver(); a, b, c = s.bitvec('a', 32), s.bitvec('b', 32), s.bitvec('c', 32); s.add(a == 5); s.add(b == 6); s.add(a + b == c); assert s.check(); print(s.model())" >&2
+  '';
+
+  passthru = {
+    updateScript = nix-update-script {
+      extraArgs = [
+        "--version-regex"
+        "^v(2\\.3\\.[0-9]+)$"
+      ];
+    };
+  };
+
+  meta = {
     description = "Simple Theorem Prover";
-    maintainers = with maintainers; [ McSinyx numinit ];
-    platforms = platforms.linux;
-    license = licenses.mit;
+    homepage = "https://stp.github.io/";
+    maintainers = with lib.maintainers; [
+      McSinyx
+      numinit
+    ];
+    platforms = with lib.platforms; linux ++ darwin;
+    license = lib.licenses.mit;
   };
-}
+})

pkgs/by-name/st/stp/stdint.patch

@@ -15779,6 +15779,10 @@ self: super: with self; {
 
   stop-words = callPackage ../development/python-modules/stop-words { };
 
+  stp = toPythonModule (pkgs.stp.override {
+    python3 = self.python;
+  });
+
   stransi = callPackage ../development/python-modules/stransi { };
 
   strategies = callPackage ../development/python-modules/strategies { };