gentoo auto-resync : 15:01:2024 - 23:10:08

6 files changed, 31 insertions, 34 deletions

diff --git a/metadata/md5-cache/sci-mathematics/Manifest.gz b/metadata/md5-cache/sci-mathematics/Manifest.gz
index a09d99fb6744..b20cf8993437 100644
--- a/metadata/md5-cache/sci-mathematics/Manifest.gz
+++ b/metadata/md5-cache/sci-mathematics/Manifest.gz
diff --git a/metadata/md5-cache/sci-mathematics/coq-mathcomp-1.16.0-r1 b/metadata/md5-cache/sci-mathematics/coq-mathcomp-1.19.0
index 2acc650b796b..3b2b073a6eed 100644
--- a/metadata/md5-cache/sci-mathematics/coq-mathcomp-1.16.0-r1
+++ b/metadata/md5-cache/sci-mathematics/coq-mathcomp-1.19.0
@@ -6,6 +6,6 @@ HOMEPAGE=https://github.com/math-comp/math-comp/
 KEYWORDS=~amd64
 LICENSE=CeCILL-B
 RDEPEND=>=sci-mathematics/coq-8.16.0:= dev-lang/ocaml:=
-SLOT=0/1.16.0
-SRC_URI=https://github.com/math-comp/math-comp/archive/mathcomp-1.16.0.tar.gz -> coq-mathcomp-1.16.0.tar.gz
-_md5_=7744fa680896197a26f8a5e0260e7652
+SLOT=0/1.19.0
+SRC_URI=https://github.com/math-comp/math-comp/archive/mathcomp-1.19.0.tar.gz -> coq-mathcomp-1.19.0.tar.gz
+_md5_=389be06bd85bd68015c738f568ec99bb
diff --git a/metadata/md5-cache/sci-mathematics/coq-serapi-0.17.0 b/metadata/md5-cache/sci-mathematics/coq-serapi-0.17.0
deleted file mode 100644
index d166ff3eb889..000000000000
--- a/metadata/md5-cache/sci-mathematics/coq-serapi-0.17.0
+++ /dev/null
@@ -1,16 +0,0 @@
-BDEPEND=emacs? ( >=app-editors/emacs-23.1:* ) test? ( sci-mathematics/coq-mathcomp ) dev-lang/ocaml dev-ml/dune
-DEFINED_PHASES=compile install postinst postrm test
-DEPEND=>=sci-mathematics/coq-8.17.0:= <sci-mathematics/coq-8.18.0:= >=dev-ml/ppx_sexp_conv-0.13.0:= dev-ml/cmdliner:= dev-ml/ppx_compare:= dev-ml/ppx_deriving:= dev-ml/ppx_deriving_yojson:= dev-ml/ppx_hash:= dev-ml/ppx_import:= dev-ml/sexplib:= dev-ml/yojson:= >=dev-lang/ocaml-4:=[ocamlopt?] dev-ml/dune:=
-DESCRIPTION=Serialization library and protocol for interaction with the Coq proof assistant
-EAPI=8
-HOMEPAGE=https://github.com/ejgallego/coq-serapi/
-INHERIT=elisp-common dune
-IUSE=emacs +ocamlopt test
-KEYWORDS=~amd64
-LICENSE=GPL-3+
-RDEPEND=>=sci-mathematics/coq-8.17.0:= <sci-mathematics/coq-8.18.0:= >=dev-ml/ppx_sexp_conv-0.13.0:= dev-ml/cmdliner:= dev-ml/ppx_compare:= dev-ml/ppx_deriving:= dev-ml/ppx_deriving_yojson:= dev-ml/ppx_hash:= dev-ml/ppx_import:= dev-ml/sexplib:= dev-ml/yojson:= >=dev-lang/ocaml-4:=[ocamlopt?] dev-ml/dune:=
-RESTRICT=!test? ( test )
-SLOT=0/0.17.0
-SRC_URI=https://github.com/ejgallego/coq-serapi/archive/8.17.0+0.17.0.tar.gz -> coq-serapi-0.17.0.tar.gz
-_eclasses_=dune	beddc7cde467b2e48afc78a87d042c01	edo	c0eb9cbe6b0bd01fcb4918f12598a4d3	elisp-common	2a0fa407d2e6363c663ccb299503b25c	multiprocessing	30ead54fa2e2b5f9cd4e612ffc34d0fe
-_md5_=23e75861df0e6ab4488206048389f9c9
diff --git a/metadata/md5-cache/sci-mathematics/eprover-3.0.03 b/metadata/md5-cache/sci-mathematics/eprover-3.0.03
new file mode 100644
index 000000000000..9982f399b9df
--- /dev/null
+++ b/metadata/md5-cache/sci-mathematics/eprover-3.0.03
@@ -0,0 +1,13 @@
+BDEPEND=sys-apps/help2man
+DEFINED_PHASES=compile configure install prepare
+DESCRIPTION=Automated theorem prover for full first-order logic with equality
+EAPI=8
+HOMEPAGE=https://www.eprover.org/ https://github.com/eprover/eprover/
+INHERIT=toolchain-funcs
+IUSE=+ho
+KEYWORDS=~amd64 ~x86
+LICENSE=GPL-2+
+SLOT=0
+SRC_URI=https://github.com/eprover/eprover/archive/E-3.0.03.tar.gz -> eprover-3.0.03.tar.gz
+_eclasses_=multilib	c19072c3cd7ac5cb21de013f7e9832e0	toolchain-funcs	e56c7649b804f051623c8bc1a1c44084
+_md5_=a738ad3e7bb3fea44d92b8f996669864
diff --git a/metadata/md5-cache/sci-mathematics/gappa-1.4.2 b/metadata/md5-cache/sci-mathematics/gappa-1.4.2
new file mode 100644
index 000000000000..7158ae803aa4
--- /dev/null
+++ b/metadata/md5-cache/sci-mathematics/gappa-1.4.2
@@ -0,0 +1,15 @@
+BDEPEND=doc? ( app-text/doxygen )
+DEFINED_PHASES=compile install test
+DEPEND=dev-libs/boost:= dev-libs/gmp:0= dev-libs/mpfr:0=
+DESCRIPTION=Tool for verifying floating-point or fixed-point arithmetic
+EAPI=8
+HOMEPAGE=https://gappa.gitlabpages.inria.fr/ https://gitlab.inria.fr/gappa/gappa/
+INHERIT=docs multiprocessing
+IUSE=doc
+KEYWORDS=~amd64 ~x86
+LICENSE=CeCILL-2 GPL-3+
+RDEPEND=dev-libs/boost:= dev-libs/gmp:0= dev-libs/mpfr:0=
+SLOT=0
+SRC_URI=https://gappa.gitlabpages.inria.fr/releases/gappa-1.4.2.tar.gz
+_eclasses_=docs	7f3c0d47338743498c69f1887a139f57	multiprocessing	30ead54fa2e2b5f9cd4e612ffc34d0fe
+_md5_=2aa7d6e62f76d923e74195b6f93aae7e
diff --git a/metadata/md5-cache/sci-mathematics/lean-4.2.0_rc4 b/metadata/md5-cache/sci-mathematics/lean-4.2.0_rc4
deleted file mode 100644
index 6986f3de2692..000000000000
--- a/metadata/md5-cache/sci-mathematics/lean-4.2.0_rc4
+++ /dev/null
@@ -1,15 +0,0 @@
-BDEPEND=|| ( dev-lang/python:3.12 dev-lang/python:3.11 dev-lang/python:3.10 ) dev-build/make >=dev-build/cmake-3.20.5
-DEFINED_PHASES=compile configure install prepare setup test
-DEPEND=dev-libs/gmp:=
-DESCRIPTION=The Lean Theorem Prover
-EAPI=8
-HOMEPAGE=https://leanprover-community.github.io/
-INHERIT=cmake flag-o-matic python-any-r1
-IUSE=debug source
-KEYWORDS=~amd64 ~x86
-LICENSE=Apache-2.0
-RDEPEND=dev-libs/gmp:=
-SLOT=0/4
-SRC_URI=https://github.com/leanprover/lean4/archive/refs/tags/v4.2.0-rc4.tar.gz -> lean-4.2.0_rc4.tar.gz
-_eclasses_=cmake	c7c9a62d6232cac66d4ea32d575c3e7c	flag-o-matic	78cf3cc2d5572fddf5e5e10c70f7c81a	multilib	c19072c3cd7ac5cb21de013f7e9832e0	multiprocessing	30ead54fa2e2b5f9cd4e612ffc34d0fe	ninja-utils	2df4e452cea39a9ec8fb543ce059f8d6	python-any-r1	f5169813d1619761b459800587005fd2	python-utils-r1	042f4cc53680245bf99a84669b94155a	toolchain-funcs	e56c7649b804f051623c8bc1a1c44084	xdg-utils	baea6080dd821f5562d715887954c9d3
-_md5_=867ce6e13c8e3a5abfc02fd4a232de38