From nobody Thu Jan 05 08:16:28 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 4NnfSX5xPzz2r1sr; Thu, 5 Jan 2023 08:16:28 +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 4NnfSX5SgJz4Z9b; Thu, 5 Jan 2023 08:16:28 +0000 (UTC) (envelope-from git@FreeBSD.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1672906588; 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=dVGahysERndqR508+n3Wbn/WCJuZvA2nGQIx1nlz58Q=; b=OoDFjl2muUHE1z4wxQo1KmSVkV+vGh1jmuXxXrXUcJy3FzxVxrdB736+6Rv8b3pQ3VRI+B 2Nle8QSxxagjTYRKduVLsJXqzNG0pvVgomQUNRzAqf7rsDJ05sO3dXUanBwAW/J4IQ0v2f GnKvh37I7L0H7HY+kznUhOCegL1qwX8kZotoD4pZ1GZur1I/SvEQ6jm7ac+ZWlZhaUvEKS aDEzN0PL4HeVJIkYzNj9+AOWOI6/hLAYezALw7DKZqbkD40voRMDiTq8Q4PLdHIvbpVClb obrkiHMjOotu2qD4PN8L6NDaf3GAfFzZKONB1oJO6rczVRc/SfXJjjVt0rrdRA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1672906588; 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=dVGahysERndqR508+n3Wbn/WCJuZvA2nGQIx1nlz58Q=; b=PT50joS9yoL6XGEFQ90oagJqOEfScfaS0RGGs+n0OWz6gIyzvqGLMdqQ+4wycOoAWhtWyD cW7tUSOiAHC3EsxyuI3ldg7cqA2w+8OGwIczyxltDbI9RGTGg4d1aTYU3UjNGXJZ3x9kl+ MgK8A8NmTKzYAOhmeRUUosy5qlLfiVdm3ZuPXVpW+qoifDpR8t4CYFso4HKq6VIZSPF/SW ziSYCXW0Xfcnc7RDGPuJVcNAd5Ki9lBVD9z9TpVADz14BgOTyeRUsFkz4u0VbGZRhbdCKw 0lsVdoEpTsbbCjbIe7xl/bksePOurdJBOvyfHgbHA5jkp5KGCRkWsqTivkdohw== ARC-Authentication-Results: i=1; mx1.freebsd.org; none ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1672906588; a=rsa-sha256; cv=none; b=wrxwdnT54OYk8ILfZ4fhticlQjmvMll9ZIuwLF9X3rglSevp+a/UexU413K9d0PErilEYC P3r+O+RHmFlbCGDr6DYc/9WqNncFQElBDyxtJ7QLGld9CbifMHJuD2F8L1M4Qdcpj2GfNs Y4+tCdvYU8E8kiWf2bYHqtkzaMKTvuh/Pz5Zid5ZI25TKazl8IKog0wV0qNKdsqMZ4LxVP m5xVWs9nzqYW03hWM+oFuXLg6vMJS8Ir+s36VLFHdw+BDg3JQs91WcB84lW4DYHuFts0B0 9jTtgNg85aORgviG2rDaaMxV6AvL9T7yfyTZbCTAVBJABavp7kru52ZW9ls2gw== 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 4NnfSX4QNpzk3v; Thu, 5 Jan 2023 08:16:28 +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 3058GS2O004076; Thu, 5 Jan 2023 08:16:28 GMT (envelope-from git@gitrepo.freebsd.org) Received: (from git@localhost) by gitrepo.freebsd.org (8.16.1/8.16.1/Submit) id 3058GSqr004075; Thu, 5 Jan 2023 08:16:28 GMT (envelope-from git) Date: Thu, 5 Jan 2023 08:16:28 GMT Message-Id: <202301050816.3058GSqr004075@gitrepo.freebsd.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org From: Li-Wen Hsu Subject: git: 7a04fc568338 - main - Remove math/cvc3, it was succeeded by CVC4 and 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: lwhsu X-Git-Repository: ports X-Git-Refname: refs/heads/main X-Git-Reftype: branch X-Git-Commit: 7a04fc56833848131e198bfaed4c7d5b468cb87d Auto-Submitted: auto-generated X-ThisMailContainsUnwantedMimeParts: N The branch main has been updated by lwhsu: URL: https://cgit.FreeBSD.org/ports/commit/?id=7a04fc56833848131e198bfaed4c7d5b468cb87d commit 7a04fc56833848131e198bfaed4c7d5b468cb87d Author: Li-Wen Hsu AuthorDate: 2023-01-05 08:12:39 +0000 Commit: Li-Wen Hsu CommitDate: 2023-01-05 08:16:03 +0000 Remove math/cvc3, it was succeeded by CVC4 and CVC5 Reported by: yuri --- MOVED | 1 + math/Makefile | 1 - math/cvc3/Makefile | 34 ----------- math/cvc3/distinfo | 2 - math/cvc3/files/patch-src-Makefile | 43 -------------- math/cvc3/files/patch-src-parser-Makefile | 35 ------------ math/cvc3/pkg-descr | 22 -------- math/cvc3/pkg-plist | 93 ------------------------------- 8 files changed, 1 insertion(+), 230 deletions(-) diff --git a/MOVED b/MOVED index 95671d3e34fd..9c9f2116f947 100644 --- a/MOVED +++ b/MOVED @@ -17748,3 +17748,4 @@ 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 +math/cvc3|math/cvc5|2023-01-04|CVC3 was succeeded by CVC4 and CVC5 diff --git a/math/Makefile b/math/Makefile index cbe924b35d07..6e2c159a88df 100644 --- a/math/Makefile +++ b/math/Makefile @@ -263,7 +263,6 @@ SUBDIR += ctl-sat SUBDIR += cudd SUBDIR += curv - SUBDIR += cvc3 SUBDIR += cvc5 SUBDIR += dbcsr SUBDIR += deal.ii diff --git a/math/cvc3/Makefile b/math/cvc3/Makefile deleted file mode 100644 index 962e86f0ea22..000000000000 --- a/math/cvc3/Makefile +++ /dev/null @@ -1,34 +0,0 @@ -PORTNAME= cvc3 -PORTVERSION= 2.4.1 -PORTREVISION= 7 -CATEGORIES= math -MASTER_SITES= http://www.cs.nyu.edu/acsys/cvc3/download/${PORTVERSION}/ - -MAINTAINER= lwhsu@FreeBSD.org -COMMENT= Automatic theorem prover for the SMT problem -WWW= https://www.cs.nyu.edu/acsys/cvc3/ - -LIB_DEPENDS= libgmp.so:math/gmp - -CONFIGURE_ARGS= --enable-dynamic \ - --with-arith=gmp \ - --with-build=optimized \ - --with-extra-includes=${LOCALBASE}/include \ - --with-extra-libs=${LOCALBASE}/lib -CXXFLAGS+= -fPIC -GNU_CONFIGURE= yes -USES= bison gmake pathfix perl5 -PATHFIX_MAKEFILEIN= Makefile -USE_CXXSTD= gnu++98 -USE_GCC= yes -USE_LDCONFIG= yes - -post-patch: - ${REINPLACE_CMD} -e 's,/bin/bash,/bin/sh,' ${WRKSRC}/Makefile.std - ${REINPLACE_CMD} -e 's,.*$$(LDCONFIG).*,,' ${WRKSRC}/src/Makefile - -post-install: - ${INSTALL_PROGRAM} `readlink ${WRKSRC}/bin/cvc3` ${STAGEDIR}${PREFIX}/bin - ${STRIP_CMD} ${STAGEDIR}${PREFIX}/lib/libcvc3.so.5.0.0 - -.include diff --git a/math/cvc3/distinfo b/math/cvc3/distinfo deleted file mode 100644 index a28de6748653..000000000000 --- a/math/cvc3/distinfo +++ /dev/null @@ -1,2 +0,0 @@ -SHA256 (cvc3-2.4.1.tar.gz) = d55b1d6006cfbac3f6d4c086964558902c3ed0efa66ac499cfb2193f3ee4acf7 -SIZE (cvc3-2.4.1.tar.gz) = 1196616 diff --git a/math/cvc3/files/patch-src-Makefile b/math/cvc3/files/patch-src-Makefile deleted file mode 100644 index 2543b3b6cac7..000000000000 --- a/math/cvc3/files/patch-src-Makefile +++ /dev/null @@ -1,43 +0,0 @@ ---- src/Makefile.orig 2014-07-16 11:12:07.907490115 +0800 -+++ src/Makefile 2014-07-16 11:18:34.387487445 +0800 -@@ -254,27 +254,27 @@ HEADERS = $(patsubst %, $(TOP)/src/inclu - - install: $(HEADERS) - $(MAKE) build TARGET= -- mkdir -p $(incdir) -- $(INSTALL) $(INSTALL_FLAGS) -m 644 $(HEADERS) $(incdir) -- mkdir -p $(libdir) -+ mkdir -p $(DESTDIR)$(incdir) -+ $(INSTALL) $(INSTALL_FLAGS) -m 644 $(HEADERS) $(DESTDIR)$(incdir) -+ mkdir -p $(DESTDIR)$(libdir) - ifeq ($(STATIC),1) -- $(INSTALL) $(INSTALL_FLAGS) -m 644 $(CVC_LIB_DIR)/$(CVC_LIB_NAME).$(LIB_VERSION) $(libdir) -- ln -sf $(CVC_LIB_NAME).$(LIB_VERSION) $(libdir)/$(call notdirx,$(CVC_LIB)) -+ $(INSTALL) $(INSTALL_FLAGS) -m 644 $(CVC_LIB_DIR)/$(CVC_LIB_NAME).$(LIB_VERSION) $(DESTDIR)$(libdir) -+ ln -sf $(CVC_LIB_NAME).$(LIB_VERSION) $(DESTDIR)$(libdir)/$(call notdirx,$(CVC_LIB)) - else -- $(INSTALL) $(INSTALL_FLAGS) -m 644 $(CVC_LIB) $(libdir) -+ $(INSTALL) $(INSTALL_FLAGS) -m 644 $(CVC_LIB) $(DESTDIR)$(libdir) - ifeq ($(MAC_OSX),) - ifeq ($(CYGWIN),) - $(LDCONFIG) -nv $(libdir) - endif - endif -- ln -sf $(CVC_LIB_NAME) $(libdir)/$(LIB_SHARED_COMPAT) -- ln -sf $(CVC_LIB_NAME) $(libdir)/$(LIB_SHARED_MAJOR) -- ln -sf $(CVC_LIB_NAME) $(libdir)/$(LIB_SHARED_BASE) -+ ln -sf $(CVC_LIB_NAME) $(DESTDIR)$(libdir)/$(LIB_SHARED_COMPAT) -+ ln -sf $(CVC_LIB_NAME) $(DESTDIR)$(libdir)/$(LIB_SHARED_MAJOR) -+ ln -sf $(CVC_LIB_NAME) $(DESTDIR)$(libdir)/$(LIB_SHARED_BASE) - endif -- mkdir -p $(bindir) -- $(INSTALL) $(INSTALL_FLAGS) -m 755 $(CVC_EXE) $(bindir) -- mkdir -p $(prefix)/libdata/pkgconfig -- $(INSTALL) $(INSTALL_FLAGS) -m 644 cvc3.pc $(prefix)/libdata/pkgconfig -+ mkdir -p $(DESTDIR)$(bindir) -+ $(INSTALL) $(INSTALL_FLAGS) -m 755 $(CVC_EXE) $(DESTDIR)$(bindir) -+ mkdir -p $(DESTDIR)$(prefix)/libdata/pkgconfig -+ $(INSTALL) $(INSTALL_FLAGS) -m 644 cvc3.pc $(DESTDIR)$(prefix)/libdata/pkgconfig - - ifndef FILELIST - FILELIST = /dev/null diff --git a/math/cvc3/files/patch-src-parser-Makefile b/math/cvc3/files/patch-src-parser-Makefile deleted file mode 100644 index 913580694114..000000000000 --- a/math/cvc3/files/patch-src-parser-Makefile +++ /dev/null @@ -1,35 +0,0 @@ ---- src/parser/Makefile.orig 2010-06-16 17:55:52 UTC -+++ src/parser/Makefile -@@ -38,7 +38,7 @@ parsePL_defs.h: parsePL.cpp - parsePL.cpp: PL.y - $(YACC) $(YFLAGS) -o parsePL.cpp -p PL --debug -v PL.y - @if [ -f parsePL.cpp.h ]; then mv parsePL.cpp.h parsePL.hpp; fi -- @mv parsePL.hpp parsePL_defs.h -+ @cp parsePL.hpp parsePL_defs.h - - lexLisp.cpp: Lisp.lex parseLisp_defs.h - $(LEX) $(LFLAGS) -I -PLisp -olexLisp.cpp Lisp.lex -@@ -48,7 +48,7 @@ parseLisp_defs.h: parseLisp.cpp - parseLisp.cpp: Lisp.y - $(YACC) $(YFLAGS) -o parseLisp.cpp -p Lisp --debug -v Lisp.y - @if [ -f parseLisp.cpp.h ]; then mv parseLisp.cpp.h parseLisp.hpp; fi -- @mv parseLisp.hpp parseLisp_defs.h -+ @cp parseLisp.hpp parseLisp_defs.h - - lexsmtlib.cpp: smtlib.lex parsesmtlib_defs.h - $(LEX) $(LFLAGS) -I -Psmtlib -olexsmtlib.cpp smtlib.lex -@@ -58,7 +58,7 @@ parsesmtlib_defs.h: parsesmtlib.cpp - parsesmtlib.cpp: smtlib.y - $(YACC) $(YFLAGS) -o parsesmtlib.cpp -p smtlib --debug -v smtlib.y - @if [ -f parsesmtlib.cpp.h ]; then mv parsesmtlib.cpp.h parsesmtlib.hpp; fi -- @mv parsesmtlib.hpp parsesmtlib_defs.h -+ @cp parsesmtlib.hpp parsesmtlib_defs.h - - lexsmtlib2.cpp: smtlib2.lex parsesmtlib2_defs.h - $(LEX) $(LFLAGS) -I -Psmtlib2 -olexsmtlib2.cpp smtlib2.lex -@@ -68,4 +68,4 @@ parsesmtlib2_defs.h: parsesmtlib2.cpp - parsesmtlib2.cpp: smtlib2.y - $(YACC) $(YFLAGS) -o parsesmtlib2.cpp -p smtlib2 --debug -v smtlib2.y - @if [ -f parsesmtlib2.cpp.h ]; then mv parsesmtlib2.cpp.h parsesmtlib2.hpp; fi -- @mv parsesmtlib2.hpp parsesmtlib2_defs.h -+ @cp parsesmtlib2.hpp parsesmtlib2_defs.h diff --git a/math/cvc3/pkg-descr b/math/cvc3/pkg-descr deleted file mode 100644 index 0786d4d1a1a5..000000000000 --- a/math/cvc3/pkg-descr +++ /dev/null @@ -1,22 +0,0 @@ -CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) -problems. It can be used to prove the validity (or, dually, the -satisfiability) of first-order formulas in a large number of built-in logical -theories and their combination. - -CVC3 is the last offspring of a series of popular SMT provers, which originated -at Stanford University with the SVC system. In particular, it builds on the -code base of CVC Lite, its most recent predecessor. Its high level design -follows that of the Sammy prover. - -CVC3 works with a version of first-order logic with polymorphic types and has -a wide variety of features including: - * several built-in base theories: rational and integer linear arithmetic, - arrays, tuples, records, inductive data types, bit vectors, and equality - over uninterpreted function symbols; - * support for quantifiers; - * an interactive text-based interface; - * a rich C and C++ API for embedding in other systems; - * proof and model generation abilities; - * predicate subtyping; - * essentially no limit on its use for research or commercial purposes - (see license). diff --git a/math/cvc3/pkg-plist b/math/cvc3/pkg-plist deleted file mode 100644 index c8eca32ed383..000000000000 --- a/math/cvc3/pkg-plist +++ /dev/null @@ -1,93 +0,0 @@ -bin/cvc3 -include/cvc3/assumptions.h -include/cvc3/c_interface.h -include/cvc3/c_interface_defs.h -include/cvc3/cdflags.h -include/cvc3/cdlist.h -include/cvc3/cdmap.h -include/cvc3/cdmap_ordered.h -include/cvc3/cdo.h -include/cvc3/circuit.h -include/cvc3/clause.h -include/cvc3/cnf.h -include/cvc3/cnf_manager.h -include/cvc3/command_line_exception.h -include/cvc3/command_line_flags.h -include/cvc3/common_proof_rules.h -include/cvc3/compat_hash_map.h -include/cvc3/compat_hash_set.h -include/cvc3/context.h -include/cvc3/cvc_util.h -include/cvc3/debug.h -include/cvc3/dpllt.h -include/cvc3/dpllt_basic.h -include/cvc3/dpllt_minisat.h -include/cvc3/eval_exception.h -include/cvc3/exception.h -include/cvc3/expr.h -include/cvc3/expr_hash.h -include/cvc3/expr_manager.h -include/cvc3/expr_map.h -include/cvc3/expr_op.h -include/cvc3/expr_stream.h -include/cvc3/expr_transform.h -include/cvc3/expr_value.h -include/cvc3/fdstream.h -include/cvc3/formula_value.h -include/cvc3/hash_fun.h -include/cvc3/hash_map.h -include/cvc3/hash_set.h -include/cvc3/hash_table.h -include/cvc3/kinds.h -include/cvc3/lang.h -include/cvc3/memory_manager.h -include/cvc3/memory_manager_chunks.h -include/cvc3/memory_manager_context.h -include/cvc3/memory_manager_malloc.h -include/cvc3/notifylist.h -include/cvc3/os.h -include/cvc3/parser.h -include/cvc3/parser_exception.h -include/cvc3/pretty_printer.h -include/cvc3/proof.h -include/cvc3/queryresult.h -include/cvc3/rational.h -include/cvc3/sat_api.h -include/cvc3/search.h -include/cvc3/search_fast.h -include/cvc3/search_impl_base.h -include/cvc3/search_sat.h -include/cvc3/search_simple.h -include/cvc3/smartcdo.h -include/cvc3/smtlib_exception.h -include/cvc3/sound_exception.h -include/cvc3/statistics.h -include/cvc3/theorem.h -include/cvc3/theorem_manager.h -include/cvc3/theorem_producer.h -include/cvc3/theory.h -include/cvc3/theory_arith.h -include/cvc3/theory_arith3.h -include/cvc3/theory_arith_new.h -include/cvc3/theory_arith_old.h -include/cvc3/theory_array.h -include/cvc3/theory_bitvector.h -include/cvc3/theory_core.h -include/cvc3/theory_datatype.h -include/cvc3/theory_datatype_lazy.h -include/cvc3/theory_quant.h -include/cvc3/theory_records.h -include/cvc3/theory_simulate.h -include/cvc3/theory_uf.h -include/cvc3/translator.h -include/cvc3/type.h -include/cvc3/typecheck_exception.h -include/cvc3/variable.h -include/cvc3/vc.h -include/cvc3/vc_cmd.h -include/cvc3/vcl.h -lib/libcvc3.so -lib/libcvc3.so.5 -lib/libcvc3.so.5.0 -lib/libcvc3.so.5.0.0 -libdata/pkgconfig/cvc3.pc