From nobody Wed Jan 04 11:50:57 2023 X-Original-To: dev-commits-ports-all@mlmmj.nyi.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4Nn7GV00Znz2p17K; Wed, 4 Jan 2023 11:50:58 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from mxrelay.nyi.freebsd.org (mxrelay.nyi.freebsd.org [IPv6:2610:1c1:1:606c::19:3]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256 client-signature RSA-PSS (4096 bits) client-digest SHA256) (Client CN "mxrelay.nyi.freebsd.org", Issuer "R3" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 4Nn7GT6xyQz3Q5W; Wed, 4 Jan 2023 11:50:57 +0000 (UTC) (envelope-from git@FreeBSD.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1672833057; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=cahlTGMxhxqvPmcbR3SVrtZljW12a6legBOWZQoeUbQ=; b=Hp1mR2BOyQKB6Ct49CeXKcjXsQu5EKlPG84B18UIOnquCsRlhiRx/qarqTGvYcOWbrHD8U p299JaLE2jEMZjVIXp97ziWBd1ApSASJIUs7e5pK5bJ4VNdnw76D96QBCEuZfcydkz+RAa AwcJVwTyCZCCH5oOVMnFJ6vb+jkmBfcdQkmUZUKN8AyD/8ddTjI2ZGVEBAFy9w/ZRl6WvD QYoTlVsFvJ98BdOVfRYq1w6wGWc65tI5jZRTy8ZprjlKZrKLS0u81Jr5DbnjK38wVJ7Bon Yjhl6HXqby0J4tIhdxExL3Mcoh+f12JLzUAjdk9gjVcY2dtJ8wFDXpi4+Vx4gw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1672833057; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=cahlTGMxhxqvPmcbR3SVrtZljW12a6legBOWZQoeUbQ=; b=MdQPxhvg74UEEz58/kW0ce2e89rZeIhpChTgI5ZcZs6XSaULwp+Rnkwv74fzyribsYYB+X c7RMwYjEvIU5YUYPVTvwZt2Di+GYzIOteo+VyEtCRzADvITOcPGmzrG7pVVn6XadFp9X/L WP8Zu98mm2QK0NNxK+CqUNWIeUx8XRo0OAoZa6xNATVaUimif137EufiN6I/3y00WJHH+T MVsBQPk0WYqNlDVj7iHURBl9o/FyGH5wF7CT3oqVl1VwE7g7xnKgJd5/zWO9v+SitzWtJr 8BraTJ6+X2zlroaPBuZHeLmM7S2eqSrd8x9ki6CBw1RDB2MN5ondNKOrAjjbDQ== ARC-Authentication-Results: i=1; mx1.freebsd.org; none ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1672833057; a=rsa-sha256; cv=none; b=EotoZZM3BSv6hnb4DzvkddqFJh6C3kMRXUSyi2oE2ikfQX5Y9CA8KeDsoTTMRGHxvR+Hvy btN/jDwDnYEog8JtGRuEOQ5ONunipmYkQfUdBzKJ2BAxLPcmxgLV25kUVrrOz0U7auRM6X M80a9ZCjcjaDzLQJXPFGvW9elP/Od/l+BJtIfr5CG3VBvl8aj2kiUZXBynM2mlqSt7qNI+ V28JgZtP6y53SBjVUSU2NfGa3xBhUiI5EfmSRVBstd4J7XAgfw16OwNibl7LUsiIiza3ii 8s9sFJl85qbDwUEqO8NWmXIAoJ7MrsxEcVSoocBxYvY/EnITJsx9o4WMRO3BVA== Received: from gitrepo.freebsd.org (gitrepo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:5]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (Client did not present a certificate) by mxrelay.nyi.freebsd.org (Postfix) with ESMTPS id 4Nn7GT60JXz18wr; Wed, 4 Jan 2023 11:50:57 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from gitrepo.freebsd.org ([127.0.1.44]) by gitrepo.freebsd.org (8.16.1/8.16.1) with ESMTP id 304Bovit055141; Wed, 4 Jan 2023 11:50:57 GMT (envelope-from git@gitrepo.freebsd.org) Received: (from git@localhost) by gitrepo.freebsd.org (8.16.1/8.16.1/Submit) id 304Bovic055140; Wed, 4 Jan 2023 11:50:57 GMT (envelope-from git) Date: Wed, 4 Jan 2023 11:50:57 GMT Message-Id: <202301041150.304Bovic055140@gitrepo.freebsd.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org From: Yuri Victorovich Subject: git: faf8043d8972 - main - math/cvc4: Move to math/cvc5 - CVC4 was succeeded by CVC5 List-Id: Commit messages for all branches of the ports repository List-Archive: https://lists.freebsd.org/archives/dev-commits-ports-all List-Help: List-Post: List-Subscribe: List-Unsubscribe: Sender: owner-dev-commits-ports-all@freebsd.org X-BeenThere: dev-commits-ports-all@freebsd.org MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Git-Committer: yuri X-Git-Repository: ports X-Git-Refname: refs/heads/main X-Git-Reftype: branch X-Git-Commit: faf8043d8972b9be04156c476417ed611a280821 Auto-Submitted: auto-generated X-ThisMailContainsUnwantedMimeParts: N The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=faf8043d8972b9be04156c476417ed611a280821 commit faf8043d8972b9be04156c476417ed611a280821 Author: Yuri Victorovich AuthorDate: 2023-01-04 11:27:14 +0000 Commit: Yuri Victorovich CommitDate: 2023-01-04 11:50:53 +0000 math/cvc4: Move to math/cvc5 - CVC4 was succeeded by CVC5 Remove the PYTHON option - it will be made into a separate port. --- MOVED | 1 + math/Makefile | 2 +- math/cvc4/distinfo | 7 -- math/cvc4/files/patch-cmake_FindANTLR.cmake | 13 --- math/cvc4/files/patch-cmake_FindReadline.cmake | 42 -------- math/cvc4/files/patch-doc_CMakeLists.txt | 22 ----- math/cvc4/files/patch-examples_CMakeLists.txt | 12 --- math/cvc4/files/patch-src_CMakeLists.txt | 11 --- math/cvc4/files/patch-src_base_configuration.cpp | 11 --- math/cvc4/files/patch-src_main_portfolio.cpp | 24 ----- math/cvc4/files/patch-swig4 | 40 -------- math/cvc4/files/patch-test_CMakeLists.txt | 14 --- math/cvc4/files/patch-test_regress_CMakeLists.txt | 14 --- math/cvc4/files/patch-test_system_CMakeLists.txt | 13 --- math/cvc4/pkg-plist | 111 ---------------------- math/{cvc4 => cvc5}/Makefile | 69 ++++++-------- math/cvc5/distinfo | 7 ++ math/cvc5/files/patch-cmake_FindANTLR3.cmake | 11 +++ math/cvc5/files/patch-cmake_FindEditline.cmake | 11 +++ math/{cvc4 => cvc5}/pkg-descr | 0 math/cvc5/pkg-plist | 16 ++++ 21 files changed, 74 insertions(+), 377 deletions(-) diff --git a/MOVED b/MOVED index c6ff383b5959..95671d3e34fd 100644 --- a/MOVED +++ b/MOVED @@ -17747,3 +17747,4 @@ sysutils/beats6||2023-01-01|Has expired: No longer maintained and supported sysutils/logstash6||2023-01-01|Has expired: No longer maintained and supported textproc/elasticsearch6||2023-01-01|Has expired: No longer maintained and supported japanese/ja-tex-xdvik|print/tex-xdvik|2023-01-02|pTeX support has been integrated +math/cvc4|math/cvc5|2023-01-03|CVC4 was succeeded by CVC5 diff --git a/math/Makefile b/math/Makefile index c5b0cf9072d9..cbe924b35d07 100644 --- a/math/Makefile +++ b/math/Makefile @@ -264,7 +264,7 @@ SUBDIR += cudd SUBDIR += curv SUBDIR += cvc3 - SUBDIR += cvc4 + SUBDIR += cvc5 SUBDIR += dbcsr SUBDIR += deal.ii SUBDIR += dieharder diff --git a/math/cvc4/distinfo b/math/cvc4/distinfo deleted file mode 100644 index a16df890b9e7..000000000000 --- a/math/cvc4/distinfo +++ /dev/null @@ -1,7 +0,0 @@ -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 diff --git a/math/cvc4/files/patch-cmake_FindANTLR.cmake b/math/cvc4/files/patch-cmake_FindANTLR.cmake deleted file mode 100644 index ae6462f57e37..000000000000 --- a/math/cvc4/files/patch-cmake_FindANTLR.cmake +++ /dev/null @@ -1,13 +0,0 @@ -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() diff --git a/math/cvc4/files/patch-cmake_FindReadline.cmake b/math/cvc4/files/patch-cmake_FindReadline.cmake deleted file mode 100644 index 50c691763f06..000000000000 --- a/math/cvc4/files/patch-cmake_FindReadline.cmake +++ /dev/null @@ -1,42 +0,0 @@ -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) diff --git a/math/cvc4/files/patch-doc_CMakeLists.txt b/math/cvc4/files/patch-doc_CMakeLists.txt deleted file mode 100644 index 764bb44e1d12..000000000000 --- a/math/cvc4/files/patch-doc_CMakeLists.txt +++ /dev/null @@ -1,22 +0,0 @@ ---- 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) diff --git a/math/cvc4/files/patch-examples_CMakeLists.txt b/math/cvc4/files/patch-examples_CMakeLists.txt deleted file mode 100644 index 60ccd1f7adbf..000000000000 --- a/math/cvc4/files/patch-examples_CMakeLists.txt +++ /dev/null @@ -1,12 +0,0 @@ ---- 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. - # diff --git a/math/cvc4/files/patch-src_CMakeLists.txt b/math/cvc4/files/patch-src_CMakeLists.txt deleted file mode 100644 index a516e618fe82..000000000000 --- a/math/cvc4/files/patch-src_CMakeLists.txt +++ /dev/null @@ -1,11 +0,0 @@ ---- src/CMakeLists.txt.orig 2019-07-28 18:28:58 UTC -+++ src/CMakeLists.txt -@@ -913,6 +913,6 @@ install(FILES - - # Fix include paths for all public headers. - # Note: This is a temporary fix until the new C++ API is in place. --install(CODE "execute_process(COMMAND -+install(CODE "execute_process(COMMAND sh - ${CMAKE_CURRENT_LIST_DIR}/fix-install-headers.sh -- ${CMAKE_INSTALL_PREFIX})") -+ \"\$ENV{DESTDIR}\${CMAKE_INSTALL_PREFIX}\")") diff --git a/math/cvc4/files/patch-src_base_configuration.cpp b/math/cvc4/files/patch-src_base_configuration.cpp deleted file mode 100644 index 43541f78a272..000000000000 --- a/math/cvc4/files/patch-src_base_configuration.cpp +++ /dev/null @@ -1,11 +0,0 @@ ---- src/base/configuration.cpp.orig 2019-04-09 16:14:31 UTC -+++ src/base/configuration.cpp -@@ -376,7 +376,7 @@ std::string Configuration::getCompiler() { - } - - std::string Configuration::getCompiledDateTime() { -- return __DATE__ " " __TIME__; -+ return "(timestamp removed for reproducible builds)"; - } - - }/* CVC4 namespace */ diff --git a/math/cvc4/files/patch-src_main_portfolio.cpp b/math/cvc4/files/patch-src_main_portfolio.cpp deleted file mode 100644 index 454c9693112c..000000000000 --- a/math/cvc4/files/patch-src_main_portfolio.cpp +++ /dev/null @@ -1,24 +0,0 @@ ---- src/main/portfolio.cpp.orig 2018-04-22 17:42:48 UTC -+++ src/main/portfolio.cpp -@@ -18,6 +18,9 @@ - #include - #include - #include -+#ifdef __FreeBSD__ -+#include -+#endif - - #include "base/output.h" - #include "options/options.h" -@@ -100,7 +103,11 @@ std::pair runPortfolio(int numThreads, - void *stackaddr; - size_t stacksize; - pthread_attr_t attr; -+#ifdef __linux__ - pthread_getattr_np(threads[t].native_handle(), &attr); -+#elif __FreeBSD__ -+ pthread_attr_get_np(threads[t].native_handle(), &attr); -+#endif - pthread_attr_getstack(&attr, &stackaddr, &stacksize); - Chat() << "Created worker thread " << t << " with stack size " << stacksize << std::endl; - } diff --git a/math/cvc4/files/patch-swig4 b/math/cvc4/files/patch-swig4 deleted file mode 100644 index ca9a8faea594..000000000000 --- a/math/cvc4/files/patch-swig4 +++ /dev/null @@ -1,40 +0,0 @@ -Obtained from: https://github.com/CVC4/CVC4/commit/c587235d29d2e3e1cd52a9f76dde8f58c89ae37e - ---- src/bindings/java/CMakeLists.txt.orig 2019-04-09 16:14:31 UTC -+++ src/bindings/java/CMakeLists.txt -@@ -131,6 +131,7 @@ set(gen_java_files - ${CMAKE_CURRENT_BINARY_DIR}/LastExceptionBuffer.java - ${CMAKE_CURRENT_BINARY_DIR}/LogicException.java - ${CMAKE_CURRENT_BINARY_DIR}/LogicInfo.java -+ ${CMAKE_CURRENT_BINARY_DIR}/Map_ExprExpr.java - ${CMAKE_CURRENT_BINARY_DIR}/ModalException.java - ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java - ${CMAKE_CURRENT_BINARY_DIR}/Options.java -@@ -177,7 +178,6 @@ set(gen_java_files - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpq_class.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpz_class.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__istream.java -- ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__mapT_CVC4__Expr_CVC4__Expr_t.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__ostream.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__shared_ptrT_CVC4__SygusPrintCallback_t.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__string.java -@@ -210,6 +210,7 @@ set(gen_java_files - ${CMAKE_CURRENT_BINARY_DIR}/SygusPrintCallback.java - ${CMAKE_CURRENT_BINARY_DIR}/SymbolTable.java - ${CMAKE_CURRENT_BINARY_DIR}/SymbolType.java -+ ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java - ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java - ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java - ${CMAKE_CURRENT_BINARY_DIR}/Timer.java ---- src/smt/smt_engine.i.orig 2019-04-09 16:14:31 UTC -+++ src/smt/smt_engine.i -@@ -42,6 +42,9 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEng - swigCPtr = 0; - } - } -+ -+%template(Map_ExprExpr) std::map; -+ - #endif // SWIGJAVA - - %ignore CVC4::SmtEngine::setLogic(const char*); diff --git a/math/cvc4/files/patch-test_CMakeLists.txt b/math/cvc4/files/patch-test_CMakeLists.txt deleted file mode 100644 index 43d5da2a3df0..000000000000 --- a/math/cvc4/files/patch-test_CMakeLists.txt +++ /dev/null @@ -1,14 +0,0 @@ ---- 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 diff --git a/math/cvc4/files/patch-test_regress_CMakeLists.txt b/math/cvc4/files/patch-test_regress_CMakeLists.txt deleted file mode 100644 index a52d05061534..000000000000 --- a/math/cvc4/files/patch-test_regress_CMakeLists.txt +++ /dev/null @@ -1,14 +0,0 @@ ---- 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} diff --git a/math/cvc4/files/patch-test_system_CMakeLists.txt b/math/cvc4/files/patch-test_system_CMakeLists.txt deleted file mode 100644 index d05dbdc083df..000000000000 --- a/math/cvc4/files/patch-test_system_CMakeLists.txt +++ /dev/null @@ -1,13 +0,0 @@ ---- 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) - diff --git a/math/cvc4/pkg-plist b/math/cvc4/pkg-plist deleted file mode 100644 index 9a057af977ee..000000000000 --- a/math/cvc4/pkg-plist +++ /dev/null @@ -1,111 +0,0 @@ -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/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/cvc4.h -include/cvc4/cvc4_public.h -include/cvc4/cvc4parser_public.h -include/cvc4/expr/array.h -include/cvc4/expr/array_store_all.h -include/cvc4/expr/ascription_type.h -include/cvc4/expr/chain.h -include/cvc4/expr/datatype.h -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_stream.h -include/cvc4/expr/kind.h -include/cvc4/expr/pickler.h -include/cvc4/expr/record.h -include/cvc4/expr/symbol_table.h -include/cvc4/expr/type.h -include/cvc4/expr/uninterpreted_constant.h -include/cvc4/expr/variable_type_map.h -include/cvc4/options/argument_extender.h -include/cvc4/options/arith_heuristic_pivot_rule.h -include/cvc4/options/arith_propagation_mode.h -include/cvc4/options/arith_unate_lemma_mode.h -include/cvc4/options/datatypes_modes.h -include/cvc4/options/language.h -include/cvc4/options/option_exception.h -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/smt_modes.h -include/cvc4/options/sygus_out_mode.h -include/cvc4/options/theoryof_mode.h -include/cvc4/parser/input.h -include/cvc4/parser/parser.h -include/cvc4/parser/parser_builder.h -include/cvc4/parser/parser_exception.h -include/cvc4/printer/sygus_print_callback.h -include/cvc4/proof/unsat_core.h -include/cvc4/smt/command.h -include/cvc4/smt/logic_exception.h -include/cvc4/smt/smt_engine.h -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/util/abstract_value.h -include/cvc4/util/bitvector.h -include/cvc4/util/bool.h -include/cvc4/util/cardinality.h -include/cvc4/util/channel.h -include/cvc4/util/divisible.h -include/cvc4/util/floatingpoint.h -include/cvc4/util/gmp_util.h -include/cvc4/util/hash.h -include/cvc4/util/integer.h -include/cvc4/util/integer_cln_imp.h -include/cvc4/util/integer_gmp_imp.h -include/cvc4/util/maybe.h -include/cvc4/util/proof.h -include/cvc4/util/rational.h -include/cvc4/util/rational_cln_imp.h -include/cvc4/util/rational_gmp_imp.h -include/cvc4/util/regexp.h -include/cvc4/util/resource_manager.h -include/cvc4/util/result.h -include/cvc4/util/sexpr.h -include/cvc4/util/statistics.h -include/cvc4/util/tuple.h -include/cvc4/util/unsafe_interrupt_exception.h -lib/libcvc4.so -lib/libcvc4.so.6 -%%JAVA%%lib/libcvc4jni.so -lib/libcvc4parser.so -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 -%%DATADIR%%/th_base.plf -%%DATADIR%%/th_bv.plf -%%DATADIR%%/th_bv_bitblast.plf -%%DATADIR%%/th_bv_rewrites.plf -%%DATADIR%%/th_int.plf -%%DATADIR%%/th_real.plf -%%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 diff --git a/math/cvc4/Makefile b/math/cvc5/Makefile similarity index 51% rename from math/cvc4/Makefile rename to math/cvc5/Makefile index cf288551b284..8820265fccca 100644 --- a/math/cvc4/Makefile +++ b/math/cvc5/Makefile @@ -1,54 +1,46 @@ -PORTNAME= cvc4 -DISTVERSION= 1.7 -PORTREVISION= 6 +PORTNAME= cvc5 +DISTVERSIONPREFIX= cvc5- +DISTVERSION= 1.0.3 CATEGORIES= math java 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= ports@FreeBSD.org +MAINTAINER= yuri@FreeBSD.org COMMENT= Automatic theorem prover for SMT (Satisfiability Modulo Theories) -WWW= https://cvc4.cs.stanford.edu/web/ +WWW= https://cvc5.github.io/ LICENSE= BSD3CLAUSE LICENSE_FILE= ${WRKSRC}/COPYING -BROKEN= Doesn't build, src/expr/expr_template.h:0: error: undefined replacement ${getConst_instantiations} - -BUILD_DEPENDS= bash:shells/bash +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} LIB_DEPENDS= libantlr3c.so:devel/libantlr3c \ libboost_system.so:devel/boost-libs USES= cmake ncurses compiler:c++17-lang \ - pkgconfig python:3.5+,build shebangfix - -SHEBANG_FILES= src/base/mktagheaders \ - src/base/mktags - + localbase:ldflags pkgconfig python:3.5+,build +USE_LDCONFIG= yes USE_GITHUB= yes -GH_ACCOUNT= CVC4 -GH_PROJECT= CVC4 USE_JAVA= yes JAVA_BUILD= yes -USE_LDCONFIG= yes - CMAKE_BUILD_TYPE= Production -CMAKE_ARGS+= -DANTLR_BINARY=${WRKDIR}/antlr3 +CMAKE_ARGS+= -DANTLR_BINARY=${WRKDIR}/antlr3 \ + -DFREEBSD_DISTDIR=${DISTDIR} +CMAKE_ON= BUILD_SHARED_LIBS +CMAKE_OFF= BUILD_BINDINGS_PYTHON USE_PYTHON3 # Python binding should be a separate port -OPTIONS_DEFINE= CRYPTOMINISAT JAVA PYTHON READLINE +OPTIONS_DEFINE= CRYPTOMINISAT JAVA EDITLINE OPTIONS_RADIO= NUMLIB OPTIONS_RADIO_NUMLIB= GMP CLN -OPTIONS_DEFAULT= CRYPTOMINISAT JAVA PYTHON READLINE GMP +OPTIONS_DEFAULT= CRYPTOMINISAT JAVA EDITLINE 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_CMAKE_BOOL= USE_CRYPTOMINISAT CRYPTOMINISAT_LIB_DEPENDS= libcryptominisat5.so:math/cryptominisat @@ -59,25 +51,22 @@ JAVA_CMAKE_ON= -DJAVA_INCLUDE_PATH:PATH=${JAVA_HOME}/include \ -DJAVA_JVM_LIBRARY:PATH=${JAVA_HOME}/jre/lib/${ATCH}/libjava.so JAVA_BUILD_DEPENDS= swig:devel/swig -PYTHON_CMAKE_BOOL= BUILD_BINDINGS_PYTHON USE_PYTHON3 -PYTHON_BUILD_DEPENDS= swig:devel/swig - -READLINE_CMAKE_BOOL= USE_READLINE -READLINE_USES= readline +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 -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 +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:MREADLINE} || ${PORT_OPTIONS:MCLN} +.if ${PORT_OPTIONS:MCLN} LICENSE= GPLv3 CMAKE_ARGS+= -DENABLE_GPL:BOOL=ON .endif @@ -89,11 +78,7 @@ post-extract: @${CHMOD} +x ${WRKDIR}/antlr3 post-patch: - @${REINPLACE_CMD} -e "s|sed -i 's|sed -i '' 's|g" \ - ${WRKSRC}/src/fix-install-headers.sh - -# 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 + @${REINPLACE_CMD} -e "s|sed -i'' -e 's|sed -i '' -e 's|g" \ + ${WRKSRC}/src/fix-install-headers.sh .include diff --git a/math/cvc5/distinfo b/math/cvc5/distinfo new file mode 100644 index 000000000000..76743a798912 --- /dev/null +++ b/math/cvc5/distinfo @@ -0,0 +1,7 @@ +TIMESTAMP = 1672779263 +SHA256 (antlr-3.4-complete.jar) = 9d3e866b610460664522520f73b81777b5626fb0a282a5952b9800b751550bf7 +SIZE (antlr-3.4-complete.jar) = 2388361 +SHA256 (cvc5-cvc5-cvc5-1.0.3_GH0.tar.gz) = bf787b74c35ef61958865902e21dcb8f98f79d910b00a9e762a00ff8fcd2c462 +SIZE (cvc5-cvc5-cvc5-1.0.3_GH0.tar.gz) = 8335175 +SHA256 (fc8907afc08d.patch) = dfb42f7c9fbc4091d21ce4804f11c72945ccc9131f3d79dbc275fd9238ff55d4 +SIZE (fc8907afc08d.patch) = 1156 diff --git a/math/cvc5/files/patch-cmake_FindANTLR3.cmake b/math/cvc5/files/patch-cmake_FindANTLR3.cmake new file mode 100644 index 000000000000..4af6273f9f53 --- /dev/null +++ b/math/cvc5/files/patch-cmake_FindANTLR3.cmake @@ -0,0 +1,11 @@ +--- cmake/FindANTLR3.cmake.orig 2022-12-12 22:42:47 UTC ++++ cmake/FindANTLR3.cmake +@@ -18,7 +18,7 @@ + + include(deps-helper) + +-find_file(ANTLR3_JAR NAMES antlr-3.4-complete.jar PATH_SUFFIXES share/java/) ++set(ANTLR3_JAR ${FREEBSD_DISTDIR}/antlr-3.4-complete.jar) + find_path(ANTLR3_INCLUDE_DIR NAMES antlr3.h) + find_library(ANTLR3_LIBRARIES NAMES antlr3c) + diff --git a/math/cvc5/files/patch-cmake_FindEditline.cmake b/math/cvc5/files/patch-cmake_FindEditline.cmake new file mode 100644 index 000000000000..a8d897cd7b95 --- /dev/null +++ b/math/cvc5/files/patch-cmake_FindEditline.cmake @@ -0,0 +1,11 @@ +--- cmake/FindEditline.cmake.orig 2023-01-04 10:29:29 UTC ++++ cmake/FindEditline.cmake +@@ -41,7 +41,7 @@ if(Editline_INCLUDE_DIRS) + unset(CMAKE_REQUIRED_LIBRARIES) + unset(CMAKE_REQUIRED_INCLUDES) + +- if(NOT CMAKE_SYSTEM_NAME STREQUAL "Darwin") ++ if(FALSE AND NOT CMAKE_SYSTEM_NAME STREQUAL "Darwin") + set(Editline_LIBRARIES ${Editline_LIBRARIES} bsd tinfo) + endif() + endif() diff --git a/math/cvc4/pkg-descr b/math/cvc5/pkg-descr similarity index 100% rename from math/cvc4/pkg-descr rename to math/cvc5/pkg-descr diff --git a/math/cvc5/pkg-plist b/math/cvc5/pkg-plist new file mode 100644 index 000000000000..75d440acfa8e --- /dev/null +++ b/math/cvc5/pkg-plist @@ -0,0 +1,16 @@ +bin/cvc5 +include/cvc5/cvc5.h +include/cvc5/cvc5_export.h +include/cvc5/cvc5_kind.h +include/cvc5/cvc5_types.h +lib/cmake/cvc5/cvc5Config.cmake +lib/cmake/cvc5/cvc5ConfigVersion.cmake +lib/cmake/cvc5/cvc5JavaTargets.cmake +lib/cmake/cvc5/cvc5Targets-%%CMAKE_BUILD_TYPE%%.cmake +lib/cmake/cvc5/cvc5Targets.cmake +lib/libcvc5.so +%%JAVA%%lib/libcvc5jni.so +lib/libcvc5parser.so +lib/libcvc5parser.so.1 +%%JAVA%%%%JAVASHAREDIR%%/cvc5-1.0.3.jar +%%JAVA%%%%JAVASHAREDIR%%/cvc5.jar