From 2549be898de0eb535d6b1cd04728791b2935f23e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?J=C3=B6rg=20Thalheim?= Date: Sun, 14 May 2017 09:55:19 +0100 Subject: [PATCH] stp: 2014.01.07 -> 2.2.0 --- .../science/logic/stp/default.nix | 43 ++-- .../science/logic/stp/fixbuild.diff | 45 ---- .../science/logic/stp/fixrefs.diff | 192 ------------------ 3 files changed, 26 insertions(+), 254 deletions(-) delete mode 100644 pkgs/applications/science/logic/stp/fixbuild.diff delete mode 100644 pkgs/applications/science/logic/stp/fixrefs.diff diff --git a/pkgs/applications/science/logic/stp/default.nix b/pkgs/applications/science/logic/stp/default.nix index 444bb06c4a0..8c0b82cc549 100644 --- a/pkgs/applications/science/logic/stp/default.nix +++ b/pkgs/applications/science/logic/stp/default.nix @@ -1,23 +1,32 @@ -{stdenv, cmake, boost, bison, flex, fetchgit, perl, zlib}: +{ stdenv, cmake, boost, bison, flex, fetchFromGitHub, perl, python3, python3Packages, zlib, minisatUnstable, cryptominisat }: + stdenv.mkDerivation rec { - version = "2014.01.07"; + version = "2.2.0"; name = "stp-${version}"; - src = fetchgit { - url = "git://github.com/stp/stp"; - rev = "3aa11620a823d617fc033d26aedae91853d18635"; - sha256 = "832520787f57f63cf47364d080f30ad10d6d6e00f166790c19b125be3d6dd45c"; + + src = fetchFromGitHub { + owner = "stp"; + repo = "stp"; + rev = "stp-${version}"; + sha256 = "1jh23wjm62nnqfx447g2y53bbangq04hjrvqc35v9xxpcjgj3i49"; }; - buildInputs = [ cmake boost bison flex perl zlib ]; - cmakeFlags = [ "-DBUILD_SHARED_LIBS=ON" ]; - patchPhase = '' - sed -e 's,^export(PACKAGE.*,,' -i CMakeLists.txt - patch -p1 < ${./fixbuild.diff} - patch -p1 < ${./fixrefs.diff} + + buildInputs = [ boost zlib minisatUnstable cryptominisat python3 ]; + nativeBuildInputs = [ cmake bison flex perl ]; + preConfigure = '' + python_install_dir=$out/${python3Packages.python.sitePackages} + mkdir -p $python_install_dir + cmakeFlagsArray=( + $cmakeFlagsArray + "-DBUILD_SHARED_LIBS=ON" + "-DPYTHON_LIB_INSTALL_DIR=$python_install_dir" + ) ''; - meta = { - description = ''Simple Theorem Prover''; - maintainers = with stdenv.lib.maintainers; [mornfall]; - platforms = with stdenv.lib.platforms; linux; - license = stdenv.lib.licenses.mit; + + meta = with stdenv.lib; { + description = "Simple Theorem Prover"; + maintainers = with maintainers; [ mornfall ]; + platforms = platforms.linux; + license = licenses.mit; }; } diff --git a/pkgs/applications/science/logic/stp/fixbuild.diff b/pkgs/applications/science/logic/stp/fixbuild.diff deleted file mode 100644 index 01782cb4f40..00000000000 --- a/pkgs/applications/science/logic/stp/fixbuild.diff +++ /dev/null @@ -1,45 +0,0 @@ -diff --git a/src/libstp/CMakeLists.txt b/src/libstp/CMakeLists.txt -index 83bd03a..9c0304b 100644 ---- a/src/libstp/CMakeLists.txt -+++ b/src/libstp/CMakeLists.txt -@@ -23,6 +23,15 @@ set(stp_lib_targets - printer - ) - -+include_directories(${CMAKE_SOURCE_DIR}/src/AST/) -+include_directories(${CMAKE_BINARY_DIR}/src/AST/) -+ -+add_library(globalstp OBJECT -+ ../main/Globals.cpp -+ ${CMAKE_CURRENT_BINARY_DIR}/../main/GitSHA1.cpp -+) -+add_dependencies(globalstp ASTKind_header) -+ - # Create list of objects and gather list of - # associated public headers. - set(stp_lib_objects "") -@@ -31,6 +40,7 @@ foreach(target ${stp_lib_targets}) - list(APPEND stp_lib_objects $) - - get_target_property(TARGETS_PUBLIC_HEADERS ${target} PUBLIC_HEADER) -+ set_target_properties(${target} PROPERTIES POSITION_INDEPENDENT_CODE ON) - if (EXISTS "${TARGETS_PUBLIC_HEADERS}") - list(APPEND stp_public_headers "${TARGETS_PUBLIC_HEADERS}") - message("Adding public header(s) ${TARGETS_PUBLIC_HEADERS} to target libstp") -diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt -index 0735137..73039f5 100644 ---- a/src/main/CMakeLists.txt -+++ b/src/main/CMakeLists.txt -@@ -3,12 +3,6 @@ include_directories(${CMAKE_BINARY_DIR}/src/AST/) - - configure_file("${CMAKE_CURRENT_SOURCE_DIR}/GitSHA1.cpp.in" "${CMAKE_CURRENT_BINARY_DIR}/GitSHA1.cpp" @ONLY) - --add_library(globalstp OBJECT -- Globals.cpp -- ${CMAKE_CURRENT_BINARY_DIR}/GitSHA1.cpp --) --add_dependencies(globalstp ASTKind_header) -- - # ----------------------------------------------------------------------------- - # Create binary - # ----------------------------------------------------------------------------- diff --git a/pkgs/applications/science/logic/stp/fixrefs.diff b/pkgs/applications/science/logic/stp/fixrefs.diff deleted file mode 100644 index 60ad4949f07..00000000000 --- a/pkgs/applications/science/logic/stp/fixrefs.diff +++ /dev/null @@ -1,192 +0,0 @@ -commit 53b6043e25b2eba264faab845077fbf6736cf22f -Author: Petr Rockai -Date: Tue Jan 7 13:30:07 2014 +0100 - - aig: Comment out unused functions with undefined references in them. - -diff --git a/src/extlib-abc/aig/aig/aigPart.c b/src/extlib-abc/aig/aig/aigPart.c -index a4cc116..5bd5f08 100644 ---- a/src/extlib-abc/aig/aig/aigPart.c -+++ b/src/extlib-abc/aig/aig/aigPart.c -@@ -869,6 +869,7 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi - SeeAlso [] - - ***********************************************************************/ -+#if 0 - Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) - { - extern int Cmd_CommandExecute( void * pAbc, char * sCommand ); -@@ -981,6 +982,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) - Aig_ManMarkValidChoices( pAig ); - return pAig; - } -+#endif - - - //////////////////////////////////////////////////////////////////////// -diff --git a/src/extlib-abc/aig/aig/aigShow.c b/src/extlib-abc/aig/aig/aigShow.c -index ae8fa8b..f04eedc 100644 ---- a/src/extlib-abc/aig/aig/aigShow.c -+++ b/src/extlib-abc/aig/aig/aigShow.c -@@ -326,6 +326,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * - SeeAlso [] - - ***********************************************************************/ -+#if 0 - void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) - { - extern void Abc_ShowFile( char * FileNameDot ); -@@ -347,7 +348,7 @@ void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) - // visualize the file - Abc_ShowFile( FileNameDot ); - } -- -+#endif - - //////////////////////////////////////////////////////////////////////// - /// END OF FILE /// -diff --git a/src/extlib-abc/aig/dar/darRefact.c b/src/extlib-abc/aig/dar/darRefact.c -index d744b4f..23fc3d5 100644 ---- a/src/extlib-abc/aig/dar/darRefact.c -+++ b/src/extlib-abc/aig/dar/darRefact.c -@@ -340,6 +340,7 @@ printf( "\n" ); - SeeAlso [] - - ***********************************************************************/ -+#if 0 - int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, int Required ) - { - Vec_Ptr_t * vCut; -@@ -428,6 +429,7 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in - } - return p->GainBest; - } -+#endif - - /**Function************************************************************* - -@@ -461,6 +463,7 @@ int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin ) - SeeAlso [] - - ***********************************************************************/ -+#if 0 - int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) - { - // Bar_Progress_t * pProgress; -@@ -583,6 +586,7 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; - return 1; - - } -+#endif - - //////////////////////////////////////////////////////////////////////// - /// END OF FILE /// -diff --git a/src/extlib-abc/aig/dar/darScript.c b/src/extlib-abc/aig/dar/darScript.c -index e60df00..1b9c24f 100644 ---- a/src/extlib-abc/aig/dar/darScript.c -+++ b/src/extlib-abc/aig/dar/darScript.c -@@ -64,6 +64,7 @@ Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig ) - SeeAlso [] - - ***********************************************************************/ -+#if 0 - Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) - //alias rwsat "st; rw -l; b -l; rw -l; rf -l" - { -@@ -108,7 +109,7 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) - - return pAig; - } -- -+#endif - - /**Function************************************************************* - -@@ -121,6 +122,7 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) - SeeAlso [] - - ***********************************************************************/ -+#if 0 - Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ) - //alias compress2 "b -l; rw -l; rwz -l; b -l; rwz -l; b -l" - { -@@ -180,6 +182,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i - - return pAig; - } -+#endif - - /**Function************************************************************* - -@@ -192,6 +195,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i - SeeAlso [] - - ***********************************************************************/ -+#if 0 - Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ) - //alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" - { -@@ -285,6 +289,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, - } - return pAig; - } -+#endif - - /**Function************************************************************* - -@@ -297,6 +302,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, - SeeAlso [] - - ***********************************************************************/ -+#if 0 - Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ) - //alias resyn "b; rw; rwz; b; rwz; b" - //alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" -@@ -311,6 +317,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL - Vec_PtrPush( vAigs, pAig ); - return vAigs; - } -+#endif - - /**Function************************************************************* - -diff --git a/src/extlib-abc/aig/kit/kitAig.c b/src/extlib-abc/aig/kit/kitAig.c -index de301f2..7e5df0f 100644 ---- a/src/extlib-abc/aig/kit/kitAig.c -+++ b/src/extlib-abc/aig/kit/kitAig.c -@@ -95,6 +95,7 @@ Aig_Obj_t * Kit_GraphToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, Kit_Graph_t - SeeAlso [] - - ***********************************************************************/ -+#if 0 - Aig_Obj_t * Kit_TruthToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, unsigned * pTruth, int nVars, Vec_Int_t * vMemory ) - { - Aig_Obj_t * pObj; -@@ -113,6 +114,7 @@ Aig_Obj_t * Kit_TruthToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, unsigned * p - Kit_GraphFree( pGraph ); - return pObj; - } -+#endif - - //////////////////////////////////////////////////////////////////////// - /// END OF FILE /// -diff --git a/src/extlib-abc/aig/kit/kitGraph.c b/src/extlib-abc/aig/kit/kitGraph.c -index 39ef587..0485c66 100644 ---- a/src/extlib-abc/aig/kit/kitGraph.c -+++ b/src/extlib-abc/aig/kit/kitGraph.c -@@ -349,6 +349,7 @@ unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph ) - SeeAlso [] - - ***********************************************************************/ -+#if 0 - Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory ) - { - Kit_Graph_t * pGraph; -@@ -365,6 +366,7 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor - pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory ); - return pGraph; - } -+#endif - - /**Function************************************************************* -