gentoo auto-resync : 10:04:2023 - 23:37:47

5 files changed, 48 insertions, 2 deletions

diff --git a/metadata/md5-cache/sci-mathematics/Manifest.gz b/metadata/md5-cache/sci-mathematics/Manifest.gz
index 3ccfd1d3dd93..34094da5c0af 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-8.17.0 b/metadata/md5-cache/sci-mathematics/coq-8.17.0
new file mode 100644
index 000000000000..5b61233068a2
--- /dev/null
+++ b/metadata/md5-cache/sci-mathematics/coq-8.17.0
@@ -0,0 +1,15 @@
+BDEPEND=dev-ml/findlib doc? ( >=dev-java/antlr-4.7:4 dev-python/antlr4-python3-runtime dev-python/beautifulsoup4 dev-python/pexpect dev-python/sphinx-rtd-theme dev-python/sphinxcontrib-bibtex dev-tex/latexmk dev-texlive/texlive-fontsextra dev-texlive/texlive-latexextra dev-texlive/texlive-xetex media-fonts/freefont ) dev-lang/ocaml dev-ml/dune
+DEFINED_PHASES=compile configure install test
+DEPEND=dev-ml/zarith:= || ( dev-ml/num <dev-lang/ocaml-4.09.0[ocamlopt?] ) gui? ( >=dev-ml/lablgtk-3.1.2:3=[sourceview,ocamlopt?] >=dev-ml/lablgtk-sourceview-3.1.2:3=[ocamlopt?] ) >=dev-lang/ocaml-4:=[ocamlopt?] dev-ml/dune:=
+DESCRIPTION=Proof assistant written in O'Caml
+EAPI=8
+HOMEPAGE=http://coq.inria.fr/ https://github.com/coq/coq/
+INHERIT=desktop dune edo
+IUSE=debug doc gui +ocamlopt
+KEYWORDS=~amd64 ~x86
+LICENSE=LGPL-2.1
+RDEPEND=dev-ml/zarith:= || ( dev-ml/num <dev-lang/ocaml-4.09.0[ocamlopt?] ) gui? ( >=dev-ml/lablgtk-3.1.2:3=[sourceview,ocamlopt?] >=dev-ml/lablgtk-sourceview-3.1.2:3=[ocamlopt?] ) >=dev-lang/ocaml-4:=[ocamlopt?] dev-ml/dune:=
+SLOT=0/8.17.0
+SRC_URI=https://github.com/coq/coq/archive/V8.17.0.tar.gz -> coq-8.17.0.tar.gz
+_eclasses_=desktop	021728fdc1b03b36357dbc89489e0f0d	dune	beddc7cde467b2e48afc78a87d042c01	edo	c0eb9cbe6b0bd01fcb4918f12598a4d3	multiprocessing	b4e253ab22cef7b1085e9b67c7a3b730
+_md5_=155d29142c721e3d825b6edd05b6f3b2
diff --git a/metadata/md5-cache/sci-mathematics/coq-serapi-0.16.3 b/metadata/md5-cache/sci-mathematics/coq-serapi-0.16.3
index c3f28a6da3a3..ab6ec1edaa6b 100644
--- a/metadata/md5-cache/sci-mathematics/coq-serapi-0.16.3
+++ b/metadata/md5-cache/sci-mathematics/coq-serapi-0.16.3
@@ -11,6 +11,6 @@ LICENSE=GPL-3+
 RDEPEND=>=sci-mathematics/coq-8.16.0:= <sci-mathematics/coq-8.17.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.16.3
-SRC_URI=https://github.com/ejgallego/coq-serapi/archive/+0.16.3.tar.gz -> coq-serapi-0.16.3.tar.gz
+SRC_URI=https://github.com/ejgallego/coq-serapi/archive/8.16.0+0.16.3.tar.gz -> coq-serapi-0.16.3.tar.gz
 _eclasses_=dune	beddc7cde467b2e48afc78a87d042c01	edo	c0eb9cbe6b0bd01fcb4918f12598a4d3	elisp-common	1d6e8d43be4713f04a441f721d890d48	multiprocessing	b4e253ab22cef7b1085e9b67c7a3b730
-_md5_=1062822da13bb0d055ad6b66c2d70a25
+_md5_=e77e0b3330ffe3ef2ab69e3e61580fa2
diff --git a/metadata/md5-cache/sci-mathematics/coq-serapi-0.17.0 b/metadata/md5-cache/sci-mathematics/coq-serapi-0.17.0
new file mode 100644
index 000000000000..7c00cd207c7c
--- /dev/null
+++ b/metadata/md5-cache/sci-mathematics/coq-serapi-0.17.0
@@ -0,0 +1,16 @@
+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	1d6e8d43be4713f04a441f721d890d48	multiprocessing	b4e253ab22cef7b1085e9b67c7a3b730
+_md5_=23e75861df0e6ab4488206048389f9c9
diff --git a/metadata/md5-cache/sci-mathematics/gappalib-coq-1.5.3 b/metadata/md5-cache/sci-mathematics/gappalib-coq-1.5.3
new file mode 100644
index 000000000000..2e2ab0833790
--- /dev/null
+++ b/metadata/md5-cache/sci-mathematics/gappalib-coq-1.5.3
@@ -0,0 +1,15 @@
+BDEPEND=dev-ml/findlib
+DEFINED_PHASES=compile install test
+DEPEND=dev-lang/ocaml:=[ocamlopt?] >=sci-mathematics/coq-8.12:= sci-mathematics/flocq:= sci-mathematics/gappa
+DESCRIPTION=Allows the certificates Gappa generates to be imported by the Coq
+EAPI=8
+HOMEPAGE=https://gappa.gitlabpages.inria.fr/ https://gitlab.inria.fr/gappa/coq/
+INHERIT=multiprocessing
+IUSE=ocamlopt
+KEYWORDS=~amd64 ~x86
+LICENSE=LGPL-3+
+RDEPEND=dev-lang/ocaml:=[ocamlopt?] >=sci-mathematics/coq-8.12:= sci-mathematics/flocq:= sci-mathematics/gappa
+SLOT=0
+SRC_URI=https://gappa.gitlabpages.inria.fr/releases/gappalib-coq-1.5.3.tar.gz
+_eclasses_=multiprocessing	b4e253ab22cef7b1085e9b67c7a3b730
+_md5_=eede2e3173501268addfc41b74909f4d