--- w/math/cvc4/Makefile +++ w/math/cvc4/Makefile @@ -1,10 +1,14 @@ # $FreeBSD$ PORTNAME= cvc4 -DISTVERSION= 1.6 -PORTREVISION= 4 +DISTVERSION= 1.7 CATEGORIES= math java -MASTER_SITES= https://cvc4.cs.stanford.edu/downloads/builds/src/ +MASTER_SITES+= http://www.antlr3.org/download/:antlr3 +DISTFILES+= antlr-3.4-complete.jar:antlr3 +EXTRACT_ONLY= ${DISTNAME}${EXTRACT_SUFX} + +PATCH_SITES= https://github.com/${GH_ACCOUNT}/${GH_PROJECT}/commit/ +PATCHFILES+= fc8907afc08d.patch:-p1 # Install Java bindings MAINTAINER= greg@unrelenting.technology COMMENT= Automatic theorem prover for SMT (Satisfiability Modulo Theories) @@ -14,63 +18,76 @@ LICENSE_FILE= ${WRKSRC}/COPYING LIB_DEPENDS= libantlr3c.so:devel/libantlr3c \ libboost_system.so:devel/boost-libs -BUILD_DEPENDS= bash:shells/bash \ - antlr3:devel/antlr3 -USES= autoreconf compiler:c++17-lang gmake libtool localbase \ +USES= cmake ncurses compiler:c++17-lang \ pkgconfig python:3.5+,build shebangfix + +USE_GITHUB= yes +GH_ACCOUNT= CVC4 +GH_PROJECT= CVC4 + USE_JAVA= yes JAVA_BUILD= yes -GNU_CONFIGURE= yes -CONFIGURE_ARGS+= --disable-dependency-tracking \ - --with-swig=${LOCALBASE}/bin/swig3.0 \ - ANTLR=${LOCALBASE}/bin/antlr3 -CONFIGURE_SHELL= ${LOCALBASE}/bin/bash USE_LDCONFIG= yes -SHEBANG_FILES= src/mk* src/theory/mk* src/base/mk* src/expr/mk* src/options/mk* test/regress/run_regression.py -OPTIONS_DEFINE= CRYPTOMINISAT JAVA READLINE DEBUG +CMAKE_BUILD_TYPE= Production +CMAKE_ARGS+= -DANTLR_BINARY=${WRKDIR}/antlr3 + +OPTIONS_DEFINE= CRYPTOMINISAT JAVA PYTHON READLINE OPTIONS_RADIO= NUMLIB OPTIONS_RADIO_NUMLIB= GMP CLN -OPTIONS_DEFAULT= CRYPTOMINISAT READLINE GMP +OPTIONS_DEFAULT= CRYPTOMINISAT JAVA PYTHON READLINE GMP OPTIONS_SUB= yes CRYPTOMINISAT_DESC= Use CryptoMiniSat as the SAT solver GMP_DESC= Use GMP numeric library CLN_DESC= Use CLN numeric library (disables portfolio mode) -CRYPTOMINISAT_CONFIGURE_ON= --with-cryptominisat --with-cryptominisat-dir=${LOCALBASE} +CRYPTOMINISAT_CMAKE_BOOL= USE_CRYPTOMINISAT CRYPTOMINISAT_LIB_DEPENDS= libcryptominisat5.so:math/cryptominisat -JAVA_CONFIGURE_ON= --enable-language-bindings=c,c++,java \ - JAVA_CPPFLAGS="-I${JAVA_HOME}/include -I${JAVA_HOME}/include/freebsd" \ - JAVAC=${JAVAC} JAVAH=${JAVAH} JAR=${JAR} -JAVA_CONFIGURE_OFF= --enable-language-bindings=c,c++ -JAVA_BUILD_DEPENDS= swig3.0:devel/swig30 +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= swig3.0:devel/swig30 -READLINE_CONFIGURE_WITH= readline -READLINE_USES= readline +PYTHON_CMAKE_BOOL= BUILD_BINDINGS_PYTHON USE_PYTHON3 +PYTHON_BUILD_DEPENDS= swig3.0:devel/swig30 -GMP_CONFIGURE_WITH= gmp -GMP_CONFIGURE_ON= --with-portfolio -GMP_LIB_DEPENDS= libgmp.so:math/gmp \ - libboost_thread.so:devel/boost-libs +READLINE_CMAKE_BOOL= USE_READLINE +READLINE_USES= readline:port + +GMP_CMAKE_BOOL= ENABLE_PORTFOLIO +GMP_CMAKE_ON= -DENABLE_DUMPING=OFF +GMP_LIB_DEPENDS= libgmp.so:math/gmp \ + libboost_thread.so:devel/boost-libs # note: CVC4 already depends on boost-libs, so portfolio mode is "free" in terms of pkg dependencies -CLN_CONFIGURE_WITH= cln -CLN_LIB_DEPENDS= libcln.so:math/cln \ - libgmp.so:math/gmp - -DEBUG_CONFIGURE_ON= --with-build=debug -DEBUG_CONFIGURE_OFF= --with-build=production -DEBUG_INSTALL_TARGET_OFF= install-strip +CLN_CMAKE_BOOL= USE_CLN +CLN_LIB_DEPENDS= libcln.so:math/cln \ + libgmp.so:math/gmp .include .if ${PORT_OPTIONS:MREADLINE} || ${PORT_OPTIONS:MCLN} LICENSE= GPLv3 -CONFIGURE_ARGS+= --enable-gpl +CMAKE_ARGS+= -DENABLE_GPL:BOOL=ON .endif +post-extract: + @${CP} ${DISTDIR}/antlr-3.4-complete.jar ${WRKDIR}/antlr3.jar + @${ECHO_CMD} "#!/bin/sh" > ${WRKDIR}/antlr3 + @${ECHO_CMD} "JAVA_VERSION=1.7+ exec \"${LOCALBASE}/bin/java\" -classpath \"${WRKDIR}/antlr3.jar\" org.antlr.Tool \"\$$@\"" >> ${WRKDIR}/antlr3 + @${CHMOD} +x ${WRKDIR}/antlr3 + +# make a relative symlink instead of absolute to build dir +post-install-JAVA-on: + @${LN} -sf CVC4-1.7.0.jar ${STAGEDIR}${PREFIX}/share/java/cvc4/CVC4.jar + +post-patch: + @${REINPLACE_CMD} -e 's|^#!/bin/bash|#!/bin/sh|g' \ + ${WRKSRC}/doc/*.sh ${WRKSRC}/src/base/mk* ${WRKSRC}/src/options/*.sh + .include --- w/math/cvc4/distinfo +++ w/math/cvc4/distinfo @@ -1,3 +1,7 @@ -TIMESTAMP = 1531429558 -SHA256 (cvc4-1.6.tar.gz) = 5c18bd5ea893fba9723a4d35c889d412ec6d29a21db9db69481891a8ff4887c7 -SIZE (cvc4-1.6.tar.gz) = 7815893 +TIMESTAMP = 1559856275 +SHA256 (antlr-3.4-complete.jar) = 9d3e866b610460664522520f73b81777b5626fb0a282a5952b9800b751550bf7 +SIZE (antlr-3.4-complete.jar) = 2388361 +SHA256 (CVC4-CVC4-1.7_GH0.tar.gz) = 9864a364a0076ef7ff63a46cdbc69cbe6568604149626338598d4df7788f8c2e +SIZE (CVC4-CVC4-1.7_GH0.tar.gz) = 6969953 +SHA256 (fc8907afc08d.patch) = b14fe811a91152d9311a48e1c198c82fc55febf0c76c6c8fab6c9d6f0addeb3f +SIZE (fc8907afc08d.patch) = 1154 --- /dev/null +++ w/math/cvc4/files/patch-cmake_FindANTLR.cmake @@ -0,0 +1,13 @@ +We fetch 3.4 (since 3.5 breaks it), we don't want it to find +system antlr3 (3.5) and overwrite our fetched one + +--- cmake/FindANTLR.cmake.orig 2019-04-09 16:14:31 UTC ++++ cmake/FindANTLR.cmake +@@ -27,7 +27,6 @@ find_library(ANTLR_LIBRARIES + NO_DEFAULT_PATH) + + if(CHECK_SYSTEM_VERSION) +- find_program(ANTLR_BINARY NAMES antlr3) + find_path(ANTLR_INCLUDE_DIR NAMES antlr3.h) + find_library(ANTLR_LIBRARIES NAMES antlr3c) + endif() --- /dev/null +++ w/math/cvc4/files/patch-cmake_FindReadline.cmake @@ -0,0 +1,42 @@ +CMAKE_REQUIRED_INCLUDES does not work for some reason, +the check is compiled without the include path + +--- cmake/FindReadline.cmake.orig 2019-04-09 16:14:31 UTC ++++ cmake/FindReadline.cmake +@@ -13,15 +13,7 @@ find_library(Readline_LIBRARIES NAMES readline) + function(try_compile_readline libs _result) + set(CMAKE_REQUIRED_QUIET TRUE) + set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES} ${libs}) +- check_cxx_source_compiles( +- " +- #include +- #include +- int main() { readline(\"\"); return 0; } +- " +- ${_result} +- ) +- set(${_result} ${${_result}} PARENT_SCOPE) ++ set(${_result} OK PARENT_SCOPE) + endfunction() + + if(Readline_INCLUDE_DIR) +@@ -42,18 +34,7 @@ if(Readline_INCLUDE_DIR) + + # Check which standard of readline is installed on the system. + # https://github.com/CVC4/CVC4/issues/702 +- include(CheckCXXSourceCompiles) +- set(CMAKE_REQUIRED_QUIET TRUE) +- set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES}) +- check_cxx_source_compiles( +- "#include +- #include +- char* foo(const char*, int) { return (char*)0; } +- int main() { rl_completion_entry_function = foo; return 0; }" +- Readline_COMPENTRY_FUNC_RETURNS_CHARPTR +- ) +- unset(CMAKE_REQUIRED_QUIET) +- unset(CMAKE_REQUIRED_LIBRARIES) ++ set(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR TRUE) + endif() + + include(FindPackageHandleStandardArgs) --- c/math/cvc4/files/patch-config_cryptominisat.m4 +++ /dev/null @@ -1,31 +0,0 @@ ---- config/cryptominisat.m4.orig 2018-07-12 21:34:02 UTC -+++ config/cryptominisat.m4 -@@ -36,7 +36,7 @@ elif test -n "$with_cryptominisat"; then - AC_MSG_RESULT([no]) - fi - -- if ! test -d "$CRYPTOMINISAT_HOME" || ! test -x "$CRYPTOMINISAT_HOME/install/bin/cryptominisat5_simple" ; then -+ if ! test -d "$CRYPTOMINISAT_HOME" || ! test -x "$CRYPTOMINISAT_HOME/bin/cryptominisat5_simple" ; then - AC_MSG_FAILURE([either $CRYPTOMINISAT_HOME is not an cryptominisat install tree or it's not yet built]) - fi - -@@ -54,7 +54,7 @@ elif test -n "$with_cryptominisat"; then - have_libcryptominisat=1 - fi - -- CRYPTOMINISAT_LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib" -+ CRYPTOMINISAT_LDFLAGS="-L$CRYPTOMINISAT_HOME/lib" - - else - AC_MSG_RESULT([no, user didn't request cryptominisat]) -@@ -74,8 +74,8 @@ if test -z "$CRYPTOMINISAT_LIBS"; then - cvc4_save_LDFLAGS="$LDFLAGS" - cvc4_save_CPPFLAGS="$CPPFLAGS" - -- LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib" -- CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/install/include" -+ LDFLAGS="-L$CRYPTOMINISAT_HOME/lib" -+ CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/include" - LIBS="-lcryptominisat5 $1" - - AC_LINK_IFELSE( --- c/math/cvc4/files/patch-configure.ac +++ /dev/null @@ -1,11 +0,0 @@ ---- configure.ac.orig 2018-07-12 21:33:27 UTC -+++ configure.ac -@@ -913,7 +913,7 @@ AC_ARG_WITH([cryptominisat], - CVC4_CHECK_FOR_CRYPTOMINISAT - if test $have_libcryptominisat -eq 1; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CRYPTOMINISAT" -- CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/install/include" -+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/include" - fi - AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1]) - AC_SUBST([CRYPTOMINISAT_LDFLAGS]) --- /dev/null +++ w/math/cvc4/files/patch-doc_CMakeLists.txt @@ -0,0 +1,22 @@ +--- doc/CMakeLists.txt.orig 2019-06-06 21:29:05 UTC ++++ doc/CMakeLists.txt +@@ -34,10 +34,10 @@ configure_file( + #-----------------------------------------------------------------------------# + # Install man pages + +-install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION share/man/man1) +-install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5 DESTINATION share/man/man5) ++install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION man/man1) ++install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5 DESTINATION man/man5) + if(ENABLE_PORTFOLIO) +- install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION share/man/man1 ++ install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION man/man1 + RENAME pcvc4.1) + endif() + install(FILES +@@ -45,4 +45,4 @@ install(FILES + ${CMAKE_CURRENT_BINARY_DIR}/libcvc4parser.3 + ${CMAKE_CURRENT_BINARY_DIR}/options.3cvc + ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.3cvc +- DESTINATION share/man/man3) ++ DESTINATION man/man3) --- /dev/null +++ w/math/cvc4/files/patch-examples_CMakeLists.txt @@ -0,0 +1,12 @@ +--- examples/CMakeLists.txt.orig 2019-06-06 19:10:39 UTC ++++ examples/CMakeLists.txt +@@ -17,9 +17,6 @@ add_custom_target(examples) + + # Create target runexamples. + # Builds and runs all examples. +-add_custom_target(runexamples +- COMMAND ctest --output-on-failure -L "example" -j${NTHREADS} $(ARGS) +- DEPENDS examples) + + # Add example target and create test to run example with ctest. + # --- w/math/cvc4/files/patch-src_base_configuration.cpp +++ w/math/cvc4/files/patch-src_base_configuration.cpp @@ -1,6 +1,6 @@ ---- src/base/configuration.cpp.orig 2018-06-25 21:13:17 UTC +--- src/base/configuration.cpp.orig 2019-04-09 16:14:31 UTC +++ src/base/configuration.cpp -@@ -405,7 +405,7 @@ std::string Configuration::getCompiler() { +@@ -376,7 +376,7 @@ std::string Configuration::getCompiler() { } std::string Configuration::getCompiledDateTime() { --- /dev/null +++ w/math/cvc4/files/patch-test_CMakeLists.txt @@ -0,0 +1,14 @@ +--- test/CMakeLists.txt.orig 2019-06-06 19:12:46 UTC ++++ test/CMakeLists.txt +@@ -15,11 +15,6 @@ add_dependencies(build-tests examples) + # first run the command of the regress target (i.e., run all regression tests) + # and afterwards run the command specified for the check target. + # Dependencies of check are added in the corresponding subdirectories. +-add_custom_target(check +- COMMAND +- ctest --output-on-failure -LE "regress[3-4]" -j${CTEST_NTHREADS} $(ARGS) +- DEPENDS +- build-tests) + + #-----------------------------------------------------------------------------# + # Add subdirectories --- /dev/null +++ w/math/cvc4/files/patch-test_regress_CMakeLists.txt @@ -0,0 +1,14 @@ +--- test/regress/CMakeLists.txt.orig 2019-06-06 19:13:41 UTC ++++ test/regress/CMakeLists.txt +@@ -2138,11 +2138,6 @@ set(run_regress_script ${CMAKE_CURRENT_LIST_DIR}/run_r + add_custom_target(build-regress DEPENDS cvc4-bin) + add_dependencies(build-tests build-regress) + +-add_custom_target(regress +- COMMAND +- ctest --output-on-failure -L "regress[0-2]" -j${CTEST_NTHREADS} $(ARGS) +- DEPENDS build-regress) +- + macro(cvc4_add_regression_test level file) + add_test(${file} + ${run_regress_script} --- /dev/null +++ w/math/cvc4/files/patch-test_system_CMakeLists.txt @@ -0,0 +1,13 @@ +--- test/system/CMakeLists.txt.orig 2019-06-06 19:13:50 UTC ++++ test/system/CMakeLists.txt +@@ -10,10 +10,6 @@ include_directories(${CMAKE_BINARY_DIR}/src) + add_custom_target(build-systemtests) + add_dependencies(build-tests build-systemtests) + +-add_custom_target(systemtests +- COMMAND ctest --output-on-failure -L "system" -j${CTEST_NTHREADS} $(ARGS) +- DEPENDS build-systemtests) +- + set(CVC4_SYSTEM_TEST_FLAGS + -D__BUILDING_CVC4_SYSTEM_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS) + --- w/math/cvc4/pkg-plist +++ w/math/cvc4/pkg-plist @@ -1,23 +1,17 @@ bin/cvc4 %%GMP%%bin/pcvc4 +include/cvc4/api/cvc4cpp.h +include/cvc4/api/cvc4cppkind.h include/cvc4/base/configuration.h include/cvc4/base/exception.h include/cvc4/base/listener.h include/cvc4/base/modal_exception.h -include/cvc4/base/tls.h -include/cvc4/bindings/compat/c/c_interface.h -include/cvc4/bindings/compat/c/c_interface_defs.h -include/cvc4/compat/cvc3_compat.h include/cvc4/context/cdhashmap_forward.h include/cvc4/context/cdhashset_forward.h include/cvc4/context/cdinsert_hashmap_forward.h include/cvc4/context/cdlist_forward.h -include/cvc4/context/cdtrail_hashmap_forward.h include/cvc4/cvc4.h -include/cvc4/cvc4_private.h -include/cvc4/cvc4_private_library.h include/cvc4/cvc4_public.h -include/cvc4/cvc4parser_private.h include/cvc4/cvc4parser_public.h include/cvc4/expr/array.h include/cvc4/expr/array_store_all.h @@ -28,11 +22,8 @@ include/cvc4/expr/emptyset.h include/cvc4/expr/expr.h include/cvc4/expr/expr_iomanip.h include/cvc4/expr/expr_manager.h -include/cvc4/expr/expr_manager_template.h include/cvc4/expr/expr_stream.h -include/cvc4/expr/expr_template.h include/cvc4/expr/kind.h -include/cvc4/expr/kind_template.h include/cvc4/expr/pickler.h include/cvc4/expr/record.h include/cvc4/expr/symbol_table.h @@ -50,7 +41,7 @@ include/cvc4/options/options.h include/cvc4/options/printer_modes.h include/cvc4/options/quantifiers_modes.h include/cvc4/options/set_language.h -include/cvc4/options/simplification_mode.h +include/cvc4/options/smt_modes.h include/cvc4/options/sygus_out_mode.h include/cvc4/options/theoryof_mode.h include/cvc4/parser/input.h @@ -66,7 +57,6 @@ include/cvc4/smt_util/lemma_channels.h include/cvc4/smt_util/lemma_input_channel.h include/cvc4/smt_util/lemma_output_channel.h include/cvc4/theory/logic_info.h -include/cvc4/theory/theory_test_utils.h include/cvc4/util/abstract_value.h include/cvc4/util/bitvector.h include/cvc4/util/bool.h @@ -91,32 +81,16 @@ include/cvc4/util/sexpr.h include/cvc4/util/statistics.h include/cvc4/util/tuple.h include/cvc4/util/unsafe_interrupt_exception.h -%%JAVA%%lib/jni/libcvc4compatjni.so -%%JAVA%%lib/jni/libcvc4compatjni.so.5 -%%JAVA%%lib/jni/libcvc4compatjni.so.5.0.0 -%%JAVA%%lib/jni/libcvc4jni.so -%%JAVA%%lib/jni/libcvc4jni.so.5 -%%JAVA%%lib/jni/libcvc4jni.so.5.0.0 lib/libcvc4.so -lib/libcvc4.so.5 -lib/libcvc4.so.5.0.0 -lib/libcvc4bindings_c_compat.so -lib/libcvc4bindings_c_compat.so.5 -lib/libcvc4bindings_c_compat.so.5.0.0 -lib/libcvc4compat.so -lib/libcvc4compat.so.5 -lib/libcvc4compat.so.5.0.0 +lib/libcvc4.so.6 +%%JAVA%%lib/libcvc4jni.so lib/libcvc4parser.so -lib/libcvc4parser.so.5 -lib/libcvc4parser.so.5.0.0 -man/man1/cvc4.1.gz -%%GMP%%man/man1/pcvc4.1.gz -man/man3/SmtEngine.3cvc.gz -man/man3/libcvc4.3.gz -man/man3/libcvc4compat.3.gz -man/man3/libcvc4parser.3.gz -man/man3/options.3cvc.gz -man/man5/cvc4.5.gz +lib/libcvc4parser.so.6 +%%PYTHON%%%%PYTHON_SITELIBDIR%%/CVC4.py +%%PYTHON%%%%PYTHON_SITELIBDIR%%/_CVC4.so +%%DATADIR%%/drat.plf +%%DATADIR%%/er.plf +%%DATADIR%%/lrat.plf %%DATADIR%%/sat.plf %%DATADIR%%/smt.plf %%DATADIR%%/th_arrays.plf @@ -126,5 +100,12 @@ man/man5/cvc4.5.gz %%DATADIR%%/th_bv_rewrites.plf %%DATADIR%%/th_int.plf %%DATADIR%%/th_real.plf -%%JAVA%%share/java/CVC4.jar -%%JAVA%%share/java/CVC4compat.jar +%%JAVA%%%%JAVASHAREDIR%%/cvc4/CVC4-1.7.0.jar +%%JAVA%%%%JAVASHAREDIR%%/cvc4/CVC4.jar +man/man1/cvc4.1.gz +%%GMP%%man/man1/pcvc4.1.gz +man/man3/SmtEngine.3cvc.gz +man/man3/libcvc4.3.gz +man/man3/libcvc4parser.3.gz +man/man3/options.3cvc.gz +man/man5/cvc4.5.gz