Attachment 195132 Details for Bug 229780 – cvc4.patch

[patch] cvc4.patch

cvc4.patch (text/plain), 8.48 KB, created by Val Packett on 2018-07-15 00:12:42 UTC

(hide)

Description:

Filename:

MIME Type:

Creator: Val Packett

Created: 2018-07-15 00:12:42 UTC

Size: 8.48 KB

patch

obsolete

>diff --git c/math/cvc4/Makefile i/math/cvc4/Makefile
>index 426e951f4c72..67bba722afe4 100644
>--- c/math/cvc4/Makefile
>+++ i/math/cvc4/Makefile
>@@ -1,7 +1,7 @@
> # $FreeBSD$
> 
> PORTNAME=	cvc4
>-PORTVERSION=	1.5
>+PORTVERSION=	1.6
> CATEGORIES=	math java
> MASTER_SITES=	https://cvc4.cs.stanford.edu/downloads/builds/src/
> 
>@@ -13,11 +13,10 @@ LICENSE_FILE=	${WRKSRC}/COPYING
> 
> LIB_DEPENDS=	libantlr3c.so:devel/libantlr3c \
> 		libboost_system.so:devel/boost-libs
>-BUILD_DEPENDS=	gexpr:sysutils/coreutils \
>-		bash:shells/bash \
>+BUILD_DEPENDS=	bash:shells/bash \
> 		antlr3:devel/antlr3
> 
>-USES=		compiler:c++11-lang pkgconfig gmake libtool shebangfix localbase
>+USES=		compiler:c++11-lang python:3.5+,build pkgconfig autoreconf gmake libtool shebangfix localbase
> USE_JAVA=	yes
> JAVA_BUILD=	yes
> 
>@@ -27,17 +26,21 @@ CONFIGURE_ARGS+=	--disable-dependency-tracking \
> 			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
>+SHEBANG_FILES=		src/mk* src/theory/mk* src/base/mk* src/expr/mk* src/options/mk* test/regress/run_regression.py
> 
>-OPTIONS_DEFINE=		JAVA READLINE DEBUG
>+OPTIONS_DEFINE=		CRYPTOMINISAT JAVA READLINE DEBUG
> OPTIONS_RADIO=		NUMLIB
> OPTIONS_RADIO_NUMLIB=	GMP CLN
>-OPTIONS_DEFAULT=	READLINE GMP
>+OPTIONS_DEFAULT=	CRYPTOMINISAT 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_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}
>@@ -61,9 +64,6 @@ DEBUG_CONFIGURE_ON=		--with-build=debug
> DEBUG_CONFIGURE_OFF=		--with-build=production
> DEBUG_INSTALL_TARGET_OFF=	install-strip
> 
>-post-patch:
>-	${REINPLACE_CMD} -e 's|expr |gexpr |g' ${WRKSRC}/src/options/mkoptions
>-
> .include <bsd.port.options.mk>
> 
> .if ${PORT_OPTIONS:MREADLINE} || ${PORT_OPTIONS:MCLN}
>diff --git c/math/cvc4/distinfo i/math/cvc4/distinfo
>index 579934f7d6c3..a251931aa151 100644
>--- c/math/cvc4/distinfo
>+++ i/math/cvc4/distinfo
>@@ -1,3 +1,3 @@
>-TIMESTAMP = 1524235369
>-SHA256 (cvc4-1.5.tar.gz) = 5d6b4f8ee8420f85e3f804181341cedf6ea32342c48f355a5be87754152b14e9
>-SIZE (cvc4-1.5.tar.gz) = 8059968
>+TIMESTAMP = 1531429558
>+SHA256 (cvc4-1.6.tar.gz) = 5c18bd5ea893fba9723a4d35c889d412ec6d29a21db9db69481891a8ff4887c7
>+SIZE (cvc4-1.6.tar.gz) = 7815893
>diff --git c/math/cvc4/files/patch-config_cryptominisat.m4 i/math/cvc4/files/patch-config_cryptominisat.m4
>new file mode 100644
>index 000000000000..96985b4b41d7
>--- /dev/null
>+++ i/math/cvc4/files/patch-config_cryptominisat.m4
>@@ -0,0 +1,31 @@
>+--- 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
>new file mode 100644
>index 000000000000..b4177f36639f
>--- /dev/null
>+++ i/math/cvc4/files/patch-configure.ac
>@@ -0,0 +1,11 @@
>+--- 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 i/math/cvc4/files/patch-src_base_configuration.cpp
>index 6e48c9e5c562..4206b023799e 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-04-22 17:53:43 UTC
>+--- src/base/configuration.cpp.orig	2018-06-25 21:13:17 UTC
> +++ src/base/configuration.cpp
>-@@ -291,7 +291,7 @@ std::string Configuration::getCompiler() {
>+@@ -405,7 +405,7 @@ std::string Configuration::getCompiler() {
>  }
>  
>  std::string Configuration::getCompiledDateTime() {
>diff --git c/math/cvc4/pkg-plist i/math/cvc4/pkg-plist
>index a7758f76b670..4c8bb1c64da8 100644
>--- c/math/cvc4/pkg-plist
>+++ i/math/cvc4/pkg-plist
>@@ -1,11 +1,9 @@
> bin/cvc4
>-bin/lfsc-checker
> %%GMP%%bin/pcvc4
> include/cvc4/base/configuration.h
> include/cvc4/base/exception.h
> include/cvc4/base/listener.h
> include/cvc4/base/modal_exception.h
>-include/cvc4/base/ptr_closer.h
> include/cvc4/base/tls.h
> include/cvc4/bindings/compat/c/c_interface.h
> include/cvc4/bindings/compat/c/c_interface_defs.h
>@@ -36,7 +34,6 @@ 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/predicate.h
> include/cvc4/expr/record.h
> include/cvc4/expr/symbol_table.h
> include/cvc4/expr/type.h
>@@ -46,6 +43,7 @@ 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
>@@ -53,11 +51,13 @@ 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/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
>@@ -79,6 +79,7 @@ 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
>@@ -88,27 +89,26 @@ include/cvc4/util/resource_manager.h
> include/cvc4/util/result.h
> include/cvc4/util/sexpr.h
> include/cvc4/util/statistics.h
>-include/cvc4/util/subrange_bound.h
> include/cvc4/util/tuple.h
> include/cvc4/util/unsafe_interrupt_exception.h
> %%JAVA%%lib/jni/libcvc4compatjni.so
>-%%JAVA%%lib/jni/libcvc4compatjni.so.4
>-%%JAVA%%lib/jni/libcvc4compatjni.so.4.0.0
>+%%JAVA%%lib/jni/libcvc4compatjni.so.5
>+%%JAVA%%lib/jni/libcvc4compatjni.so.5.0.0
> %%JAVA%%lib/jni/libcvc4jni.so
>-%%JAVA%%lib/jni/libcvc4jni.so.4
>-%%JAVA%%lib/jni/libcvc4jni.so.4.0.0
>+%%JAVA%%lib/jni/libcvc4jni.so.5
>+%%JAVA%%lib/jni/libcvc4jni.so.5.0.0
> lib/libcvc4.so
>-lib/libcvc4.so.4
>-lib/libcvc4.so.4.0.0
>+lib/libcvc4.so.5
>+lib/libcvc4.so.5.0.0
> lib/libcvc4bindings_c_compat.so
>-lib/libcvc4bindings_c_compat.so.4
>-lib/libcvc4bindings_c_compat.so.4.0.0
>+lib/libcvc4bindings_c_compat.so.5
>+lib/libcvc4bindings_c_compat.so.5.0.0
> lib/libcvc4compat.so
>-lib/libcvc4compat.so.4
>-lib/libcvc4compat.so.4.0.0
>+lib/libcvc4compat.so.5
>+lib/libcvc4compat.so.5.0.0
> lib/libcvc4parser.so
>-lib/libcvc4parser.so.4
>-lib/libcvc4parser.so.4.0.0
>+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

Actions: View | Diff

Attachments on bug 229780: 195132