diff --git a/math/boolector/Makefile b/math/boolector/Makefile index 419bf7877c46..9bc42a36a4be 100644 --- a/math/boolector/Makefile +++ b/math/boolector/Makefile @@ -1,43 +1,43 @@ PORTNAME= boolector DISTVERSION= 3.2.2 -PORTREVISION= 1 +PORTREVISION= 2 CATEGORIES= math MAINTAINER= yuri@FreeBSD.org COMMENT= Satisfiability Modulo Theories (SMT) solver WWW= https://boolector.github.io/ LICENSE= MIT LICENSE_FILE= ${WRKSRC}/COPYING BUILD_DEPENDS= ${LOCALBASE}/lib/libcadical.a:math/cadical \ ${LOCALBASE}/lib/liblgl.a:math/lingeling LIB_DEPENDS= libbtor2parser.so:math/btor2tools \ libcryptominisat5.so:math/cryptominisat \ libminisat.so:math/minisat \ libpicosat.so:math/picosat \ libgmp.so:math/gmp TEST_DEPENDS= bash:shells/bash USES= cmake:noninja compiler:c++11-lang cpe python:test # ninja fails to build tests CPE_VENDOR= boolector_project USE_GITHUB= yes GH_ACCOUNT= Boolector CMAKE_ON= BUILD_SHARED_LIBS \ USE_GMP CMAKE_ARGS= -DCaDiCaL_INCLUDE_DIR=${LOCALBASE}/include do-test: @${FIND} ${WRKDIR} -name "*.py" \ | ${XARGS} ${REINPLACE_CMD} -e 's|#!/usr/bin/env python$$|#!${PYTHON_CMD}| ; s|#!/usr/bin/env python3$$|#!${PYTHON_CMD}|' @${FIND} ${WRKDIR} -name "*.sh" \ | ${XARGS} ${REINPLACE_CMD} 's|#!/bin/bash$$|#!${LOCALBASE}/bin/bash|' @cd ${BUILD_WRKSRC} && \ ${SETENV} ${CONFIGURE_ENV} ${CMAKE_BIN} ${CMAKE_ARGS} -DBUILD_TESTING:BOOL=ON ${CMAKE_SOURCE_PATH} && \ ${SETENV} ${MAKE_ENV} ${MAKE_CMD} ${MAKE_ARGS} ${ALL_TARGET} && \ ${SETENV} ${MAKE_ENV} ${MAKE_CMD} ${MAKE_ARGS} test .include diff --git a/math/cadical/Makefile b/math/cadical/Makefile index 815d8cb14cd1..fef83a185bf9 100644 --- a/math/cadical/Makefile +++ b/math/cadical/Makefile @@ -1,43 +1,43 @@ PORTNAME= cadical DISTVERSIONPREFIX= rel- -DISTVERSION= 1.5.3 +DISTVERSION= 1.6.0 CATEGORIES= math devel MAINTAINER= yuri@FreeBSD.org COMMENT= Simple CDCL satisfiability solver WWW= http://fmv.jku.at/cadical/ LICENSE= MIT LICENSE_FILE= ${WRKSRC}/LICENSE USES= compiler:c++0x gmake tar:xz USE_GITHUB= yes GH_ACCOUNT= arminbiere GNU_CONFIGURE= yes CXXFLAGS+= -fPIC MAKEFILE= makefile BINARY_ALIAS= make=${GMAKE} EXES= cadical mobical TEST_TARGET= test PLIST_FILES= ${EXES:S/^/bin\//} \ include/cadical.hpp \ include/ccadical.h \ lib/libcadical.a do-install: # workaround for https://github.com/arminbiere/cadical/issues/49 .for e in ${EXES} ${INSTALL_PROGRAM} ${WRKSRC}/build/${e} ${STAGEDIR}${PREFIX}/bin .endfor ${INSTALL_DATA} ${WRKSRC}/src/cadical.hpp ${STAGEDIR}${PREFIX}/include ${INSTALL_DATA} ${WRKSRC}/src/ccadical.h ${STAGEDIR}${PREFIX}/include ${INSTALL_DATA} ${WRKSRC}/build/libcadical.a ${STAGEDIR}${PREFIX}/lib .include diff --git a/math/cadical/distinfo b/math/cadical/distinfo index ee0e226276a6..0efebe577ed3 100644 --- a/math/cadical/distinfo +++ b/math/cadical/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1672780757 -SHA256 (arminbiere-cadical-rel-1.5.3_GH0.tar.gz) = 0ff521ed36d57478a8dbc610e0d27536c9d3a2154d859152f33f8733a6dca31e -SIZE (arminbiere-cadical-rel-1.5.3_GH0.tar.gz) = 596378 +TIMESTAMP = 1687708706 +SHA256 (arminbiere-cadical-rel-1.6.0_GH0.tar.gz) = 104a271f7448827f5b48798e0b305b150631df6a6bca1106b3d2b4ea4044efab +SIZE (arminbiere-cadical-rel-1.6.0_GH0.tar.gz) = 618384 diff --git a/math/cadical/files/patch-src_mobical.cpp b/math/cadical/files/patch-src_mobical.cpp deleted file mode 100644 index 096b51f70222..000000000000 --- a/math/cadical/files/patch-src_mobical.cpp +++ /dev/null @@ -1,18 +0,0 @@ -- workaround for https://github.com/arminbiere/cadical/issues/48 - ---- src/mobical.cpp.orig 2022-08-17 10:12:36 UTC -+++ src/mobical.cpp -@@ -2611,7 +2611,12 @@ Mobical::Mobical () - { - const int prot = PROT_READ | PROT_WRITE; - const int flags = MAP_ANONYMOUS | MAP_SHARED; -- shared = (Shared*) mmap (0, sizeof *shared, prot, flags, 0, 0); -+ void *m = mmap (0, sizeof *shared, prot, flags, -1, 0); -+ if (m == MAP_FAILED) { -+ perror("mmap failed"); -+ exit(1); -+ } -+ shared = (Shared*)m; - } - - Mobical::~Mobical () { diff --git a/math/cvc5/Makefile b/math/cvc5/Makefile index 8d9bcdef596d..e66fdc5dfa2e 100644 --- a/math/cvc5/Makefile +++ b/math/cvc5/Makefile @@ -1,105 +1,105 @@ PORTNAME= cvc5 DISTVERSIONPREFIX= cvc5- DISTVERSION= 1.0.5 -PORTREVISION= 1 +PORTREVISION= 2 CATEGORIES= math java MASTER_SITES+= http://www.antlr3.org/download/:antlr3 DISTFILES+= antlr-3.4-complete.jar:antlr3 EXTRACT_ONLY= ${DISTNAME}${EXTRACT_SUFX} MAINTAINER= yuri@FreeBSD.org COMMENT= Automatic theorem prover for SMT (Satisfiability Modulo Theories) WWW= https://cvc5.github.io/ LICENSE= BSD3CLAUSE LICENSE_FILE= ${WRKSRC}/COPYING BUILD_DEPENDS= bash:shells/bash \ ${LOCALBASE}/lib/libcadical.a:math/cadical \ ${LOCALBASE}/lib/symfpu.a:math/symfpu \ ${PYTHON_PKGNAMEPREFIX}toml>0:textproc/py-toml@${PY_FLAVOR} \ ${PYTHON_PKGNAMEPREFIX}pyparsing>0:devel/py-pyparsing@${PY_FLAVOR} LIB_DEPENDS= libantlr3c.so:devel/libantlr3c \ libboost_system.so:devel/boost-libs USES= cmake:testing ncurses compiler:c++17-lang \ localbase:ldflags pkgconfig python:3.5+,build USE_LDCONFIG= yes USE_GITHUB= yes USE_JAVA= yes JAVA_BUILD= yes CMAKE_BUILD_TYPE= Production CMAKE_ARGS+= -DANTLR_BINARY=${WRKDIR}/antlr3 \ -DFREEBSD_DISTDIR=${DISTDIR} \ -DPython_EXECUTABLE:STRING=${PYTHON_CMD} CMAKE_ON= BUILD_SHARED_LIBS CMAKE_OFF= BUILD_BINDINGS_PYTHON USE_PYTHON3 # Python binding should be a separate port CMAKE_TESTING_ON= ENABLE_UNIT_TESTING CMAKE_TESTING_TARGET= check # check target runs only quick tests (based on https://github.com/cvc5/cvc5/issues/9569#issuecomment-1484943348) #CMAKE_TESTING_TARGET= test # test target also runs longer tests, 2 of which fail, see https://github.com/cvc5/cvc5/issues/9569 OPTIONS_DEFINE= COCOALIB EDITLINE JAVA OPTIONS_GROUP= SOLVERS OPTIONS_GROUP_SOLVERS= CRYPTOMINISAT KISSAT OPTIONS_RADIO= NUMLIB OPTIONS_RADIO_NUMLIB= GMP CLN OPTIONS_DEFAULT= CRYPTOMINISAT EDITLINE JAVA GMP # COCOALIB KISSAT OPTIONS_SUB= yes COCOALIB_DESC= Use CoCoALib for further polynomial operations COCOALIB_CMAKE_BOOL= USE_COCOA COCOALIB_BROKEN= fails to compile with cocoalib, see https://github.com/cvc5/cvc5/issues/9484 JAVA_CMAKE_BOOL= BUILD_BINDINGS_JAVA JAVA_CMAKE_ON= -DJAVA_INCLUDE_PATH:PATH=${JAVA_HOME}/include \ -DJAVA_AWT_LIBRARY:PATH=${JAVA_HOME}/jre/lib/${ARCH}/libjawt.so \ -DJAVA_JVM_LIBRARY:PATH=${JAVA_HOME}/jre/lib/${ATCH}/libjava.so JAVA_BUILD_DEPENDS= swig:devel/swig EDITLINE_DESC= Use Editline for better interactive support EDITLINE_CMAKE_BOOL= USE_EDITLINE EDITLINE_BUILD_DEPENDS= libedit>0:devel/libedit EDITLINE_RUN_DEPENDS= libedit>0:devel/libedit # SOLVERS options CRYPTOMINISAT_DESC= Use CryptoMiniSat as the SAT solver CRYPTOMINISAT_CMAKE_BOOL= USE_CRYPTOMINISAT CRYPTOMINISAT_LIB_DEPENDS= libcryptominisat5.so:math/cryptominisat KISSAT_DESC= Use Kissat solver KISSAT_CMAKE_BOOL= USE_KISSAT KISSAT_BROKEN= fails to link with libkissat.so, see https://github.com/cvc5/cvc5/issues/9483 # NUMLIB options GMP_DESC= Use GMP numeric library GMP_LIB_DEPENDS= libgmp.so:math/gmp CLN_DESC= Use CLN numeric library CLN_CMAKE_BOOL= USE_CLN CLN_LIB_DEPENDS= libcln.so:math/cln \ libgmp.so:math/gmp .include .if ${PORT_OPTIONS:MCLN} LICENSE= GPLv3 CMAKE_ARGS+= -DENABLE_GPL:BOOL=ON .endif PORTSCOUT= limit:^cvc5-[1-9].* # prevent older generation versions like 1.8 post-extract: @${CP} ${DISTDIR}/antlr-3.4-complete.jar ${WRKDIR}/antlr3.jar @${ECHO_CMD} "#!/bin/sh" > ${WRKDIR}/antlr3 @${ECHO_CMD} "exec \"${LOCALBASE}/bin/java\" -classpath \"${WRKDIR}/antlr3.jar\" org.antlr.Tool \"\$$@\"" >> ${WRKDIR}/antlr3 @${CHMOD} +x ${WRKDIR}/antlr3 xpost-patch: @${REINPLACE_CMD} -e "s|sed -i'' -e 's|sed -i '' -e 's|g" \ ${WRKSRC}/src/fix-install-headers.sh .include