gentoo auto-resync : 11:01:2023 - 05:43:34

19 files changed, 337 insertions, 8 deletions

diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index 3f0ad1f98c27..8406de39f580 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
diff --git a/sci-mathematics/boolector/Manifest b/sci-mathematics/boolector/Manifest
new file mode 100644
index 000000000000..01c7a42e9bbe
--- /dev/null
+++ b/sci-mathematics/boolector/Manifest
@@ -0,0 +1,3 @@
+DIST boolector-3.2.2_p20220110.tar.gz 1567668 BLAKE2B 6816f0434d88c790a27b9afe4c3b63c18a55b14f9f13b092f2940309e34842fe4868bf8d378bad130c4561d25e7d79b356fc27d9422bd42ba1b74ff98be36f72 SHA512 b1b964c155c8227e631025cf6bff69cf54728b1d875c2bd44a5a1ddb2857de2ab8fefc96d194faa5f98015e730b417d46a415ea601740e890df07ad5e50ad656
+EBUILD boolector-3.2.2_p20220110.ebuild 1791 BLAKE2B cf124ec570c488760e50384cb59131557fb5860729e7204ee84b3f123fe9a4a4ce79df946f4038bc018d25c635abe57ec8d29528e108e4ecb80705ad8beeb8fc SHA512 a8c0c27f80e29f5177bc1026f1598d86f12fd0142d983e8f65a064312d55234ab59213f658dcee9bb9345502201c64c3b813e48dea315471c6d23a0fec68868a
+MISC metadata.xml 1245 BLAKE2B a04e1e5a6af857100b8b569f57f4d2610593e9eb741513e4e6405a8fa9828471b92aaa1ad57a3163dc2f251b5664493692f92477b7191621ff8fd76eed9f57e7 SHA512 81257f7be3b21bf10caad654d5747ef2d978c0df5a05049b890420e2d170b7a4fa06151da0604a8b1b6e7daf2fb01344003c9243205a94b4040c580beb414836
diff --git a/sci-mathematics/boolector/boolector-3.2.2_p20220110.ebuild b/sci-mathematics/boolector/boolector-3.2.2_p20220110.ebuild
new file mode 100644
index 000000000000..289c5358a5b9
--- /dev/null
+++ b/sci-mathematics/boolector/boolector-3.2.2_p20220110.ebuild
@@ -0,0 +1,77 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+H=13a8a06d561041cafcaf5458e404c1ec354b2841
+PYTHON_COMPAT=( python3_{8..11} )
+
+inherit python-single-r1 cmake
+
+DESCRIPTION="Fast SMT solver for bit-vectors, arrays and uninterpreted functions"
+HOMEPAGE="https://boolector.github.io/
+	https://github.com/Boolector/boolector/"
+
+if [[ "${PV}" == *9999* ]] ; then
+	inherit git-r3
+	EGIT_REPO_URI="https://github.com/Boolector/${PN}.git"
+else
+	SRC_URI="https://github.com/Boolector/${PN}/archive/${H}.tar.gz
+		-> ${P}.tar.gz"
+	S="${WORKDIR}"/${PN}-${H}
+	KEYWORDS="~amd64 ~x86"
+fi
+
+LICENSE="MIT"
+SLOT="0"
+IUSE="cryptominisat examples +gmp minisat +picosat python test"
+REQUIRED_USE="
+	python? ( ${PYTHON_REQUIRED_USE} )
+	|| ( cryptominisat minisat picosat )
+"
+RESTRICT="!test? ( test )"
+
+RDEPEND="
+	sci-mathematics/btor2tools:=
+	cryptominisat? ( sci-mathematics/cryptominisat:= )
+	gmp? ( dev-libs/gmp:= )
+	minisat? ( sci-mathematics/minisat:= )
+	picosat? ( sci-mathematics/picosat:= )
+	python? ( ${PYTHON_DEPS} )
+"
+DEPEND="${RDEPEND}"
+BDEPEND="test? ( dev-cpp/gtest )"
+
+pkg_setup() {
+	use python && python-single-r1_pkg_setup
+}
+
+src_configure() {
+	local mycmakeargs=(
+		-DBUILD_SHARED_LIBS=ON
+		-DUSE_PYTHON2=OFF
+		-DPYTHON=$(usex python)
+		-DTESTING=$(usex test)
+		-DUSE_GMP=$(usex gmp)
+		-DUSE_PYTHON3=$(usex python)
+
+		# Integration with other SMT solvers
+		-DUSE_LINGELING=OFF  # Not packaged yet.
+		-DUSE_CADICAL=OFF  # Fails to link.
+		-DUSE_CMS=$(usex cryptominisat)
+		-DUSE_MINISAT=$(usex minisat)
+		-DUSE_PICOSAT=$(usex picosat)
+	)
+	cmake_src_configure
+}
+
+src_install() {
+	cmake_src_install
+
+	dodir /usr/$(get_libdir)
+	mv "${ED}"/usr/lib/*.so "${ED}"/usr/$(get_libdir)/ || die
+
+	if use examples ; then
+		dodoc -r examples
+	fi
+}
diff --git a/sci-mathematics/boolector/metadata.xml b/sci-mathematics/boolector/metadata.xml
new file mode 100644
index 000000000000..b61474ce8353
--- /dev/null
+++ b/sci-mathematics/boolector/metadata.xml
@@ -0,0 +1,32 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</email>
+    <name>Gentoo Mathematics Project</name>
+  </maintainer>
+  <longdescription>
+    Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories
+    of fixed-size bit-vectors, arrays and uninterpreted functions. It supports
+    the SMT-LIB logics BV, QF_ABV, QF_AUFBV, QF_BV and QF_UFBV. Boolector
+    provides a rich C and Python API and supports incremental solving, both
+    with the SMT-LIB commands push and pop, and as solving under assumptions.
+  </longdescription>
+  <use>
+    <flag name="cryptominisat">
+      Enable support for <pkg>sci-mathematics/cryptominisat</pkg>
+    </flag>
+    <flag name="minisat">
+      Enable support for <pkg>sci-mathematics/minisat</pkg>
+    </flag>
+    <flag name="picosat">
+      Enable support for <pkg>sci-mathematics/picosat</pkg>
+    </flag>
+  </use>
+  <upstream>
+    <bugs-to>https://github.com/Boolector/boolector/issues/</bugs-to>
+    <doc>https://boolector.github.io/docs/index.html</doc>
+    <remote-id type="github">Boolector/boolector</remote-id>
+  </upstream>
+</pkgmetadata>
diff --git a/sci-mathematics/btor2tools/Manifest b/sci-mathematics/btor2tools/Manifest
new file mode 100644
index 000000000000..a6f98fe33e62
--- /dev/null
+++ b/sci-mathematics/btor2tools/Manifest
@@ -0,0 +1,5 @@
+AUX btor2tools-1.0.0_pre20220518-cmake-also-static.patch 804 BLAKE2B bdfb9e99a98f9cd9989ba0eb10490877b24553c5db478281c8771bb922060c20412521dbab513e5742daa4878189313cae075d044b4ba4ee8f265bde15aef520 SHA512 ac03a333bd0563559b940d4b4b0f2e5da4440503e5ec84b0a28ddb4c4b5a17cf96910c025abe088f93dc82147023cfaa598eb18a6aa409e690baffe0166d10d6
+AUX btor2tools-1.0.0_pre20220518-cmake-clfags.patch 551 BLAKE2B 8cc8c427a2ec7defc4bd7f251b2a2a6484bc321b0f0d88a7099e8a69963cfbf6b69d13dbce4f54874d8138ec01ae870752a947a01c93c3cf996456c546ce012e SHA512 a6c446440405ab44b9bffb8316d170782241d77334c5837820ee0ea1e6da5ff97121b966a49af9c15e8e0e2a184ae3781166eb9c0ba07c4319dd92fed105ae2d
+DIST btor2tools-1.0.0_pre20220518.tar.gz 87420 BLAKE2B df8ddc8f286c32c580a8feaf0c7e90dff113d2b0303e3da0a378f2906cd34134ea91707cd40c95c38782990bf4d815416b3a566680f4d6668ddca46321ae530a SHA512 96e17327de311b3d16e086031038a8248431d0dda75b83ce137d6526a096b69fc062290f92ec5b58fffb56aa25437835f97a96bd15f0044d4d52263bf386d928
+EBUILD btor2tools-1.0.0_pre20220518.ebuild 783 BLAKE2B a911486c6340478d3c00421c77f8f4eca47e442cae1fd0df8c048e5ea27065c219ec58af95618eba7b837b4ee20b250746a92d0d915a66a1f01b1287feabed62 SHA512 2bb3a28dd080ffd68f8e37c92a58a12ac1f19a2864e116d4c66d46e2e793d733fe1d9fdfc2539c1c3c108f6590cb4bb0564c009d8b0b854c7f43bb1e0f644f7e
+MISC metadata.xml 437 BLAKE2B 93f1e3a98b8dd3edd95de3bd8f830427a9e05dcfc73690899ed16ec49be25bfd524d86fcaa9735d15c22515b98d13ded8a95c7a39e4970e3035c72e4cbe7d544 SHA512 39b7bd39e597f6d3086358738cb2d668f0317af3a8674eb4c032f59c64de0ceada799900bd193f244f049f51e1a91dcd9bb4474db39ac88967086206f3090a62
diff --git a/sci-mathematics/btor2tools/btor2tools-1.0.0_pre20220518.ebuild b/sci-mathematics/btor2tools/btor2tools-1.0.0_pre20220518.ebuild
new file mode 100644
index 000000000000..efade1283737
--- /dev/null
+++ b/sci-mathematics/btor2tools/btor2tools-1.0.0_pre20220518.ebuild
@@ -0,0 +1,39 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+H=b8456dda4780789e882f5791eb486f295ade4da4
+
+inherit cmake
+
+DESCRIPTION="Generic parser and tools for the BTOR2 format"
+HOMEPAGE="https://github.com/Boolector/btor2tools/"
+
+if [[ "${PV}" == *9999* ]] ; then
+	inherit git-r3
+	EGIT_REPO_URI="https://github.com/Boolector/${PN}.git"
+else
+	SRC_URI="https://github.com/Boolector/${PN}/archive/${H}.tar.gz
+		-> ${P}.tar.gz"
+	S="${WORKDIR}"/${PN}-${H}
+	KEYWORDS="~amd64 ~x86"
+fi
+
+LICENSE="MIT"
+SLOT="0"
+IUSE="examples"
+
+PATCHES=(
+	"${FILESDIR}"/${P}-cmake-also-static.patch
+	"${FILESDIR}"/${P}-cmake-clfags.patch
+)
+
+src_install() {
+	cmake_src_install
+
+	if use examples ; then
+		insinto /usr/share/${PN}
+		dodoc -r examples
+	fi
+}
diff --git a/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-also-static.patch b/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-also-static.patch
new file mode 100644
index 000000000000..061ddac84194
--- /dev/null
+++ b/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-also-static.patch
@@ -0,0 +1,28 @@
+--- a/src/CMakeLists.txt
++++ b/src/CMakeLists.txt
+@@ -1,4 +1,5 @@
+ add_library(btor2parser
++  SHARED
+   btor2parser/btor2parser.c
+ )
+ target_include_directories(btor2parser PRIVATE .)
+@@ -10,6 +11,19 @@ install(
+   PUBLIC_HEADER DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}
+ )
+ 
++add_library(btor2parser_static
++  STATIC
++  btor2parser/btor2parser.c
++)
++target_include_directories(btor2parser_static PRIVATE .)
++set_target_properties(btor2parser_static PROPERTIES OUTPUT_NAME btor2parser)
++set_target_properties(btor2parser_static PROPERTIES PUBLIC_HEADER btor2parser/btor2parser.h)
++install(
++  TARGETS btor2parser_static
++  ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}
++  PUBLIC_HEADER DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}
++)
++
+ add_executable(btorsim
+   btorsim/btorsimam.cpp
+   btorsim/btorsimstate.cpp
diff --git a/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-clfags.patch b/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-clfags.patch
new file mode 100644
index 000000000000..84c6631c9219
--- /dev/null
+++ b/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-clfags.patch
@@ -0,0 +1,19 @@
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -91,16 +91,6 @@ add_check_c_cxx_flag("-Wredundant-decls")
+ add_check_c_flag("-std=gnu99")
+ add_required_cxx_flag("-std=gnu++11")
+ 
+-if(CMAKE_BUILD_TYPE STREQUAL "Debug")
+-  add_check_c_cxx_flag("-g3")
+-  add_check_c_cxx_flag("-ggdb")
+-else()
+-  add_check_c_cxx_flag("-O3")
+-  if(NOT CHECK)
+-    add_check_c_cxx_flag("-DNDEBUG")
+-  endif()
+-endif()
+-
+ if(ASAN)
+   # -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set,
+   # otherwise the -fsanitize=address check will fail while linking.
diff --git a/sci-mathematics/btor2tools/metadata.xml b/sci-mathematics/btor2tools/metadata.xml
new file mode 100644
index 000000000000..237d97fb7791
--- /dev/null
+++ b/sci-mathematics/btor2tools/metadata.xml
@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</email>
+    <name>Gentoo Mathematics Project</name>
+  </maintainer>
+  <upstream>
+    <bugs-to>https://github.com/Boolector/btor2tools/issues/</bugs-to>
+    <remote-id type="github">Boolector/btor2tools</remote-id>
+  </upstream>
+</pkgmetadata>
diff --git a/sci-mathematics/cadical/Manifest b/sci-mathematics/cadical/Manifest
index 1fbc26daa231..67a34a024cd4 100644
--- a/sci-mathematics/cadical/Manifest
+++ b/sci-mathematics/cadical/Manifest
@@ -3,5 +3,5 @@ AUX cadical-makefile.in-ar.patch 323 BLAKE2B 226618745824824d8d7ccea53a3435abed9
 DIST cadical-1.5.2.tar.gz 596334 BLAKE2B 2e6c0f0602b807cf9ee5993aa627e074291b0128d19474d5431e01992d66b111773e593c14712338e9702f64e23eae6fdd937b5b86b2b9b3e08022dbbb199fd7 SHA512 1aab87bdaec938eb219f75f13bf2fcb031f47ac1f49b586f769aeececd1c33b166341bef3bc8713e62b4612a91c405db33e6d1b48e1074a3433d80e9ecb33fe2
 DIST cadical-1.5.3.tar.gz 596378 BLAKE2B 1ac27412745b0f24668ccf2ea1ff89e02c1e68137110bf9522a63ad82b14621d898d0bf873a651a24ccef9f502982f5e2d5b9c558ed0b1c5b7432c1a1459cb58 SHA512 bec811ab6a4c392506bdc391227d108476b5b5fae280b2d7d484429fe6d84e86206a054a1044cf68046ce183ecd7af3ec58f8be3ac27224fe37930cf43f08f3b
 EBUILD cadical-1.5.2-r1.ebuild 732 BLAKE2B f97142135bf5be3f3912d572235aa0de953ac4137e715b0b3732014c19527cb2a6a4fca456bdd5e48b9384038b1028fcaef8b47695ead65bff5ebdd17fc1d3ce SHA512 aed6e5bd0cda217c6b2a1c9a32dc27f0b0c5f051dcbf43a3e06e806e5a6099340a8d224027b77e6949b3ca3f053f1cd1676cf968d95c9a63636bbe18703e7f79
-EBUILD cadical-1.5.3.ebuild 787 BLAKE2B b4303e9b1636eabd5697e1dcf2111182ca297c7b7d76a64eddf03acef1dd9e3ce569cf1907282cb8511d74a54d4372f5fd67d1d8f1f2f9430fbb9ecb13d9cb70 SHA512 bb7d45d98a46b0a61ce0174a9d287c2fdd425dad7da90fd0f8c963aaf53cdd0aa8b617a9a7ae1ff817a44b39ea2e4ff951d17539dcc5958ad20cd5e24f60d929
+EBUILD cadical-1.5.3-r1.ebuild 813 BLAKE2B 028ee0555334e9f2a4e3a4c90cac3d85644592c69f5d44392212c941889ad24bb7e9b1f7bbe5a67e6efd370d1f9832300da57b16543c30d17e32786925c774b8 SHA512 1dc7b61c695804ae6348ff35b4047b9ad2bb26f3a63906d661dcf87b4e0a4ff5127228c9694d46377517ec2c27d04f2173a5f9e3f8582349e1b8662ff2f1cab6
 MISC metadata.xml 613 BLAKE2B 6d7e0c1b5eae3803aa0981b195457cdcc6d2ffa2af655837e615da6ed6914ac5bec7a831ced6703ff67476561cf67139ea5519d98cdc2bd8d5781108496046e2 SHA512 b04ad6ae6e2626cea18049e3e20eb227b5580853b8ad77179ea693ed61f12d042b7ea505eb8cfafaa0121564ab0a4b6c7dcdf84f78fa2f47c465e6f61fb1a3f0
diff --git a/sci-mathematics/cadical/cadical-1.5.3.ebuild b/sci-mathematics/cadical/cadical-1.5.3-r1.ebuild
index dac39982db2e..63bd3bf453f3 100644
--- a/sci-mathematics/cadical/cadical-1.5.3.ebuild
+++ b/sci-mathematics/cadical/cadical-1.5.3-r1.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=8
@@ -7,7 +7,8 @@ inherit toolchain-funcs
 
 DESCRIPTION="Simplified Satisfiability Solver"
 HOMEPAGE="http://fmv.jku.at/cadical/"
-SRC_URI="https://github.com/arminbiere/${PN}/archive/rel-${PV}.tar.gz -> ${P}.tar.gz"
+SRC_URI="https://github.com/arminbiere/${PN}/archive/rel-${PV}.tar.gz
+	-> ${P}.tar.gz"
 S="${WORKDIR}"/${PN}-rel-${PV}
 
 LICENSE="MIT"
@@ -31,5 +32,6 @@ src_install() {
 	doexe build/{cadical,mobical}
 	dolib.a build/libcadical.a
 	doheader src/cadical.hpp
+	doheader src/ccadical.h
 	einstalldocs
 }
diff --git a/sci-mathematics/cubicle/Manifest b/sci-mathematics/cubicle/Manifest
new file mode 100644
index 000000000000..aa9a2c6b901b
--- /dev/null
+++ b/sci-mathematics/cubicle/Manifest
@@ -0,0 +1,4 @@
+AUX 50cubicle-gentoo.el 185 BLAKE2B 76ef002c52bd0d6ef8ce5474e5cf9032cffe861d273a88176c3a8eae17f6176896bc1a4cb099d1f793b63f1ad3e0b7fb6d4b066317f160a0a4fd586e0a61ec64 SHA512 c9a93fec3f1f12cbe326940a79dfe950b56c82e7bdd24a6bf5923d1c4fe6245b8fec4c399f3e60c16cc4757f290f9cbeab606a20b5844f4228a4f29b0ed669f4
+DIST cubicle-1.2.0.tar.gz 866004 BLAKE2B 4fd944acb394165396344b7a9d4b29ffcb7b61571e1ac9cb90aacf1a5ddb0521d399f301a51af6b37461e5a47244fb095ad69ab0041440c240257522ba4de4a7 SHA512 e2815b4b7b4feda30df91eabebae741d14a2c822f5efea972676bc7a941454ea368e9dc003f754c2edb1c6b1db5a5c86a354b3612c2d47a9095f8fc348dfb692
+EBUILD cubicle-1.2.0-r1.ebuild 1332 BLAKE2B 7dbbb9ed042dd4ecabb00ee3ccc050e39174b01e7131f90b6bbd5dde249299071e30eee3f2cfd5576f8504b7a3f27ab1430428935b4012e0da69c8cbc67409b7 SHA512 a9018679ffa0b2481fd3629518317e8ceab2494d66d1688e1a95ff41b73964a62f17b4d2c6e2ad17e130c09e93b84bb1d23f360e5eebdb8f6f87f154a4069f9d
+MISC metadata.xml 1503 BLAKE2B d67f3f6524234cf3be4b0118aced6f4e3424a25754d91b13eb5c8250aedb6a57a6f7faabe6539875953874f48b2d8349fe3adfe431b72675fdd6723cb9ff3c52 SHA512 96540a56c6ef839924fa93f49e4ffdeb8a5eb3b83ef43bd62ccbed72dfa522f1b0acad4132650f67387915af5be8fe432fd6d01f8c9a76271c53f7f3a33f476d
diff --git a/sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild b/sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild
new file mode 100644
index 000000000000..8159f9f60a4a
--- /dev/null
+++ b/sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild
@@ -0,0 +1,71 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit autotools elisp-common
+
+DESCRIPTION="Model checker for verifying properties of array-based systems"
+HOMEPAGE="https://cubicle.lri.fr/
+	https://github.com/cubicle-model-checker/cubicle/"
+SRC_URI="https://github.com/cubicle-model-checker/${PN}/archive/${PV}.tar.gz
+	 -> ${P}.tar.gz"
+
+LICENSE="Apache-2.0"
+SLOT="0/${PV}"
+KEYWORDS="~amd64 ~x86"
+IUSE="emacs examples ocamlopt"
+
+RDEPEND="
+	>=dev-lang/ocaml-4.09.0:=[ocamlopt=]
+	dev-ml/num:=
+	emacs? ( >=app-editors/emacs-23.1:* )
+"
+DEPEND="${RDEPEND}"
+BDEPEND="
+	dev-ml/findlib
+	sys-apps/gawk
+"
+
+SITEFILE="50${PN}-gentoo.el"
+
+src_prepare() {
+	default
+	eautoreconf
+
+	# Makefile checks if "configure.in" exists,
+	#   it is needed by the ".depend" target.
+	ln -s configure.ac configure.in || die
+}
+
+src_configure() {
+	econf --without-z3  # Needs Z3 Ocaml bindings, not yet packaged.
+}
+
+src_compile() {
+	default
+
+	if use emacs ; then
+	   elisp-compile emacs/*.el
+	fi
+}
+
+src_install() {
+	default
+
+	doman doc/${PN}.1
+
+	if use emacs ; then
+	   elisp-install ${PN} emacs/*.el{,c}
+	   elisp-site-file-install "${FILESDIR}/${SITEFILE}"
+	fi
+	use examples && dodoc -r examples
+}
+
+pkg_postinst() {
+	use emacs && elisp-site-regen
+}
+
+pkg_postrm() {
+	use emacs && elisp-site-regen
+}
diff --git a/sci-mathematics/cubicle/files/50cubicle-gentoo.el b/sci-mathematics/cubicle/files/50cubicle-gentoo.el
new file mode 100644
index 000000000000..bab0f0d76325
--- /dev/null
+++ b/sci-mathematics/cubicle/files/50cubicle-gentoo.el
@@ -0,0 +1,4 @@
+(add-to-list 'load-path "@SITELISP@")
+(autoload 'cubicle-mode "cubicle-mode"
+  "A major mode for editing Cubicle files." t)
+(add-to-list 'auto-mode-alist '("\\.cub\\'" . cubicle-mode))
diff --git a/sci-mathematics/cubicle/metadata.xml b/sci-mathematics/cubicle/metadata.xml
new file mode 100644
index 000000000000..d3a0058bc0c9
--- /dev/null
+++ b/sci-mathematics/cubicle/metadata.xml
@@ -0,0 +1,31 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <maintainer type="project">
+    <email>ml@gentoo.org</email>
+    <name>ML</name>
+  </maintainer>
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</email>
+    <name>Gentoo Mathematics Project</name>
+  </maintainer>
+  <longdescription>
+    Cubicle is an open source model checker for verifying safety properties of
+    array-based systems. This is a syntactically restricted class of
+    parametrized transition systems with states represented as arrays indexed
+    by an arbitrary number of processes. Cache coherence protocols and mutual
+    exclusion algorithms are typical examples of such systems. Cubicle
+    model-checks by a symbolic backward reachability analysis on infinite sets
+    of states represented by specific simple formulas, called cubes. Cubicle is
+    based on ideas introduced by MCMT from which, in addition to revealing the
+    implementation details, it differs in a more friendly input language and a
+    concurrent architecture. Cubicle is written in OCaml. Its SMT solver is a
+    tightly integrated, lightweight and enhanced version of Alt-Ergo; and its
+    parallel implementation relies on the Functory library.
+  </longdescription>
+  <upstream>
+    <bugs-to>https://github.com/cubicle-model-checker/cubicle/issues/</bugs-to>
+    <remote-id type="github">cubicle-model-checker/cubicle</remote-id>
+  </upstream>
+</pkgmetadata>
diff --git a/sci-mathematics/picosat/Manifest b/sci-mathematics/picosat/Manifest
index d2426840a5b1..cbf04723294e 100644
--- a/sci-mathematics/picosat/Manifest
+++ b/sci-mathematics/picosat/Manifest
@@ -1,4 +1,4 @@
 AUX picosat-965-makefile.in.patch 364 BLAKE2B fd6d9ade8e918dd8c9a16ced81a8f47a6ba2b64c7b262a385b0637092beaac4adcc0886506b49c5b21131a550f332b170bc4cc456696d99b7404aa8c11d37018 SHA512 950bddde2363c5b0e36c2333201fbfee54229674f9051f3c4f45023f4364a3bdca3cdaf6b083eed7c9a59c4de0ab92c0eb748092c6cba4c9dba5da6146d6b90f
 DIST picosat-965.tar.gz 64386 BLAKE2B 913b08a72c0b15065353c2ee1ff8fe5a9c0f7a2a8653d80f4cdcee8fdcf69eed7621e28f4259a9d0fb506fefb8eccfd293f06aa7c1b3ea3f6cc31eb319a30532 SHA512 b5372962a0079d70641fd76c431b4ab5042c2f3015179762e447634f220cf0744eea786ee40b00035a342f3ead482061ebe1a9e3726bd06e7adf8e0ac0c5eabf
-EBUILD picosat-965.ebuild 756 BLAKE2B e9f78bc57ecb6098b4adf42604c953d7ceff70d50c5cb6c2050efc6c7bed971f831c48a037b79411d501b9d6c63b6f12020b63ae0968b7cc219261b128bf9d47 SHA512 a567120a954bd949c3550bf765187624b6403befef00f5d1b4fa98a45b1f51f7159d2c8d1e366d38898651cec0600e5759e43988a5365eb70b4363bb87336199
+EBUILD picosat-965-r1.ebuild 778 BLAKE2B 1bbc097e9d473e4f7924ecf9a867481c6d3b845e8386e6d5bebbf2c761b7d985f077ac12e6b5b0b50e761daa6be9be1c1d8ede80e9d16ecf795e333e1988cd49 SHA512 9d446c871c701798b8b5cff7261bd817103775968fe885293112d782e135b94f2cbaa4e41307bc0379916d52a1618ad6303daadd47c6a7c6c6e2ab16657bdba1
 MISC metadata.xml 277 BLAKE2B 3d5dbdb3275e5d5623299c686ddb7ce896215621e87d688814bc03d383eeec180594639627ed7b8ac903fba49120507407c9e53813401c797c67a2da8330ef02 SHA512 f7b11642db7488b1cc11d3a5602fc18985a0e050502a332ed6850e123c51d3cad21790c09e032454c7590b61d4718cd91bde453c1ec00baaedea90ee9f57882c
diff --git a/sci-mathematics/picosat/picosat-965.ebuild b/sci-mathematics/picosat/picosat-965-r1.ebuild
index 9803703a619b..30e893f62288 100644
--- a/sci-mathematics/picosat/picosat-965.ebuild
+++ b/sci-mathematics/picosat/picosat-965-r1.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=8
@@ -31,6 +31,7 @@ src_install() {
 	insinto /usr/share
 	newins VERSION picosat.version
 
+	dolib.a libpicosat.a
 	dolib.so libpicosat.so
 	doheader picosat.h
 
diff --git a/sci-mathematics/singular/Manifest b/sci-mathematics/singular/Manifest
index e08a451c39ba..29648303b20d 100644
--- a/sci-mathematics/singular/Manifest
+++ b/sci-mathematics/singular/Manifest
@@ -1,6 +1,6 @@
 AUX 60singular-gentoo.el 298 BLAKE2B 5b42e2083037e2ff2ace5597ddebfb079920e09ed91d1a359e058fc654c6778456174d6cee9242f7fcaf81bf1464f47f43604b9e4eb298f051c6a4daba4630ca SHA512 4c17a25d91c085e12f26441fcde858e61bf191bd7d9dcf63ff5b5a1dce1d63e3f7c4f78ce8afa4f2359ad4ba6eb51f3e224ae6c502b18f5f7a76738534337431
 DIST singular-4.3.1p1.tar.gz 15090370 BLAKE2B d4e40378b3892b98b1f78c3928c8a40484336ea25ea4dcd4b3a1e5f651281d2cdb06d92c9cc64427ce76e91c5bf4eaa1c3b643df174a24c188823ae808817ad9 SHA512 d27d8e042ea085e49aed6a0697056c36e78e62ea0b9d17751cdf4c556cf4f6efce3b34b411c77aef97c6d90675bea11c97651eb7009634cb8a9b630ec820a06e
-DIST singular-4.3.1p2.tar.gz 15088650 BLAKE2B 17d73518653f6348297c955214aa8d30b3ce7cdf342f1bbb6fb49b746ddc563b1f46906df92f45abd601c834c77139f7aaccadf14bf706010017564d56948ca2 SHA512 ff2282b2fcd1a5b8809297036d524838403a2b66ae87ceb566ed6ff0571843d3c4aa0f7a4abbaab8541630f4e0130b6171ea0a7b8a5296b3b10f6c5cd5088828
+DIST singular-4.3.1p3.tar.gz 14991986 BLAKE2B 0ae2585a362839914d3a134bfe637f6faa34d95f58937f2adcca0c5a35e3218eb36554bae8187f5bb3a423dcac445c836e9bfff2d0d1a19d4e14a4452b84d839 SHA512 f092683f4a92158d82a2e694f284662c6285bac5faaa7d5e5695a84a220012fb8a733b4bbc52820def3037e1596ea4c2ab3846f58a3a3fb19e01bf7595790462
 EBUILD singular-4.3.1_p1.ebuild 2294 BLAKE2B 1147387c35f31d8bef97c67ec8d4596952494c85d8dd0c427981c7d491200fb3eb02658f3f63fde4e8323e1cc0f9ccbb467ae73ba17bbba12a05831b12f35348 SHA512 2d0c8047da3d2940f7ada1f68f314b7499a497dce09d7166f866f62bd67ab315df7bca5e90af07f897839ceb288651dd6be347a1ecceaa8ce6177f9a30df72d9
-EBUILD singular-4.3.1_p2.ebuild 2300 BLAKE2B d55b7cf13d0fbdd2d61f52237b709ffa470b955e256563b525a30929eeed12fe321b9f7935616d300d3e313e07bdebe62995c34b9586391cff70304f42915297 SHA512 dd7be599866c801ed2303319061f325f8052a8041b280d0815902cdc9f75fc88be5d1187ff4c4785716bd62eff8e480adf4c5a1bacfdab2711f05471e47a50b9
+EBUILD singular-4.3.1_p3.ebuild 2300 BLAKE2B 8335c3d556cb98834fa9f8f9a5287954b62444a30f3d6e4c5602b425f03d2646fe8fafe922bf41a0e978104e6cf424e4c5afbaf9263758a38b2e7931398a4362 SHA512 2beceeec3f73e1ef4fe470642d170eb4a0dce7d737dfb9453ca7cb1ab0283ab9199cb01a490487580ebb9a4f57f74ccc7c3742ddae6fe776396dee92ab648d3f
 MISC metadata.xml 782 BLAKE2B 7f10704c78b5a55cff9d07ffc3456a57aba4001ffd337dfbbb712e32608446ab9ae8039d14143939ad41710dcc6d4725992db2c80bcd1678397e563fefa929b4 SHA512 3c4904a4a8f63ff073745409caf9a9a68aa5d46861b8e8d77a538716a7a6a099d87137d604e52a3b8ce4ab81b7333f95389cd888ccbabe52017b6e8b1e4a77d0
diff --git a/sci-mathematics/singular/singular-4.3.1_p2.ebuild b/sci-mathematics/singular/singular-4.3.1_p3.ebuild
index 810f2e71b223..b51070f29cc5 100644
--- a/sci-mathematics/singular/singular-4.3.1_p2.ebuild
+++ b/sci-mathematics/singular/singular-4.3.1_p3.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=8