[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/files/, sci-mathematics/cvc4/

2024-05-20 Thread Alfredo Tupone 
commit: c11cbec28dbd063e597839ed1603f9bea62d3e73
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Mon May 20 13:03:04 2024 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Mon May 20 13:03:54 2024 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=c11cbec2

sci-mathematics/cvc4: fix musl build

Closes: https://bugs.gentoo.org/839402
Signed-off-by: Alfredo Tupone  gentoo.org>

 sci-mathematics/cvc4/cvc4-1.8-r5.ebuild| 11 +++-
 sci-mathematics/cvc4/files/cvc4-1.8-musl.patch | 80 ++
 2 files changed, 89 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.8-r5.ebuild 
b/sci-mathematics/cvc4/cvc4-1.8-r5.ebuild
index 6de0fc9372aa..4870f7af7ba6 100644
--- a/sci-mathematics/cvc4/cvc4-1.8-r5.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.8-r5.ebuild
@@ -11,6 +11,8 @@ DESCRIPTION="Automatic theorem prover for satisfiability 
modulo theories (SMT) p
 HOMEPAGE="https://cvc4.github.io/;
 SRC_URI="https://github.com/CVC4/CVC4-archived/archive/refs/tags/${PV}.tar.gz 
-> ${P}.tar.gz"
 
+S="${WORKDIR}"/${PN^^}-archived-${PV}
+
 LICENSE="GPL-2"
 SLOT="0"
 KEYWORDS="~amd64 ~x86"
@@ -28,8 +30,6 @@ BDEPEND="$(python_gen_any_dep '
')
 "
 
-S="${WORKDIR}"/${PN^^}-archived-${PV}
-
 PATCHES=(
"${FILESDIR}"/${P}-gentoo.patch
"${FILESDIR}"/${P}-toml.patch
@@ -40,6 +40,13 @@ python_check_deps() {
python_has_version "dev-python/tomli[${PYTHON_USEDEP}]"
 }
 
+src_prepare() {
+   cmake_src_prepare
+   if use elibc_musl ; then
+   eapply "${FILESDIR}"/${P}-musl.patch
+   fi
+}
+
 src_configure() {
local mycmakeargs=(
-DANTLR_BINARY=/usr/bin/antlr3

diff --git a/sci-mathematics/cvc4/files/cvc4-1.8-musl.patch 
b/sci-mathematics/cvc4/files/cvc4-1.8-musl.patch
new file mode 100644
index ..3448f9bab64f
--- /dev/null
+++ b/sci-mathematics/cvc4/files/cvc4-1.8-musl.patch
@@ -0,0 +1,80 @@
+--- a/src/prop/bvminisat/simp/Main.cc  2024-05-20 14:52:26.827202665 +0200
 b/src/prop/bvminisat/simp/Main.cc  2024-05-20 14:53:05.967758613 +0200
+@@ -80,11 +80,6 @@
+ setUsageHelp("USAGE: %s [options]  
\n\n  where input may be either in plain or gzipped 
DIMACS.\n");
+ // printf("This is MiniSat 2.0 beta\n");
+ 
+-#if defined(__linux__)
+-fpu_control_t oldcw, newcw;
+-_FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; 
_FPU_SETCW(newcw);
+-printf("WARNING: for repeatability, setting FPU to use double 
precision\n");
+-#endif
+ // Extra options:
+ //
+ IntOptionverb   ("MAIN", "verb",   "Verbosity level (0=silent, 
1=some, 2=more).", 1, IntRange(0, 2));
+--- a/src/prop/bvminisat/core/Main.cc  2024-05-20 14:52:35.361105845 +0200
 b/src/prop/bvminisat/core/Main.cc  2024-05-20 14:53:27.116518689 +0200
+@@ -80,11 +80,6 @@
+ setUsageHelp("USAGE: %s [options]  
\n\n  where input may be either in plain or gzipped 
DIMACS.\n");
+ // printf("This is MiniSat 2.0 beta\n");
+ 
+-#if defined(__linux__)
+-fpu_control_t oldcw, newcw;
+-_FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; 
_FPU_SETCW(newcw);
+-printf("WARNING: for repeatability, setting FPU to use double 
precision\n");
+-#endif
+ // Extra options:
+ //
+ IntOptionverb   ("MAIN", "verb",   "Verbosity level (0=silent, 
1=some, 2=more).", 1, IntRange(0, 2));
+--- a/src/prop/minisat/simp/Main.cc2024-05-20 14:52:44.044007338 +0200
 b/src/prop/minisat/simp/Main.cc2024-05-20 14:53:39.356379840 +0200
+@@ -81,11 +81,6 @@
+ setUsageHelp("USAGE: %s [options]  
\n\n  where input may be either in plain or gzipped 
DIMACS.\n");
+ // printf("This is MiniSat 2.0 beta\n");
+ 
+-#if defined(__linux__)
+-fpu_control_t oldcw, newcw;
+-_FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; 
_FPU_SETCW(newcw);
+-printf("WARNING: for repeatability, setting FPU to use double 
precision\n");
+-#endif
+ // Extra options:
+ //
+ IntOptionverb   ("MAIN", "verb",   "Verbosity level (0=silent, 
1=some, 2=more).", 1, IntRange(0, 2));
+--- a/src/prop/minisat/core/Main.cc2024-05-20 14:52:50.063939036 +0200
 b/src/prop/minisat/core/Main.cc2024-05-20 14:53:53.834215599 +0200
+@@ -79,11 +79,6 @@
+ setUsageHelp("USAGE: %s [options]  
\n\n  where input may be either in plain or gzipped 
DIMACS.\n");
+ // printf("This is MiniSat 2.0 beta\n");
+ 
+-#if defined(__linux__)
+-fpu_control_t oldcw, newcw;
+-_FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; 
_FPU_SETCW(newcw);
+-printf("WARNING: for repeatability, setting FPU to use double 
precision\n");
+-#endif
+ // Extra options:
+ //
+ IntOptionverb   ("MAIN", "verb",   "Verbosity level (0=silent, 
1=some, 2=more).", 1, IntRange(0, 2));

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2024-01-19 Thread Alfredo Tupone 
commit: 81be47150ce44a0ed7c89b58fa1dafa072907392
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Fri Jan 19 21:30:37 2024 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Fri Jan 19 21:31:45 2024 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=81be4715

sci-mathematics/cvc4: PythonCompatUpdate

Signed-off-by: Alfredo Tupone  gentoo.org>

 sci-mathematics/cvc4/{cvc4-1.8-r4.ebuild => cvc4-1.8-r5.ebuild} | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.8-r4.ebuild 
b/sci-mathematics/cvc4/cvc4-1.8-r5.ebuild
similarity index 95%
rename from sci-mathematics/cvc4/cvc4-1.8-r4.ebuild
rename to sci-mathematics/cvc4/cvc4-1.8-r5.ebuild
index d62729a94aa8..6de0fc9372aa 100644
--- a/sci-mathematics/cvc4/cvc4-1.8-r4.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.8-r5.ebuild
@@ -1,10 +1,10 @@
-# Copyright 1999-2023 Gentoo Authors
+# Copyright 1999-2024 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=7
 
 CMAKE_MAKEFILE_GENERATOR=emake
-PYTHON_COMPAT=( python3_{9..11} )
+PYTHON_COMPAT=( python3_{9..12} )
 inherit cmake python-any-r1
 
 DESCRIPTION="Automatic theorem prover for satisfiability modulo theories (SMT) 
problems"

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/files/, sci-mathematics/cvc4/

2023-03-05 Thread Sam James 
commit: 978a74a61f2ca616c39051f9de4aab1214920bca
Author: Kai-Chun Ning  gmail  com>
AuthorDate: Sun Mar  5 10:53:54 2023 +
Commit: Sam James  gentoo  org>
CommitDate: Sun Mar  5 11:31:38 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=978a74a6

sci-mathematics/cvc4: fix build with bash 5.2

Closes: https://bugs.gentoo.org/883273
Signed-off-by: Kai-Chun Ning  gmail.com>
Closes: https://github.com/gentoo/gentoo/pull/29933
Signed-off-by: Sam James  gentoo.org>

 .../{cvc4-1.8-r3.ebuild => cvc4-1.8-r4.ebuild} |  1 +
 .../cvc4/files/cvc4-1.8-bash-5.2-fix.patch | 44 ++
 2 files changed, 45 insertions(+)

diff --git a/sci-mathematics/cvc4/cvc4-1.8-r3.ebuild 
b/sci-mathematics/cvc4/cvc4-1.8-r4.ebuild
similarity index 97%
rename from sci-mathematics/cvc4/cvc4-1.8-r3.ebuild
rename to sci-mathematics/cvc4/cvc4-1.8-r4.ebuild
index 276bdf289c12..d62729a94aa8 100644
--- a/sci-mathematics/cvc4/cvc4-1.8-r3.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.8-r4.ebuild
@@ -33,6 +33,7 @@ S="${WORKDIR}"/${PN^^}-archived-${PV}
 PATCHES=(
"${FILESDIR}"/${P}-gentoo.patch
"${FILESDIR}"/${P}-toml.patch
+   "${FILESDIR}"/${P}-bash-5.2-fix.patch
 )
 
 python_check_deps() {

diff --git a/sci-mathematics/cvc4/files/cvc4-1.8-bash-5.2-fix.patch 
b/sci-mathematics/cvc4/files/cvc4-1.8-bash-5.2-fix.patch
new file mode 100644
index ..54398da72555
--- /dev/null
+++ b/sci-mathematics/cvc4/files/cvc4-1.8-bash-5.2-fix.patch
@@ -0,0 +1,44 @@
+Description: Fix FTBFS with bash 5.2
+Author: Jerry James 
+Forwarded: no
+Last-Update: 2022-10-17
+Bug: https://bugs.gentoo.org/883273
+See: 
https://salsa.debian.org/science-team/cvc4/-/merge_requests/2/diffs?commit_id=05ca9eee24e279ddfbaebea7393b4303200141ad
+---
+
+diff --git a/src/expr/mkexpr b/src/expr/mkexpr
+index c5f12f487..642a7ff0d 100755
+--- a/src/expr/mkexpr
 b/src/expr/mkexpr
+@@ -16,6 +16,7 @@
+ #
+ 
+ copyright=2010-2014
++shopt -u patsub_replacement
+ 
+ filename=`basename "$1" | sed 's,_template,,'`
+ 
+diff --git a/src/expr/mkkind b/src/expr/mkkind
+index fbf37eff4..77a8fc7e5 100755
+--- a/src/expr/mkkind
 b/src/expr/mkkind
+@@ -15,6 +15,7 @@
+ #
+ 
+ copyright=2010-2014
++shopt -u patsub_replacement
+ 
+ filename=`basename "$1" | sed 's,_template,,'`
+ 
+diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
+index e2a733ec8..935040bed 100755
+--- a/src/expr/mkmetakind
 b/src/expr/mkmetakind
+@@ -18,6 +18,7 @@
+ #
+ 
+ copyright=2010-2014
++shopt -u patsub_replacement
+ 
+ cat <

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2023-02-22 Thread Alfredo Tupone 
commit: efd139384b4115a72399f8afe83890c8c021b6dc
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Wed Feb 22 11:25:04 2023 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Wed Feb 22 11:25:33 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=efd13938

sci-mathematics/cvc4: add support to python 3.11

Signed-off-by: Alfredo Tupone  gentoo.org>

 sci-mathematics/cvc4/{cvc4-1.8-r2.ebuild => cvc4-1.8-r3.ebuild} | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.8-r2.ebuild 
b/sci-mathematics/cvc4/cvc4-1.8-r3.ebuild
similarity index 97%
rename from sci-mathematics/cvc4/cvc4-1.8-r2.ebuild
rename to sci-mathematics/cvc4/cvc4-1.8-r3.ebuild
index 7f7a9ad7aa88..276bdf289c12 100644
--- a/sci-mathematics/cvc4/cvc4-1.8-r2.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.8-r3.ebuild
@@ -4,7 +4,7 @@
 EAPI=7
 
 CMAKE_MAKEFILE_GENERATOR=emake
-PYTHON_COMPAT=( python3_{9..10} )
+PYTHON_COMPAT=( python3_{9..11} )
 inherit cmake python-any-r1
 
 DESCRIPTION="Automatic theorem prover for satisfiability modulo theories (SMT) 
problems"

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/, sci-mathematics/cvc4/files/

2023-01-29 Thread Alfredo Tupone 
commit: b20b0dbffda6f89cf521ba6c714803d26054e177
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Sun Jan 29 13:11:43 2023 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Sun Jan 29 13:13:33 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=b20b0dbf

sci-mathematics/cvc4: drop 1.7-r1

Signed-off-by: Alfredo Tupone  gentoo.org>

 sci-mathematics/cvc4/Manifest|  1 -
 sci-mathematics/cvc4/cvc4-1.7-r1.ebuild  | 62 
 sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch | 43 
 sci-mathematics/cvc4/metadata.xml|  1 -
 4 files changed, 107 deletions(-)

diff --git a/sci-mathematics/cvc4/Manifest b/sci-mathematics/cvc4/Manifest
index fe5e434767b8..4326a842f502 100644
--- a/sci-mathematics/cvc4/Manifest
+++ b/sci-mathematics/cvc4/Manifest
@@ -1,2 +1 @@
-DIST cvc4-1.7.tar.gz 6969953 BLAKE2B 
3a64db14a734e0314fb7d7b8dbed79e067c9bbf1723343dac1e9c47b3f09811b1a32ff0116412667bd0afefda2489c6c1679bf109710402a67bee0d91b62dd94
 SHA512 
b91dfac7ddf979a3474f562eb98f2d6f17a53efa38c1be5502429309a0c059e1f2b0d85ee95e5aee17d35f34c825f01f879ec4aaf26025b1fcac835c33a867c6
 DIST cvc4-1.8.tar.gz 7554297 BLAKE2B 
f4d2b223ba2c01ef745520d8874381a1873358fbc7eca12559656512ffeefccec4eca3d73a26debf34110ca14a3bccf35ca87e2a49575b8b67484bed79df081c
 SHA512 
d6b0153b0f5c4e615c995a8eecfbfd783cfc1004c5134c6880230044081c71d638fee39cceb987eb8d72e91b2b6596b184dc0daacec8880cfc176c6dee8aa445

diff --git a/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild 
b/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild
deleted file mode 100644
index 340a8727e35b..
--- a/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild
+++ /dev/null
@@ -1,62 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-CMAKE_MAKEFILE_GENERATOR=emake
-PYTHON_COMPAT=( python3_{9..10} )
-inherit cmake python-any-r1
-
-DESCRIPTION="Automatic theorem prover for satisfiability modulo theories (SMT) 
problems"
-HOMEPAGE="https://cvc4.github.io/;
-SRC_URI="https://github.com/CVC4/CVC4/archive/${PV}.tar.gz -> ${P}.tar.gz"
-
-LICENSE="GPL-2"
-SLOT="0"
-KEYWORDS="~amd64 ~x86"
-IUSE="+cln proofs readline replay +statistics"
-
-RDEPEND="dev-libs/antlr-c
-   dev-java/antlr:3
-   dev-libs/boost
-   readline? ( sys-libs/readline:0= )
-   cln? ( sci-libs/cln )
-   !cln? ( dev-libs/gmp:= )"
-DEPEND="${RDEPEND}"
-BDEPEND="${PYTHON_DEPS}"
-
-S="${WORKDIR}"/${P^^}
-
-PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
-
-src_configure() {
-   local mycmakeargs=(
-   -DANTLR_BINARY=/usr/bin/antlr3
-   -DENABLE_GPL=ON
-   -DENABLE_OPTIMIZED=ON
-   -DUSE_CLN="$(usex cln ON OFF)"
-   -DUSE_READLINE="$(usex readline ON OFF)"
-   -DENABLE_STATISTICS="$(usex statistics ON OFF)"
-   -DENABLE_PROOFS="$(usex proofs ON OFF)"
-   -DENABLE_REPLAY="$(usex replay ON OFF)"
-   )
-   cmake_src_configure
-}
-
-src_test() {
-   emake -C "${BUILD_DIR}" \
-   examples \
-   boilerplate \
-   ouroborous \
-   reset_assertions \
-   sep_log_api \
-   smt2_compliance \
-   two_smt_engines \
-   statistics
-   cmake_src_test
-}
-
-src_install() {
-   cmake_src_install
-   mv "${D}"/usr/{lib,$(get_libdir)}
-}

diff --git a/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch 
b/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch
deleted file mode 100644
index 55331f6c39b8..
--- a/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch
+++ /dev/null
@@ -1,43 +0,0 @@
 a/CMakeLists.txt   2019-07-09 14:47:12.552425226 +0200
-+++ b/CMakeLists.txt   2019-07-09 14:50:02.595001358 +0200
-@@ -143,7 +143,7 @@
- 
- # Note: Module CodeCoverage requires the name of the debug build to conform
- #   to cmake standards (first letter uppercase).
--set(BUILD_TYPES Production Debug Testing Competition)
-+set(BUILD_TYPES Production Debug Testing Competition Gentoo)
- 
- if(ENABLE_ASAN)
- #_cmake_modify_IGNORE   set(CMAKE_BUILD_TYPE Debug)
-@@ -166,12 +166,10 @@
- endif()
- 
- message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
--include(Config${CMAKE_BUILD_TYPE})
- 
- 
#-#
- # Compiler flags
- 
--add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
- add_check_c_cxx_flag("-Wall")
- add_check_c_flag("-fexceptions")
- add_check_c_cxx_flag("-Wno-deprecated")
 a/test/regress/CMakeLists.txt  2019-07-14 09:49:38.429990489 +0200
-+++ b/test/regress/CMakeLists.txt  2019-07-14 09:50:28.854234838 +0200
-@@ -1810,7 +1810,7 @@
-   regress4/C880mul.miter.shuffled-as.sat03-348.smt
-   regress4/NEQ016_size5.smt
-   regress4/bug143.smt
--  regress4/comb2.shuffled-as.sat03-420.smt
-+  #regress4/comb2.shuffled-as.sat03-420.smt
-   regress4/hole10.cvc
-   regress4/instance_1151.smt
-

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2022-12-05 Thread Alfredo Tupone 
commit: 04828edf3713620506974d416284136cc7741923
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Mon Dec  5 13:32:33 2022 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Mon Dec  5 13:32:33 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=04828edf

sci-mathematics/cvc4: add github upstream metadata

Signed-off-by: Alfredo Tupone  gentoo.org>

 sci-mathematics/cvc4/metadata.xml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/sci-mathematics/cvc4/metadata.xml 
b/sci-mathematics/cvc4/metadata.xml
index 685032332723..012b2a3438e4 100644
--- a/sci-mathematics/cvc4/metadata.xml
+++ b/sci-mathematics/cvc4/metadata.xml
@@ -17,4 +17,7 @@
the validity (or, dually, the satisfiability) of first-order 
formulas
in a large number of built-in logical theories and their 
combination.

+   
+   CVC4/CVC4-archived
+

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/files/, sci-mathematics/cvc4/

2022-11-11 Thread Alfredo Tupone 
commit: ebdd2a9c7d597d29d1efa38f8bac6b3e68a8adb7
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Fri Nov 11 22:34:11 2022 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Fri Nov 11 22:34:41 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ebdd2a9c

sci-mathematics/cvc4: drop toml usage

Closes: https://bugs.gentoo.org/878679
Signed-off-by: Alfredo Tupone  gentoo.org>

 .../{cvc4-1.8-r1.ebuild => cvc4-1.8-r2.ebuild} |  9 +++--
 sci-mathematics/cvc4/files/cvc4-1.8-toml.patch | 46 ++
 2 files changed, 52 insertions(+), 3 deletions(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.8-r1.ebuild 
b/sci-mathematics/cvc4/cvc4-1.8-r2.ebuild
similarity index 87%
rename from sci-mathematics/cvc4/cvc4-1.8-r1.ebuild
rename to sci-mathematics/cvc4/cvc4-1.8-r2.ebuild
index c013d2a2ed33..5757f85d54c2 100644
--- a/sci-mathematics/cvc4/cvc4-1.8-r1.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.8-r2.ebuild
@@ -24,16 +24,19 @@ RDEPEND="dev-libs/antlr-c
!cln? ( dev-libs/gmp:= )"
 DEPEND="${RDEPEND}"
 BDEPEND="$(python_gen_any_dep '
-   dev-python/toml[${PYTHON_USEDEP}]
+   dev-python/tomli[${PYTHON_USEDEP}]
')
 "
 
 S="${WORKDIR}"/${PN^^}-archived-${PV}
 
-PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
+PATCHES=(
+   "${FILESDIR}"/${P}-gentoo.patch
+   "${FILESDIR}"/${P}-toml.patch
+)
 
 python_check_deps() {
-   python_has_version "dev-python/toml[${PYTHON_USEDEP}]"
+   python_has_version "dev-python/tomli[${PYTHON_USEDEP}]"
 }
 
 src_configure() {

diff --git a/sci-mathematics/cvc4/files/cvc4-1.8-toml.patch 
b/sci-mathematics/cvc4/files/cvc4-1.8-toml.patch
new file mode 100644
index ..f2ac73bf25c3
--- /dev/null
+++ b/sci-mathematics/cvc4/files/cvc4-1.8-toml.patch
@@ -0,0 +1,46 @@
+--- a/src/options/CMakeLists.txt   2022-11-11 23:12:59.874087267 +0100
 b/src/options/CMakeLists.txt   2022-11-11 23:13:11.974894643 +0100
+@@ -1,17 +1,3 @@
+-# Check if the toml Python module is installed.
+-execute_process(
+-  COMMAND
+-  ${PYTHON_EXECUTABLE} -c "import toml"
+-  RESULT_VARIABLE
+-RET_TOML
+-  ERROR_QUIET
+-)
+-
+-if(RET_TOML)
+-message(FATAL_ERROR
+-  "Could not find Python module toml. Install via `pip install toml'.")
+-endif()
+-
+ libcvc4_add_sources(
+   base_handlers.h
+   decision_weight.h
+--- a/src/options/mkoptions.py 2022-11-11 23:16:22.577858012 +0100
 b/src/options/mkoptions.py 2022-11-11 23:23:12.014320054 +0100
+@@ -46,7 +46,11 @@
+ import re
+ import sys
+ import textwrap
+-import toml
++
++if sys.version_info >= (3, 11):
++import tomllib
++else:
++import tomli as tomllib
+ 
+ ### Allowed attributes for module/option/alias
+ 
+@@ -1309,7 +1313,9 @@
+ # Parse files, check attributes and create module/option objects
+ modules = []
+ for filename in filenames:
+-module = parse_module(filename, toml.load(filename))
++with open(filename, "rb") as f:
++d1 = tomllib.load(f)
++module = parse_module(filename, d1)
+ 
+ # Check if long options are valid and unique.  First populate
+ # g_long_cache with option.long and --no- alternatives if

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2022-10-15 Thread Sam James 
commit: 2926d84a6e508609bd9eb5d2861c9ae46c1c0d3c
Author: Sam James  gentoo  org>
AuthorDate: Sat Oct 15 14:56:16 2022 +
Commit: Sam James  gentoo  org>
CommitDate: Sat Oct 15 14:56:16 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=2926d84a

sci-mathematics/cvc4: fix PythonHasVersionUsage

Signed-off-by: Sam James  gentoo.org>

 sci-mathematics/cvc4/cvc4-1.8-r1.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.8-r1.ebuild 
b/sci-mathematics/cvc4/cvc4-1.8-r1.ebuild
index ed74ecc20fba..c013d2a2ed33 100644
--- a/sci-mathematics/cvc4/cvc4-1.8-r1.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.8-r1.ebuild
@@ -33,7 +33,7 @@ S="${WORKDIR}"/${PN^^}-archived-${PV}
 PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
 
 python_check_deps() {
-   has_version "dev-python/toml[${PYTHON_USEDEP}]"
+   python_has_version "dev-python/toml[${PYTHON_USEDEP}]"
 }
 
 src_configure() {

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2022-08-26 Thread Sam James 
commit: 4a9afda7605ad144df0c1d23e966fdc8aeec1e34
Author: Petr Vaněk  atlas  cz>
AuthorDate: Thu Aug 25 21:41:00 2022 +
Commit: Sam James  gentoo  org>
CommitDate: Fri Aug 26 10:46:28 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=4a9afda7

sci-mathematics/cvc4: use  tag in metadata.xml

Signed-off-by: Petr Vaněk  atlas.cz>
Signed-off-by: Sam James  gentoo.org>

 sci-mathematics/cvc4/metadata.xml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/cvc4/metadata.xml 
b/sci-mathematics/cvc4/metadata.xml
index 42b2bfab2e1a..685032332723 100644
--- a/sci-mathematics/cvc4/metadata.xml
+++ b/sci-mathematics/cvc4/metadata.xml
@@ -6,7 +6,7 @@
Tupone Alfredo


-   Use sci-libs/cln
+   Use sci-libs/cln
Include statistics
Turn on the replay feature
Support for proof generation

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2022-02-17 Thread Alfredo Tupone 
commit: 25d067881ac71f918b69864739c6e7fabbf5d9a4
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Thu Feb 17 14:10:32 2022 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Thu Feb 17 14:10:32 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=25d06788

sci-mathematics/cvc4: fix deps check

Closes: https://bugs.gentoo.org/833362
Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone  gentoo.org>

 sci-mathematics/cvc4/cvc4-1.8-r1.ebuild | 9 ++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.8-r1.ebuild 
b/sci-mathematics/cvc4/cvc4-1.8-r1.ebuild
index d15cbba2d1f8..ed74ecc20fba 100644
--- a/sci-mathematics/cvc4/cvc4-1.8-r1.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.8-r1.ebuild
@@ -4,7 +4,7 @@
 EAPI=7
 
 CMAKE_MAKEFILE_GENERATOR=emake
-PYTHON_COMPAT=( python3_{7..10} )
+PYTHON_COMPAT=( python3_{8..10} )
 inherit cmake python-any-r1
 
 DESCRIPTION="Automatic theorem prover for satisfiability modulo theories (SMT) 
problems"
@@ -23,8 +23,7 @@ RDEPEND="dev-libs/antlr-c
cln? ( sci-libs/cln )
!cln? ( dev-libs/gmp:= )"
 DEPEND="${RDEPEND}"
-BDEPEND="${PYTHON_DEPS}
-   $(python_gen_any_dep '
+BDEPEND="$(python_gen_any_dep '
dev-python/toml[${PYTHON_USEDEP}]
')
 "
@@ -33,6 +32,10 @@ S="${WORKDIR}"/${PN^^}-archived-${PV}
 
 PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
 
+python_check_deps() {
+   has_version "dev-python/toml[${PYTHON_USEDEP}]"
+}
+
 src_configure() {
local mycmakeargs=(
-DANTLR_BINARY=/usr/bin/antlr3

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2022-02-08 Thread Sam James 
commit: 2ee65e4c7a1eaa5fe9ca21f260be762a1e36d370
Author: Sam James  gentoo  org>
AuthorDate: Wed Feb  9 01:37:43 2022 +
Commit: Sam James  gentoo  org>
CommitDate: Wed Feb  9 01:37:43 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=2ee65e4c

sci-mathematics/cvc4: revbump for CMake config file fix

This file is installed and embeds the libdir path which will affect
consumers trying to build against/detect cvc4.

See: 03321382501b45387f99917ba5acf9aa627805bd
Closes: https://bugs.gentoo.org/820515
Signed-off-by: Sam James  gentoo.org>

 sci-mathematics/cvc4/{cvc4-1.8.ebuild => cvc4-1.8-r1.ebuild} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.8.ebuild 
b/sci-mathematics/cvc4/cvc4-1.8-r1.ebuild
similarity index 100%
rename from sci-mathematics/cvc4/cvc4-1.8.ebuild
rename to sci-mathematics/cvc4/cvc4-1.8-r1.ebuild

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/files/

2022-02-08 Thread Alfredo Tupone 
commit: 03321382501b45387f99917ba5acf9aa627805bd
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Tue Feb  8 20:10:53 2022 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Tue Feb  8 20:10:53 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=03321382

sci-mathematics/cvc4: fix library path

Closes: https://bugs.gentoo.org/820515
Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone  gentoo.org>

 sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch | 9 +
 1 file changed, 9 insertions(+)

diff --git a/sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch 
b/sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch
index 372bea03fb72..64cf5bd771b2 100644
--- a/sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch
+++ b/sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch
@@ -1,5 +1,14 @@
 --- a/CMakeLists.txt   2019-07-09 14:47:12.552425226 +0200
 +++ b/CMakeLists.txt   2019-07-09 14:50:02.595001358 +0200
+@@ -83,7 +83,7 @@
+ 
#-#
+ 
+ set(INCLUDE_INSTALL_DIR include)
+-set(LIBRARY_INSTALL_DIR lib)
++set(LIBRARY_INSTALL_DIR ${CMAKE_INSTALL_LIBDIR})
+ set(RUNTIME_INSTALL_DIR bin)
+ 
+ 
#-#
 @@ -143,7 +143,7 @@
  
  # Note: Module CodeCoverage requires the name of the debug build to conform

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2022-02-08 Thread Alfredo Tupone 
commit: 222d7c3f5514f8cef25d7b119ebd97ff3a532ea1
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Tue Feb  8 08:56:11 2022 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Tue Feb  8 08:56:11 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=222d7c3f

sci-mathematics/cvc4: fix deps

Closes: https://bugs.gentoo.org/823023
Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone  gentoo.org>

 sci-mathematics/cvc4/cvc4-1.8.ebuild | 6 +-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.8.ebuild 
b/sci-mathematics/cvc4/cvc4-1.8.ebuild
index 879bf5675991..d15cbba2d1f8 100644
--- a/sci-mathematics/cvc4/cvc4-1.8.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.8.ebuild
@@ -23,7 +23,11 @@ RDEPEND="dev-libs/antlr-c
cln? ( sci-libs/cln )
!cln? ( dev-libs/gmp:= )"
 DEPEND="${RDEPEND}"
-BDEPEND="${PYTHON_DEPS}"
+BDEPEND="${PYTHON_DEPS}
+   $(python_gen_any_dep '
+   dev-python/toml[${PYTHON_USEDEP}]
+   ')
+"
 
 S="${WORKDIR}"/${PN^^}-archived-${PV}

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2022-02-07 Thread Alfredo Tupone 
commit: a67e2887fe1c15ec3bbabb3907ce352d1fd24803
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Tue Feb  8 07:44:06 2022 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Tue Feb  8 07:44:06 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=a67e2887

sci-mathematics/cvc4: remove unused CMake variables

Closes: https://bugs.gentoo.org/829088
Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone  gentoo.org>

 sci-mathematics/cvc4/cvc4-1.8.ebuild | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.8.ebuild 
b/sci-mathematics/cvc4/cvc4-1.8.ebuild
index 6eb40f393dc6..879bf5675991 100644
--- a/sci-mathematics/cvc4/cvc4-1.8.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.8.ebuild
@@ -14,7 +14,7 @@ 
SRC_URI="https://github.com/CVC4/CVC4-archived/archive/refs/tags/${PV}.tar.gz ->
 LICENSE="GPL-2"
 SLOT="0"
 KEYWORDS="~amd64 ~x86"
-IUSE="+cln proofs readline replay +statistics"
+IUSE="+cln proofs readline +statistics"
 
 RDEPEND="dev-libs/antlr-c
dev-java/antlr:3
@@ -33,12 +33,10 @@ src_configure() {
local mycmakeargs=(
-DANTLR_BINARY=/usr/bin/antlr3
-DENABLE_GPL=ON
-   -DENABLE_OPTIMIZED=ON
-DUSE_CLN="$(usex cln ON OFF)"
-DUSE_READLINE="$(usex readline ON OFF)"
-DENABLE_STATISTICS="$(usex statistics ON OFF)"
-DENABLE_PROOFS="$(usex proofs ON OFF)"
-   -DENABLE_REPLAY="$(usex replay ON OFF)"
)
cmake_src_configure
 }

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2022-02-05 Thread Alfredo Tupone 
commit: e137bda5f125920805b32c956f63726445bf41f9
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Sat Feb  5 11:21:55 2022 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Sat Feb  5 11:21:55 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=e137bda5

sci-mathematics/cvc4: PythonCompatUpdate

Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone  gentoo.org>

 sci-mathematics/cvc4/cvc4-1.7-r1.ebuild | 4 ++--
 sci-mathematics/cvc4/cvc4-1.8.ebuild| 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild 
b/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild
index 36e9f4689a67..a2f98aac04cc 100644
--- a/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild
@@ -1,10 +1,10 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=7
 
 CMAKE_MAKEFILE_GENERATOR=emake
-PYTHON_COMPAT=( python3_{7,8,9} )
+PYTHON_COMPAT=( python3_{7..10} )
 inherit cmake python-any-r1
 
 DESCRIPTION="Automatic theorem prover for satisfiability modulo theories (SMT) 
problems"

diff --git a/sci-mathematics/cvc4/cvc4-1.8.ebuild 
b/sci-mathematics/cvc4/cvc4-1.8.ebuild
index 347dbda0a248..6eb40f393dc6 100644
--- a/sci-mathematics/cvc4/cvc4-1.8.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.8.ebuild
@@ -1,10 +1,10 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=7
 
 CMAKE_MAKEFILE_GENERATOR=emake
-PYTHON_COMPAT=( python3_{7,8,9} )
+PYTHON_COMPAT=( python3_{7..10} )
 inherit cmake python-any-r1
 
 DESCRIPTION="Automatic theorem prover for satisfiability modulo theories (SMT) 
problems"

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/files/, sci-mathematics/cvc4/

2021-05-27 Thread Alfredo Tupone 
commit: f156562b157e5e59722065a39c5264413fcde2f1
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Thu May 27 16:45:43 2021 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Thu May 27 16:45:43 2021 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=f156562b

sci-mathematics/cvc4: version bump to 1.8

Package-Manager: Portage-3.0.18, Repoman-3.0.2
Signed-off-by: Alfredo Tupone  gentoo.org>

 sci-mathematics/cvc4/Manifest|  1 +
 sci-mathematics/cvc4/cvc4-1.8.ebuild | 55 
 sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch | 42 ++
 3 files changed, 98 insertions(+)

diff --git a/sci-mathematics/cvc4/Manifest b/sci-mathematics/cvc4/Manifest
index bf26cdb9e5e..fe5e434767b 100644
--- a/sci-mathematics/cvc4/Manifest
+++ b/sci-mathematics/cvc4/Manifest
@@ -1 +1,2 @@
 DIST cvc4-1.7.tar.gz 6969953 BLAKE2B 
3a64db14a734e0314fb7d7b8dbed79e067c9bbf1723343dac1e9c47b3f09811b1a32ff0116412667bd0afefda2489c6c1679bf109710402a67bee0d91b62dd94
 SHA512 
b91dfac7ddf979a3474f562eb98f2d6f17a53efa38c1be5502429309a0c059e1f2b0d85ee95e5aee17d35f34c825f01f879ec4aaf26025b1fcac835c33a867c6
+DIST cvc4-1.8.tar.gz 7554297 BLAKE2B 
f4d2b223ba2c01ef745520d8874381a1873358fbc7eca12559656512ffeefccec4eca3d73a26debf34110ca14a3bccf35ca87e2a49575b8b67484bed79df081c
 SHA512 
d6b0153b0f5c4e615c995a8eecfbfd783cfc1004c5134c6880230044081c71d638fee39cceb987eb8d72e91b2b6596b184dc0daacec8880cfc176c6dee8aa445

diff --git a/sci-mathematics/cvc4/cvc4-1.8.ebuild 
b/sci-mathematics/cvc4/cvc4-1.8.ebuild
new file mode 100644
index 000..347dbda0a24
--- /dev/null
+++ b/sci-mathematics/cvc4/cvc4-1.8.ebuild
@@ -0,0 +1,55 @@
+# Copyright 1999-2021 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+CMAKE_MAKEFILE_GENERATOR=emake
+PYTHON_COMPAT=( python3_{7,8,9} )
+inherit cmake python-any-r1
+
+DESCRIPTION="Automatic theorem prover for satisfiability modulo theories (SMT) 
problems"
+HOMEPAGE="https://cvc4.github.io/;
+SRC_URI="https://github.com/CVC4/CVC4-archived/archive/refs/tags/${PV}.tar.gz 
-> ${P}.tar.gz"
+
+LICENSE="GPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="+cln proofs readline replay +statistics"
+
+RDEPEND="dev-libs/antlr-c
+   dev-java/antlr:3
+   dev-libs/boost
+   readline? ( sys-libs/readline:0= )
+   cln? ( sci-libs/cln )
+   !cln? ( dev-libs/gmp:= )"
+DEPEND="${RDEPEND}"
+BDEPEND="${PYTHON_DEPS}"
+
+S="${WORKDIR}"/${PN^^}-archived-${PV}
+
+PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
+
+src_configure() {
+   local mycmakeargs=(
+   -DANTLR_BINARY=/usr/bin/antlr3
+   -DENABLE_GPL=ON
+   -DENABLE_OPTIMIZED=ON
+   -DUSE_CLN="$(usex cln ON OFF)"
+   -DUSE_READLINE="$(usex readline ON OFF)"
+   -DENABLE_STATISTICS="$(usex statistics ON OFF)"
+   -DENABLE_PROOFS="$(usex proofs ON OFF)"
+   -DENABLE_REPLAY="$(usex replay ON OFF)"
+   )
+   cmake_src_configure
+}
+
+src_test() {
+   emake -C "${BUILD_DIR}" \
+   systemtests
+   cmake_src_test
+}
+
+src_install() {
+   cmake_src_install
+   mv "${D}"/usr/{lib,$(get_libdir)}
+}

diff --git a/sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch 
b/sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch
new file mode 100644
index 000..372bea03fb7
--- /dev/null
+++ b/sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch
@@ -0,0 +1,42 @@
+--- a/CMakeLists.txt   2019-07-09 14:47:12.552425226 +0200
 b/CMakeLists.txt   2019-07-09 14:50:02.595001358 +0200
+@@ -143,7 +143,7 @@
+ 
+ # Note: Module CodeCoverage requires the name of the debug build to conform
+ #   to cmake standards (first letter uppercase).
+-set(BUILD_TYPES Production Debug Testing Competition)
++set(BUILD_TYPES Production Debug Testing Competition Gentoo)
+ 
+ if(ENABLE_ASAN)
+ #_cmake_modify_IGNORE   set(CMAKE_BUILD_TYPE Debug)
+@@ -166,12 +166,10 @@
+ endif()
+ 
+ message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
+-include(Config${CMAKE_BUILD_TYPE})
+ 
+ 
#-#
+ # Compiler flags
+ 
+-add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
+ add_check_c_cxx_flag("-Wall")
+ add_check_c_flag("-fexceptions")
+ add_check_c_cxx_flag("-Wno-deprecated")
+--- a/test/regress/CMakeLists.txt  2019-07-14 09:49:38.429990489 +0200
 b/test/regress/CMakeLists.txt  2019-07-14 09:50:28.854234838 +0200
+@@ -2155,7 +2155,6 @@
+   regress4/C880mul.miter.shuffled-as.sat03-348.smtv1.smt2
+   regress4/NEQ016_size5.smtv1.smt2
+   regress4/bug143.smtv1.smt2
+-  regress4/comb2.shuffled-as.sat03-420.smtv1.smt2
+   regress4/hole10.cvc
+   regress4/instance_1151.smtv1.smt2
+ )
+--- a/src/CMakeLists.txt   2019-07-18 08:56:47.923025745 +0200
 b/src/CMakeLists.txt   2019-07-18 08:58:10.584750385 +0200
+@@ -915,4 +915,4 @@
+ # Note: This is a temporary fix until the new C++ API

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2021-04-05 Thread Andreas Sturmlechner 
commit: b953b436445abffd13d9320514039055fe4eba04
Author: Andreas Sturmlechner  gentoo  org>
AuthorDate: Mon Apr  5 11:20:48 2021 +
Commit: Andreas Sturmlechner  gentoo  org>
CommitDate: Mon Apr  5 16:53:21 2021 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=b953b436

sci-mathematics/cvc4: python3_9, switch to cmake.eclass

Package-Manager: Portage-3.0.18, Repoman-3.0.3
Signed-off-by: Andreas Sturmlechner  gentoo.org>

 sci-mathematics/cvc4/cvc4-1.7-r1.ebuild | 19 +--
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild 
b/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild
index e50bae6113f..36e9f4689a6 100644
--- a/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild
@@ -3,12 +3,12 @@
 
 EAPI=7
 
-PYTHON_COMPAT=( python3_{7,8} )
+CMAKE_MAKEFILE_GENERATOR=emake
+PYTHON_COMPAT=( python3_{7,8,9} )
+inherit cmake python-any-r1
 
-inherit python-any-r1 cmake-utils
-
-DESCRIPTION="automatic theorem prover for satisfiability modulo theories (SMT) 
problems"
-HOMEPAGE="http://cvc4.cs.stanford.edu/web/;
+DESCRIPTION="Automatic theorem prover for satisfiability modulo theories (SMT) 
problems"
+HOMEPAGE="https://cvc4.github.io/;
 SRC_URI="https://github.com/CVC4/CVC4/archive/${PV}.tar.gz -> ${P}.tar.gz"
 
 LICENSE="GPL-2"
@@ -25,12 +25,11 @@ RDEPEND="dev-libs/antlr-c
 DEPEND="${RDEPEND}"
 BDEPEND="${PYTHON_DEPS}"
 
-S="${WORKDIR}"/CVC4-${PV}
+S="${WORKDIR}"/${P^^}
 
 PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
 
 src_configure() {
-   CMAKE_MAKEFILE_GENERATOR=emake
local mycmakeargs=(
-DANTLR_BINARY=/usr/bin/antlr3
-DENABLE_GPL=ON
@@ -41,7 +40,7 @@ src_configure() {
-DENABLE_PROOFS="$(usex proofs ON OFF)"
-DENABLE_REPLAY="$(usex replay ON OFF)"
)
-   cmake-utils_src_configure
+   cmake_src_configure
 }
 
 src_test() {
@@ -54,10 +53,10 @@ src_test() {
smt2_compliance \
two_smt_engines \
statistics
-   cmake-utils_src_test
+   cmake_src_test
 }
 
 src_install() {
-   cmake-utils_src_install
+   cmake_src_install
mv "${D}"/usr/{lib,$(get_libdir)}
 }

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2021-01-19 Thread Alfredo Tupone 
commit: 5e516f03a0f0543480601b545cadfa074c6051eb
Author: Alfredo Tupone  gentoo  org>
AuthorDate: Wed Jan 20 07:31:58 2021 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Wed Jan 20 07:31:58 2021 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=5e516f03

sci-mathematics/cvc4: add python dep

Closes: https://bugs.gentoo.org/766099
Package-Manager: Portage-3.0.12, Repoman-3.0.2
Signed-off-by: Alfredo Tupone  gentoo.org>

 sci-mathematics/cvc4/{cvc4-1.7.ebuild => cvc4-1.7-r1.ebuild} | 7 +--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.7.ebuild 
b/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild
similarity index 90%
rename from sci-mathematics/cvc4/cvc4-1.7.ebuild
rename to sci-mathematics/cvc4/cvc4-1.7-r1.ebuild
index 09aab161f76..a35698d4920 100644
--- a/sci-mathematics/cvc4/cvc4-1.7.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.7-r1.ebuild
@@ -1,9 +1,11 @@
-# Copyright 1999-2019 Gentoo Authors
+# Copyright 1999-2021 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=7
 
-inherit cmake-utils
+PYTHON_COMPAT=( python3_{6,7,8} )
+
+inherit python-any-r1 cmake-utils
 
 DESCRIPTION="automatic theorem prover for satisfiability modulo theories (SMT) 
problems"
 HOMEPAGE="http://cvc4.cs.stanford.edu/web/;
@@ -21,6 +23,7 @@ RDEPEND="dev-libs/antlr-c
cln? ( sci-libs/cln )
!cln? ( dev-libs/gmp:= )"
 DEPEND="${RDEPEND}"
+BDEPEND="${PYTHON_DEPS}"
 
 S="${WORKDIR}"/CVC4-${PV}

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2019-07-25 Thread Alfredo Tupone 
commit: f0be729b2f2055afe79f68cb95c9e856d0303e82
Author: Tupone Alfredo  gentoo  org>
AuthorDate: Thu Jul 25 06:12:57 2019 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Thu Jul 25 06:12:57 2019 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=f0be729b

sci-mathematics/cvc4: Add readline use flag

Closes: https://github.com/gentoo/gentoo/pull/12536
Signed-off-by: Alfredo Tupone  gentoo.org>
Package-Manager: Portage-2.3.66, Repoman-2.3.11

 sci-mathematics/cvc4/cvc4-1.7.ebuild | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.7.ebuild 
b/sci-mathematics/cvc4/cvc4-1.7.ebuild
index cc6e6eb4f4f..09aab161f76 100644
--- a/sci-mathematics/cvc4/cvc4-1.7.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.7.ebuild
@@ -12,11 +12,12 @@ SRC_URI="https://github.com/CVC4/CVC4/archive/${PV}.tar.gz 
-> ${P}.tar.gz"
 LICENSE="GPL-2"
 SLOT="0"
 KEYWORDS="~amd64 ~x86"
-IUSE="+cln +statistics proofs replay"
+IUSE="+cln proofs readline replay +statistics"
 
 RDEPEND="dev-libs/antlr-c
dev-java/antlr:3
dev-libs/boost
+   readline? ( sys-libs/readline:0= )
cln? ( sci-libs/cln )
!cln? ( dev-libs/gmp:= )"
 DEPEND="${RDEPEND}"
@@ -32,6 +33,7 @@ src_configure() {
-DENABLE_GPL=ON
-DENABLE_OPTIMIZED=ON
-DUSE_CLN="$(usex cln ON OFF)"
+   -DUSE_READLINE="$(usex readline ON OFF)"
-DENABLE_STATISTICS="$(usex statistics ON OFF)"
-DENABLE_PROOFS="$(usex proofs ON OFF)"
-DENABLE_REPLAY="$(usex replay ON OFF)"

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2019-07-23 Thread Alfredo Tupone 
commit: d72e9b862cbc9ccfabd0df7f53e7fe7664d22ae9
Author: Tupone Alfredo  gentoo  org>
AuthorDate: Tue Jul 23 13:20:29 2019 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Tue Jul 23 13:20:29 2019 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=d72e9b86

sci-mathematics/cvc4: add statistics, replay and proofs use flag

Closes: https://github.com/gentoo/gentoo/pull/12520
Signed-off-by: Alfredo Tupone  gentoo.org>
Package-Manager: Portage-2.3.66, Repoman-2.3.11

 sci-mathematics/cvc4/cvc4-1.7.ebuild | 6 +-
 sci-mathematics/cvc4/metadata.xml| 3 +++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/sci-mathematics/cvc4/cvc4-1.7.ebuild 
b/sci-mathematics/cvc4/cvc4-1.7.ebuild
index 0b192f12739..cc6e6eb4f4f 100644
--- a/sci-mathematics/cvc4/cvc4-1.7.ebuild
+++ b/sci-mathematics/cvc4/cvc4-1.7.ebuild
@@ -12,7 +12,7 @@ SRC_URI="https://github.com/CVC4/CVC4/archive/${PV}.tar.gz -> 
${P}.tar.gz"
 LICENSE="GPL-2"
 SLOT="0"
 KEYWORDS="~amd64 ~x86"
-IUSE="+cln"
+IUSE="+cln +statistics proofs replay"
 
 RDEPEND="dev-libs/antlr-c
dev-java/antlr:3
@@ -30,7 +30,11 @@ src_configure() {
local mycmakeargs=(
-DANTLR_BINARY=/usr/bin/antlr3
-DENABLE_GPL=ON
+   -DENABLE_OPTIMIZED=ON
-DUSE_CLN="$(usex cln ON OFF)"
+   -DENABLE_STATISTICS="$(usex statistics ON OFF)"
+   -DENABLE_PROOFS="$(usex proofs ON OFF)"
+   -DENABLE_REPLAY="$(usex replay ON OFF)"
)
cmake-utils_src_configure
 }

diff --git a/sci-mathematics/cvc4/metadata.xml 
b/sci-mathematics/cvc4/metadata.xml
index d1a299673f8..8ab072c9051 100644
--- a/sci-mathematics/cvc4/metadata.xml
+++ b/sci-mathematics/cvc4/metadata.xml
@@ -7,6 +7,9 @@


Use sci-libs/cln
+   Include statistics
+   Turn on the replay feature
+   Support for proof generation


CVC4 is an efficient open-source automatic theorem prover for

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/files/

2019-07-18 Thread Alfredo Tupone 
commit: 91f593d0b2dceda3acb4035fe501726f290e
Author: Tupone Alfredo  gentoo  org>
AuthorDate: Thu Jul 18 10:27:55 2019 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Thu Jul 18 10:27:55 2019 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=91f593d0

sci-mathematics/cvc4: Fix sandbox issue

Closes: https://bugs.gentoo.org/689918
Signed-off-by: Alfredo Tupone  gentoo.org>
Package-Manager: Portage-2.3.66, Repoman-2.3.11

 sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch | 8 
 1 file changed, 8 insertions(+)

diff --git a/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch 
b/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch
index 849b4a8a429..55331f6c39b 100644
--- a/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch
+++ b/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch
@@ -33,3 +33,11 @@
regress4/hole10.cvc
regress4/instance_1151.smt
  )
+--- a/src/CMakeLists.txt   2019-07-18 08:56:47.923025745 +0200
 b/src/CMakeLists.txt   2019-07-18 08:58:10.584750385 +0200
+@@ -915,4 +915,4 @@
+ # Note: This is a temporary fix until the new C++ API is in place.
+ install(CODE "execute_process(COMMAND
+ ${CMAKE_CURRENT_LIST_DIR}/fix-install-headers.sh
+-${CMAKE_INSTALL_PREFIX})")
++\$ENV{DESTDIR}${CMAKE_INSTALL_PREFIX})")

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/, sci-mathematics/cvc4/files/

2019-07-14 Thread Alfredo Tupone 
commit: 0165d1484b0c9ad0f2272960c80703e2c0b231f2
Author: Tupone Alfredo  gentoo  org>
AuthorDate: Sun Jul 14 19:48:18 2019 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Sun Jul 14 19:48:18 2019 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0165d148

sci-mathematics/cvc4: Bump to 1.7

Closes: https://bugs.gentoo.org/688652
Signed-off-by: Alfredo Tupone  gentoo.org>
Package-Manager: Portage-2.3.66, Repoman-2.3.11

 sci-mathematics/cvc4/Manifest|  1 +
 sci-mathematics/cvc4/cvc4-1.7.ebuild | 54 
 sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch | 35 +++
 3 files changed, 90 insertions(+)

diff --git a/sci-mathematics/cvc4/Manifest b/sci-mathematics/cvc4/Manifest
index 2b268f2188b..daaafcc4d44 100644
--- a/sci-mathematics/cvc4/Manifest
+++ b/sci-mathematics/cvc4/Manifest
@@ -1 +1,2 @@
 DIST cvc4-1.6.tar.gz 7815893 BLAKE2B 
626e0dd49f911384e64d7e8ecf635aa12dad32830b2032bdcb96afd1a17c3566f56df51f75e9193cf365b562855733d0ea4ff3311ac99fc86e928a956298d2ad
 SHA512 
0887b3f74a4b9e51e634591c7cf39d730110ca5d930149bab4816a49e383eeea8ccadf8474d22f5529cc03ddd045acacf8a2b92434b882adf352f4de4075fcd4
+DIST cvc4-1.7.tar.gz 6969953 BLAKE2B 
3a64db14a734e0314fb7d7b8dbed79e067c9bbf1723343dac1e9c47b3f09811b1a32ff0116412667bd0afefda2489c6c1679bf109710402a67bee0d91b62dd94
 SHA512 
b91dfac7ddf979a3474f562eb98f2d6f17a53efa38c1be5502429309a0c059e1f2b0d85ee95e5aee17d35f34c825f01f879ec4aaf26025b1fcac835c33a867c6

diff --git a/sci-mathematics/cvc4/cvc4-1.7.ebuild 
b/sci-mathematics/cvc4/cvc4-1.7.ebuild
new file mode 100644
index 000..0b192f12739
--- /dev/null
+++ b/sci-mathematics/cvc4/cvc4-1.7.ebuild
@@ -0,0 +1,54 @@
+# Copyright 1999-2019 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+inherit cmake-utils
+
+DESCRIPTION="automatic theorem prover for satisfiability modulo theories (SMT) 
problems"
+HOMEPAGE="http://cvc4.cs.stanford.edu/web/;
+SRC_URI="https://github.com/CVC4/CVC4/archive/${PV}.tar.gz -> ${P}.tar.gz"
+
+LICENSE="GPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="+cln"
+
+RDEPEND="dev-libs/antlr-c
+   dev-java/antlr:3
+   dev-libs/boost
+   cln? ( sci-libs/cln )
+   !cln? ( dev-libs/gmp:= )"
+DEPEND="${RDEPEND}"
+
+S="${WORKDIR}"/CVC4-${PV}
+
+PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
+
+src_configure() {
+   CMAKE_MAKEFILE_GENERATOR=emake
+   local mycmakeargs=(
+   -DANTLR_BINARY=/usr/bin/antlr3
+   -DENABLE_GPL=ON
+   -DUSE_CLN="$(usex cln ON OFF)"
+   )
+   cmake-utils_src_configure
+}
+
+src_test() {
+   emake -C "${BUILD_DIR}" \
+   examples \
+   boilerplate \
+   ouroborous \
+   reset_assertions \
+   sep_log_api \
+   smt2_compliance \
+   two_smt_engines \
+   statistics
+   cmake-utils_src_test
+}
+
+src_install() {
+   cmake-utils_src_install
+   mv "${D}"/usr/{lib,$(get_libdir)}
+}

diff --git a/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch 
b/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch
new file mode 100644
index 000..849b4a8a429
--- /dev/null
+++ b/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch
@@ -0,0 +1,35 @@
+--- a/CMakeLists.txt   2019-07-09 14:47:12.552425226 +0200
 b/CMakeLists.txt   2019-07-09 14:50:02.595001358 +0200
+@@ -143,7 +143,7 @@
+ 
+ # Note: Module CodeCoverage requires the name of the debug build to conform
+ #   to cmake standards (first letter uppercase).
+-set(BUILD_TYPES Production Debug Testing Competition)
++set(BUILD_TYPES Production Debug Testing Competition Gentoo)
+ 
+ if(ENABLE_ASAN)
+ #_cmake_modify_IGNORE   set(CMAKE_BUILD_TYPE Debug)
+@@ -166,12 +166,10 @@
+ endif()
+ 
+ message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
+-include(Config${CMAKE_BUILD_TYPE})
+ 
+ 
#-#
+ # Compiler flags
+ 
+-add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
+ add_check_c_cxx_flag("-Wall")
+ add_check_c_flag("-fexceptions")
+ add_check_c_cxx_flag("-Wno-deprecated")
+--- a/test/regress/CMakeLists.txt  2019-07-14 09:49:38.429990489 +0200
 b/test/regress/CMakeLists.txt  2019-07-14 09:50:28.854234838 +0200
+@@ -1810,7 +1810,7 @@
+   regress4/C880mul.miter.shuffled-as.sat03-348.smt
+   regress4/NEQ016_size5.smt
+   regress4/bug143.smt
+-  regress4/comb2.shuffled-as.sat03-420.smt
++  #regress4/comb2.shuffled-as.sat03-420.smt
+   regress4/hole10.cvc
+   regress4/instance_1151.smt
+ )

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/

2018-07-18 Thread Alfredo Tupone 
commit: ed51ccdb299c48d49d8750b05299431723016732
Author: Tupone Alfredo  gentoo  org>
AuthorDate: Wed Jul 18 06:28:48 2018 +
Commit: Alfredo Tupone  gentoo  org>
CommitDate: Wed Jul 18 06:28:48 2018 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ed51ccdb

sci-mathematics/cvc4: Add cvc4 to the tree

Package-Manager: Portage-2.3.40, Repoman-2.3.9

 sci-mathematics/cvc4/Manifest|  1 +
 sci-mathematics/cvc4/cvc4-1.6.ebuild | 24 
 sci-mathematics/cvc4/metadata.xml| 17 +
 3 files changed, 42 insertions(+)

diff --git a/sci-mathematics/cvc4/Manifest b/sci-mathematics/cvc4/Manifest
new file mode 100644
index 000..2b268f2188b
--- /dev/null
+++ b/sci-mathematics/cvc4/Manifest
@@ -0,0 +1 @@
+DIST cvc4-1.6.tar.gz 7815893 BLAKE2B 
626e0dd49f911384e64d7e8ecf635aa12dad32830b2032bdcb96afd1a17c3566f56df51f75e9193cf365b562855733d0ea4ff3311ac99fc86e928a956298d2ad
 SHA512 
0887b3f74a4b9e51e634591c7cf39d730110ca5d930149bab4816a49e383eeea8ccadf8474d22f5529cc03ddd045acacf8a2b92434b882adf352f4de4075fcd4

diff --git a/sci-mathematics/cvc4/cvc4-1.6.ebuild 
b/sci-mathematics/cvc4/cvc4-1.6.ebuild
new file mode 100644
index 000..1500f9d338d
--- /dev/null
+++ b/sci-mathematics/cvc4/cvc4-1.6.ebuild
@@ -0,0 +1,24 @@
+# Copyright 1999-2018 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=6
+
+DESCRIPTION="automatic theorem prover for satisfiability modulo theories (SMT) 
problems"
+HOMEPAGE="http://cvc4.cs.stanford.edu/web/;
+SRC_URI="http://cvc4.cs.stanford.edu/downloads/builds/src/${P}.tar.gz;
+
+LICENSE="GPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="+cln"
+
+RDEPEND="dev-libs/antlr-c
+   dev-libs/boost
+   cln? ( sci-libs/cln )
+   !cln? ( dev-libs/gmp:= )"
+DEPEND="${RDEPEND}"
+
+src_configure () {
+   econf --enable-gpl \
+   $(use_with cln)
+}

diff --git a/sci-mathematics/cvc4/metadata.xml 
b/sci-mathematics/cvc4/metadata.xml
new file mode 100644
index 000..d1a299673f8
--- /dev/null
+++ b/sci-mathematics/cvc4/metadata.xml
@@ -0,0 +1,17 @@
+
+http://www.gentoo.org/dtd/metadata.dtd;>
+
+   
+   tup...@gentoo.org
+   Tupone Alfredo
+   
+   
+   Use sci-libs/cln
+   
+   
+   CVC4 is an efficient open-source 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.
+   
+