57 lines
1.5 KiB
Makefile
57 lines
1.5 KiB
Makefile
PORTNAME= z3-solver
|
|
DISTVERSION= 5.1.0.0
|
|
CATEGORIES= math
|
|
PKGNAMEPREFIX= ${PYTHON_PKGNAMEPREFIX}
|
|
|
|
MAINTAINER= yuri@FreeBSD.org
|
|
COMMENT= Python binding for Z3 Theorem Prover
|
|
WWW= https://github.com/Z3Prover/z3
|
|
|
|
LICENSE= MIT
|
|
LICENSE_FILE= ${WRKSRC}/../../../LICENSE.txt
|
|
|
|
LIB_DEPENDS= libz3.so:math/z3
|
|
|
|
USES= cmake python
|
|
USE_PYTHON= flavors autoplist
|
|
|
|
USE_GITHUB= yes
|
|
GH_ACCOUNT= Z3Prover
|
|
GH_PROJECT= z3
|
|
GH_TAGNAME= z3-5.1.0
|
|
|
|
WRKSRC_SUBDIR= src/api/python
|
|
WRKSRC_top= ${WRKSRC}/../../..
|
|
|
|
CMAKE_ARGS= -DCMAKE_POLICY_VERSION_MINIMUM=3.5 # CMake 4.5 compatibility, see https://github.com/Z3Prover/z3/issues/10984
|
|
|
|
TEST_ENV= ${MAKE_ENV} PYTHONPATH=${STAGEDIR}${PYTHONPREFIX_SITELIBDIR}
|
|
|
|
NO_ARCH= yes
|
|
|
|
PLIST_FILES= ${PYTHON_SITELIBDIR:S,^${PREFIX}/,,}/z3/z3regex.py
|
|
|
|
post-patch:
|
|
@${RLN} ${WRKSRC_top}/scripts ${WRKSRC}/scripts
|
|
@${RLN} ${WRKSRC_top}/src/api ${WRKSRC}/api
|
|
|
|
do-test:
|
|
.for t in z3 z3num
|
|
@cd ${WRKSRC_top} && \
|
|
${CP} ${WRKSRC}/z3test.py . && \
|
|
${ECHO} "==> running the test ${t}" && \
|
|
${SETENV} ${TEST_ENV} ${PYTHON_CMD} z3test.py ${t} && \
|
|
${ECHO} "... test ${t} succeeded"
|
|
.endfor
|
|
.for e in kinematics power-of-two dog-cat-mouse sudoku eight-queens
|
|
@cd ${WRKSRC}/../../.. && \
|
|
${ECHO} "==> running the example ${e}" && \
|
|
${SETENV} ${TEST_ENV} ${PYTHON_CMD} ${FILESDIR}/example-${e}.py && \
|
|
${ECHO} "... example ${e} succeeded"
|
|
@${ECHO} "All tests succeeded."
|
|
.endfor
|
|
|
|
# tests as of 5.0.0.0: z3/z3num unit tests + kinematics, power-of-two, dog-cat-mouse, sudoku, eight-queens examples all passed.
|
|
|
|
.include <bsd.port.mk>
|