diff --git a/math/boolector/Makefile b/math/boolector/Makefile index 67612a6808f0..0d69f8ae44fe 100644 --- a/math/boolector/Makefile +++ b/math/boolector/Makefile @@ -1,34 +1,35 @@ PORTNAME= boolector DISTVERSION= 3.2.3 +PORTREVISION= 1 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 +BUILD_DEPENDS= ${LOCALBASE}/lib/liblgl.a:math/lingeling LIB_DEPENDS= libbtor2parser.so:math/btor2tools \ + libcadical.so:math/cadical \ libcryptominisat5.so:math/cryptominisat \ libminisat.so:math/minisat \ libpicosat.so:math/picosat \ libgmp.so:math/gmp TEST_DEPENDS= bash:shells/bash USES= cmake:noninja,testing 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_OFF= TESTING CMAKE_TESTING_ON= TESTING # tests fail to comile, see https://github.com/Boolector/boolector/issues/216 CMAKE_ARGS= -DCaDiCaL_INCLUDE_DIR=${LOCALBASE}/include .include diff --git a/math/cadical/Makefile b/math/cadical/Makefile index fdd221995ad1..f8e39d9c1d5e 100644 --- a/math/cadical/Makefile +++ b/math/cadical/Makefile @@ -1,43 +1,56 @@ PORTNAME= cadical DISTVERSIONPREFIX= rel- DISTVERSION= 1.9.5 +PORTREVISION= 1 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 + lib/libcadical.a \ + lib/libcadical.so \ + lib/libcadical.so.${DISTVERSION} + +post-build: # build shared library + @${ECHO} "==> Building the shared library" + cd ${WRKSRC}/src && ${CXX} \ + -shared -Wl,-soname=lib${PORTNAME}.so.$(DISTVERSION) -fPIC \ + -DNDEBUG \ + ${CXXFLAGS} ${LDFLAGS} \ + `${ECHO} *.cpp | ${SED} -e "s/cadical\.cpp//; s/mobical\.cpp//"` \ + -I ${WRKSRC}/build \ + -o ${WRKSRC}/build/lib${PORTNAME}.so.${DISTVERSION} 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 + ${INSTALL_LIB} ${WRKSRC}/build/libcadical.so.${DISTVERSION} ${STAGEDIR}${PREFIX}/lib + cd ${STAGEDIR}${PREFIX}/lib && ${LN} -s libcadical.so.${DISTVERSION} libcadical.so .include diff --git a/math/cvc5/Makefile b/math/cvc5/Makefile index 6a314f7e0dd8..f35fca75a780 100644 --- a/math/cvc5/Makefile +++ b/math/cvc5/Makefile @@ -1,95 +1,96 @@ PORTNAME= cvc5 DISTVERSIONPREFIX= cvc5- DISTVERSION= 1.1.2 +PORTREVISION= 1 CATEGORIES= math java 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}tomli>0:textproc/py-tomli@${PY_FLAVOR} \ ${PYTHON_PKGNAMEPREFIX}pyparsing>0:devel/py-pyparsing@${PY_FLAVOR} -LIB_DEPENDS= libantlr3c.so:devel/libantlr3c +LIB_DEPENDS= libantlr3c.so:devel/libantlr3c \ + libcadical.so:math/cadical USES= cmake:testing ncurses compiler:c++17-lang \ localbase:ldflags pkgconfig python:build USE_LDCONFIG= yes USE_GITHUB= yes USE_JAVA= yes JAVA_BUILD= yes CMAKE_BUILD_TYPE= Production CMAKE_ARGS+= -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 PLIST_SUB= VERSION=${DISTVERSION} 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:^[1-9]\.[0-9]+\.[0-9]+ # prevent older generation versions like 1.8, 1.7, etc. # some tests are skipped without any explanation, see https://github.com/cvc5/cvc5/issues/10456 .include