stp: 2.3.3 -> 2.3.4

Bump the version, enable checkPhase, and create an installCheckPhase.
Use cadical by default, though support `useCadical = false` in an
override if users want to disable it.

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

@@ -1,27 +1,36 @@
-{ lib
-, stdenv
-, cmake
-, boost
-, bison
-, flex
-, fetchFromGitHub
-, fetchpatch
-, perl
-, python3
-, zlib
-, minisat
-, cryptominisat
+{
+  lib,
+  clangStdenv,
+  cmake,
+  boost,
+  bison,
+  flex,
+  pkg-config,
+  fetchFromGitHub,
+  fetchpatch,
+  symlinkJoin,
+  perl,
+  python3,
+  zlib,
+  minisat,
+  cryptominisat,
+  gmp,
+  cadical,
+  gtest,
+  lit,
+  outputcheck,
+  useCadical ? true,
 }:
 
-stdenv.mkDerivation rec {
+clangStdenv.mkDerivation rec {
   pname = "stp";
-  version = "2.3.3";
+  version = "2.3.4";
 
   src = fetchFromGitHub {
     owner = "stp";
     repo = "stp";
-    rev = version;
-    hash = "sha256-B+HQF4TJPkYrpodE4qo4JHvlu+a5HTJf1AFyXTnZ4vk=";
+    rev = "${version}_cadical";
+    hash = "sha256-fNx3/VS2bimlVwCejEZtNGDqVKnwBm0O2YkIUQm6eDM=";
   };
   patches = [
     # Fix missing type declaration
@@ -35,36 +44,111 @@ stdenv.mkDerivation rec {
       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"
+    ''
+    + 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
+    gtest
+    lit
   ];
-  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
+      onOff = var: flag: lib.singleton "-D${var}=${if flag then "ON" else "OFF"}";
+    in
+    onOff "BUILD_SHARED_LIBS" true
+    ++ onOff "USE_CADICAL" useCadical
+    ++ onOff "NOCRYPTOMINISAT" useCadical
+    ++ onOff "FORCE_CMS" (!useCadical)
+    ++ lib.optional useCadical "-DCADICAL_DIR=${
+      # STP expects Cadical dependencies to all be in the same place.
+      symlinkJoin {
+        name = "stp-cadical-deps";
+        paths = [
+          cadical.lib
+          cadical.dev
+        ];
+      }
+    }"
+    ++ onOff "ENABLE_TESTING" doCheck
+    ++ lib.optional doCheck "-DLIT_ARGS=-v";
+
+  preConfigure =
+    ''
+      python_install_dir=$out/${python3.sitePackages}
+      mkdir -p $python_install_dir
+      cmakeFlagsArray+=(
+        "-DPYTHON_LIB_INSTALL_DIR=$python_install_dir"
+      )
+    ''
+    + lib.optionalString doCheck ''
+      # Link in gtest and the output check utility.
+      mkdir -p deps
+      ln -s ${gtest.src} deps/gtest
+      ln -s ${outputcheck} deps/OutputCheck
+    '';
+
+  # Seems to hang on the following on aarch64:
+  # - array-iteTests-gtest
+  # - if-checkTests-gtest
+  # - leaksTests-gtest
+  # - stp-div-001Tests-gtest
+  # - mdempskyTests-gtest
+  # - example_brokenTests-gtest
+  doCheck = lib.warnIf (!clangStdenv.isx86_64) ''
+    STP has not been validated on this platform. Disabling the test suite.
+  '' clangStdenv.isx86_64;
+
+  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
+  '';
+
+  doInstallCheck = true;
+  postInstallCheck = ''
+    $out/bin/stp --version | grep '^STP version ${version}'
   '';
 
   meta = with lib; {
     description = "Simple Theorem Prover";
-    maintainers = with maintainers; [ McSinyx numinit ];
+    homepage = "https://stp.github.io/";
+    maintainers = with maintainers; [
+      McSinyx
+      numinit
+    ];
     platforms = platforms.linux;
     license = licenses.mit;
   };

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

@@ -1,13 +1,13 @@
 diff --git a/include/stp/AST/ASTNode.h b/include/stp/AST/ASTNode.h
-index 91acd726182c..0a17db23ffbf 100644
+index a05c15d6..a823d95d 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
+@@ -26,9 +26,10 @@ THE SOFTWARE.
+
+ #include <cstdint>
 
 +#include "stp/AST/ASTInternal.h"
- #include "stp/AST/NodeFactory/HashingNodeFactory.h"
+ #include "stp/NodeFactory/HashingNodeFactory.h"
 +#include "stp/AST/UsefulDefs.h"
  #include "stp/Util/Attributes.h"
 -#include "ASTInternal.h"