stp: 2.3.3 -> 2.3.4

Bump the version, enable checkPhase, and create an installCheckPhase. Turn on Darwin support (it works) and fix the Python libs. Use cadical by default, though support `useCadical = false` in an override if users want to disable it.
2025-02-15 21:24:33 -08:00
parent 866edf51b8
commit 8f31d5335e
3 changed files with 165 additions and 62 deletions
@@ -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
  ];
-  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"
-    )
+
+  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"
+  ];
+
+  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; {
-    description = "Simple Theorem Prover";
-    maintainers = with maintainers; [ McSinyx numinit ];
-    platforms = platforms.linux;
-    license = licenses.mit;
+  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";
+    homepage = "https://stp.github.io/";
+    maintainers = with lib.maintainers; [
+      McSinyx
+      numinit
+    ];
+    platforms = with lib.platforms; linux ++ darwin;
+    license = lib.licenses.mit;
+  };
+})
@@ -1,16 +0,0 @@
-diff --git a/include/stp/AST/ASTNode.h b/include/stp/AST/ASTNode.h
-index 91acd726182c..0a17db23ffbf 100644
--- a/include/stp/AST/ASTNode.h
-+++ b/include/stp/AST/ASTNode.h
-@@ -24,9 +24,10 @@ THE SOFTWARE.
- #ifndef ASTNODE_H
- #define ASTNODE_H
- 
-+#include "stp/AST/ASTInternal.h"
- #include "stp/AST/NodeFactory/HashingNodeFactory.h"
-+#include "stp/AST/UsefulDefs.h"
- #include "stp/Util/Attributes.h"
-#include "ASTInternal.h"
- #include "stp/Globals/Globals.h"
- 
- namespace stp
@@ -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 { };