Attachment 206129 Details for Bug 238376 – cvc4.patch v3

[patch] cvc4.patch v3

cvc4.patch (text/plain), 18.83 KB, created by Val Packett on 2019-07-28 18:33:39 UTC

(hide)

Description:

Filename:

MIME Type:

Creator: Val Packett

Created: 2019-07-28 18:33:39 UTC

Size: 18.83 KB

patch

obsolete

>diff --git c/math/cvc4/Makefile i/math/cvc4/Makefile
>index ff581deff760..4ed4b903b87a 100644
>--- c/math/cvc4/Makefile
>+++ i/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,78 @@ 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 <bsd.port.options.mk>
> 
> .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
>+	@${REINPLACE_CMD} -e "s|sed -i 's|sed -ibak 's|g" \
>+		${WRKSRC}/src/fix-install-headers.sh
>+
> .include <bsd.port.mk>
>diff --git c/math/cvc4/distinfo i/math/cvc4/distinfo
>index a251931aa151..a16df890b9e7 100644
>--- c/math/cvc4/distinfo
>+++ i/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
>diff --git c/math/cvc4/files/patch-cmake_FindANTLR.cmake i/math/cvc4/files/patch-cmake_FindANTLR.cmake
>new file mode 100644
>index 000000000000..ae6462f57e37
>--- /dev/null
>+++ i/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()
>diff --git c/math/cvc4/files/patch-cmake_FindReadline.cmake i/math/cvc4/files/patch-cmake_FindReadline.cmake
>new file mode 100644
>index 000000000000..50c691763f06
>--- /dev/null
>+++ i/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 <stdio.h>
>+-    #include <readline/readline.h>
>+-    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 <stdio.h>
>+-     #include <readline/readline.h>
>+-     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 c/math/cvc4/files/patch-config_cryptominisat.m4 i/math/cvc4/files/patch-config_cryptominisat.m4
>deleted file mode 100644
>index 96985b4b41d7..000000000000
>--- 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(
>diff --git c/math/cvc4/files/patch-configure.ac i/math/cvc4/files/patch-configure.ac
>deleted file mode 100644
>index b4177f36639f..000000000000
>--- 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])
>diff --git c/math/cvc4/files/patch-doc_CMakeLists.txt i/math/cvc4/files/patch-doc_CMakeLists.txt
>new file mode 100644
>index 000000000000..764bb44e1d12
>--- /dev/null
>+++ i/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)
>diff --git c/math/cvc4/files/patch-examples_CMakeLists.txt i/math/cvc4/files/patch-examples_CMakeLists.txt
>new file mode 100644
>index 000000000000..60ccd1f7adbf
>--- /dev/null
>+++ i/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.
>+ #
>diff --git c/math/cvc4/files/patch-src_CMakeLists.txt i/math/cvc4/files/patch-src_CMakeLists.txt
>new file mode 100644
>index 000000000000..a516e618fe82
>--- /dev/null
>+++ i/math/cvc4/files/patch-src_CMakeLists.txt
>@@ -0,0 +1,11 @@
>+--- 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 c/math/cvc4/files/patch-src_base_configuration.cpp i/math/cvc4/files/patch-src_base_configuration.cpp
>index 4206b023799e..43541f78a272 100644
>--- c/math/cvc4/files/patch-src_base_configuration.cpp
>+++ i/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() {
>diff --git c/math/cvc4/files/patch-test_CMakeLists.txt i/math/cvc4/files/patch-test_CMakeLists.txt
>new file mode 100644
>index 000000000000..43d5da2a3df0
>--- /dev/null
>+++ i/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
>diff --git c/math/cvc4/files/patch-test_regress_CMakeLists.txt i/math/cvc4/files/patch-test_regress_CMakeLists.txt
>new file mode 100644
>index 000000000000..a52d05061534
>--- /dev/null
>+++ i/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}
>diff --git c/math/cvc4/files/patch-test_system_CMakeLists.txt i/math/cvc4/files/patch-test_system_CMakeLists.txt
>new file mode 100644
>index 000000000000..d05dbdc083df
>--- /dev/null
>+++ i/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)
>+ 
>diff --git c/math/cvc4/pkg-plist i/math/cvc4/pkg-plist
>index 4c8bb1c64da8..9a057af977ee 100644
>--- c/math/cvc4/pkg-plist
>+++ i/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

Actions: View | Diff

Attachments on bug 238376: 204867 | 206060 | 206064 | 206129 | 206158 | 206159 | 206182