From 814b85abd1e91ec1d9f6acf5c2645d671de08765 Mon Sep 17 00:00:00 2001 From: Morgan Jones Date: Sun, 13 Oct 2024 22:43:37 -0700 Subject: [PATCH] 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 | 156 ++++++++++++++++++++++++------- pkgs/by-name/st/stp/stdint.patch | 10 +- 2 files changed, 125 insertions(+), 41 deletions(-) diff --git a/pkgs/by-name/st/stp/package.nix b/pkgs/by-name/st/stp/package.nix index 1025663b1bd7c5..fbd45178122c10 100644 --- a/pkgs/by-name/st/stp/package.nix +++ b/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 ' -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; }; diff --git a/pkgs/by-name/st/stp/stdint.patch b/pkgs/by-name/st/stp/stdint.patch index 6595d55617315e..93927f146d5e9d 100644 --- a/pkgs/by-name/st/stp/stdint.patch +++ b/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 +#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"