Attachment 204867 Details for Bug 238376 – cvc4.patch

[patch] cvc4.patch

cvc4.patch (text/plain), 11.39 KB, created by Val Packett on 2019-06-06 23:52:00 UTC

(hide)

Description:

Filename:

MIME Type:

Creator: Val Packett

Created: 2019-06-06 23:52:00 UTC

Size: 11.39 KB

patch

obsolete

>diff --git c/math/cvc4/Makefile w/math/cvc4/Makefile
>index ff581deff760..da2838e50660 100644
>--- c/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,72 @@ 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
>+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
>+
>+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
>+
> .include <bsd.port.mk>
>diff --git c/math/cvc4/distinfo w/math/cvc4/distinfo
>index a251931aa151..a16df890b9e7 100644
>--- c/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
>diff --git c/math/cvc4/files/patch-config_cryptominisat.m4 w/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 w/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-src_base_configuration.cpp w/math/cvc4/files/patch-src_base_configuration.cpp
>index 4206b023799e..43541f78a272 100644
>--- c/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() {
>diff --git c/math/cvc4/pkg-plist w/math/cvc4/pkg-plist
>index 4c8bb1c64da8..9a057af977ee 100644
>--- c/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

Actions: View | Diff

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