diff --git a/math/bitwuzla/Makefile b/math/bitwuzla/Makefile index 2a9354538866..63387ea1b148 100644 --- a/math/bitwuzla/Makefile +++ b/math/bitwuzla/Makefile @@ -1,35 +1,36 @@ PORTNAME= bitwuzla DISTVERSION= 0.7.0 +PORTREVISION= 1 CATEGORIES= math MAINTAINER= yuri@FreeBSD.org COMMENT= SMT solver for the theories of fixed-size bit-vectors WWW= https://bitwuzla.github.io/ LICENSE= MIT LICENSE_FILE= ${WRKSRC}/COPYING BUILD_DEPENDS= gmp>0:math/gmp \ ${LOCALBASE}/lib/symfpu.a:math/symfpu LIB_DEPENDS= libcadical.so:math/cadical \ libgmp.so:math/gmp TEST_DEPENDS= googletest>0:devel/googletest USES= compiler:c++17-lang localbase:ldflags meson pkgconfig python:build USE_GITHUB= yes USE_LDCONFIG= yes LDFLAGS+= -lcadical MESON_ARGS= -Ddefault_library=shared \ -Dtesting=disabled BINARY_ALIAS= git=false do-test: # 1 test hangs, see https://github.com/bitwuzla/bitwuzla/issues/117 @cd ${WRKSRC} && \ ${SETENV} ${CONFIGURE_ENV} ${CONFIGURE_CMD} ${CONFIGURE_ARGS} -Dtesting=enabled && \ cd ${BUILD_WRKSRC} && \ ${DO_MAKE_BUILD} test .include diff --git a/math/boolector/Makefile b/math/boolector/Makefile index 2450bea7df94..4d654fa79dbf 100644 --- a/math/boolector/Makefile +++ b/math/boolector/Makefile @@ -1,38 +1,39 @@ PORTNAME= boolector DISTVERSION= 3.2.4 +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/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:build,test shebangfix CPE_VENDOR= boolector_project USE_GITHUB= yes GH_ACCOUNT= Boolector SHEBANG_GLOB= *.sh CMAKE_ON= BUILD_SHARED_LIBS \ USE_GMP CMAKE_OFF= TESTING CMAKE_TESTING_ON= TESTING # 1 test hangs, see https://github.com/Boolector/boolector/issues/227 CMAKE_ARGS= -DCaDiCaL_INCLUDE_DIR=${LOCALBASE}/include BINARY_ALIAS= python=${PYTHON_CMD} python3=${PYTHON_CMD} # only for tests .include diff --git a/math/cadiback/Makefile b/math/cadiback/Makefile index 1b7786ef63dd..594109c0d317 100644 --- a/math/cadiback/Makefile +++ b/math/cadiback/Makefile @@ -1,50 +1,51 @@ PORTNAME= cadiback DISTVERSION= g20240729 +PORTREVISION= 1 CATEGORIES= math devel MAINTAINER= yuri@FreeBSD.org COMMENT= CaDiBack BackBone Extractor WWW= https://github.com/arminbiere/cadiback LICENSE= MIT LICENSE_FILE= ${WRKSRC}/LICENSE BUILD_DEPENDS= ${NONEXISTENT}:math/cadical:patch LIB_DEPENDS= libcadical.so:math/cadical USES= gmake localbase:ldflags USE_GITHUB= yes GH_ACCOUNT= arminbiere GH_TAGNAME= 789329d MAKEFILE= makefile TEST_TARGET= test PLIST_FILES= bin/${PORTNAME} do-build: cd ${WRKSRC} && \ ( \ ${ECHO} "#define VERSION \"`cat VERSION`\""; \ ${ECHO} "#define GITID \"${GH_TAGNAME}\""; \ ${ECHO} "#define BUILD \"${CXX} -W\""; \ ) > config.hpp && \ ${CXX} \ -DNDEBUG \ ${CXXFLAGS} ${LDFLAGS} \ -I ${WRKSRC_cadical}/src \ cadiback.cpp \ -I `${MAKE} -V WRKSRC -C ${PORTSDIR}/math/cadical`/src \ -l cadical \ -o ${PORTNAME} do-install: ${INSTALL_PROGRAM} ${WRKSRC}/${PORTNAME} ${STAGEDIR}${PREFIX}/bin/${PORTNAME} do-test: @cd ${WRKSRC}/test && \ ./run.sh .include diff --git a/math/cadical/Makefile b/math/cadical/Makefile index 044ecfaffdd0..67a944066d57 100644 --- a/math/cadical/Makefile +++ b/math/cadical/Makefile @@ -1,55 +1,55 @@ PORTNAME= cadical DISTVERSIONPREFIX= rel- -DISTVERSION= 2.0.0 +DISTVERSION= 2.1.3 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 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.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/cadical/distinfo b/math/cadical/distinfo index 7c8447d30fa9..945a9f90c070 100644 --- a/math/cadical/distinfo +++ b/math/cadical/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1727899500 -SHA256 (arminbiere-cadical-rel-2.0.0_GH0.tar.gz) = 9afe5f6439442d854e56fc1fac3244ce241dbb490735939def8fd03584f89331 -SIZE (arminbiere-cadical-rel-2.0.0_GH0.tar.gz) = 709136 +TIMESTAMP = 1750305187 +SHA256 (arminbiere-cadical-rel-2.1.3_GH0.tar.gz) = abfe890aa4ccda7b8449c7ad41acb113cfb8e7e8fbf5e49369075f9b00d70465 +SIZE (arminbiere-cadical-rel-2.1.3_GH0.tar.gz) = 731545 diff --git a/math/lean4/Makefile b/math/lean4/Makefile index f88c468e34d0..acc607f13634 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,67 +1,68 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v DISTVERSION= 4.20.1 +PORTREVISION= 1 CATEGORIES= math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment MAINTAINER= yuri@FreeBSD.org COMMENT= Theorem prover and functional language for math (new gen) WWW= https://lean-lang.org/ \ https://github.com/leanprover/lean4 LICENSE= APACHE20 LICENSE_FILE= ${WRKSRC}/LICENSE BROKEN_armv7= compilation fails: ../../.build/stage1/lib/temp/Init/Coe.depend: No such file or directory BROKEN_i386= linking fails: INTERNAL PANIC: out of memory (during: Linking runLinter) BUILD_DEPENDS= bash:shells/bash \ cadical:math/cadical LIB_DEPENDS= libgmp.so:math/gmp \ libuv.so:devel/libuv RUN_DEPENDS= cadical:math/cadical USES= cmake:noninja,testing compiler:c++14-lang gmake pkgconfig python:build # ninja fails + gmake scripts are included in the project USE_GITHUB= yes GH_ACCOUNT= leanprover CFLAGS+= -fPIC CXXFLAGS+= -fPIC CMAKE_OFF= USE_MIMALLOC #MAKE_ARGS+= V=1 VERBOSE=1 #MAKE_JOBS_UNSAFE= yes MAKE_ENV= LD_LIBRARY_PATH=${BUILD_WRKSRC}/stage0/lib/lean BINARY_ALIAS= make=${GMAKE} python=${PYTHON_CMD} pre-everything:: @${ECHO_MSG} "" @${ECHO_MSG} "Please note that build Lean requires /proc to be mounted." @${ECHO_MSG} "" @${ECHO_MSG} " The usual way to do this is to add this line to /etc/fstab:" @${ECHO_MSG} " proc /proc procfs rw 0 0" @${ECHO_MSG} "" @${ECHO_MSG} " and then run this command as root:" @${ECHO_MSG} " # mount /proc" @${ECHO_MSG} "" post-install: # remove empty dirs @${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete # remove stray files @${RM} ${STAGEDIR}${PREFIX}/LICENSE* # remove bin/cadical, workaround for https://github.com/leanprover/lean4/issues/5603 @${RM} ${STAGEDIR}${PREFIX}/bin/cadical # strip binaries @cd ${STAGEDIR}${PREFIX} && ${STRIP_CMD} \ bin/lake \ bin/lean \ bin/leanc \ lib/lean/libInit_shared.so \ lib/lean/libleanshared.so tests as of 4.20.0: 99% tests passed, 16 tests failed out of 2594, see https://github.com/leanprover/lean4/issues/8628 .include