git: 7a04fc568338 - main - Remove math/cvc3, it was succeeded by CVC4 and CVC5

Go to: [ bottom of page ] [ top of archives ] [ this month ]
From: Li-Wen Hsu <lwhsu_at_FreeBSD.org>
Date: Thu, 05 Jan 2023 08:16:28 UTC
The branch main has been updated by lwhsu:

URL: https://cgit.FreeBSD.org/ports/commit/?id=7a04fc56833848131e198bfaed4c7d5b468cb87d

commit 7a04fc56833848131e198bfaed4c7d5b468cb87d
Author:     Li-Wen Hsu <lwhsu@FreeBSD.org>
AuthorDate: 2023-01-05 08:12:39 +0000
Commit:     Li-Wen Hsu <lwhsu@FreeBSD.org>
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 <bsd.port.mk>
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