gentoo resync : 20.03.2022

5 files changed, 104 insertions, 0 deletions

diff --git a/sci-mathematics/coq-serapi/Manifest b/sci-mathematics/coq-serapi/Manifest
new file mode 100644
index 000000000000..79adbadee5cb
--- /dev/null
+++ b/sci-mathematics/coq-serapi/Manifest
@@ -0,0 +1,5 @@
+AUX 50sertop-gentoo.el 85 BLAKE2B d06e7c0823a3bedbf5f9c91ea8ea26bc9ed9d2ea44030316a1f3d65c19e51d874f03c845af5ae8237a9562cff7c81e24196c5ae29e54d79d1ba322f51904ba5d SHA512 42e61d798800d2e4c7e0702bdff53401a06ff6def54a1c7c0a8a6fd3e6a2f502c48bc84a04356818aa2ec5241bdd63b407837df123bfad76fafb78cf8a5a6cca
+AUX coq-serapi-sertop.el-path.patch 319 BLAKE2B 272eca8af934e10e978d149f90ee702fba443db7506468dda344242c5fe8a336f3ba3836c536bfac9ec6e540e1ee2f4c1a031d69e42901fbea92441b64e4c2a5 SHA512 5d228659e7c07e8fae69ffbff9d6a9de3113aa444c467194ce9e238a0db86c59c2be45b3e14683e47c2453c701b869e53647c9b051652af5ced8f4b3b5a15e73
+DIST coq-serapi-0.15.0.tar.gz 268083 BLAKE2B aeea2cb8ed0f648f307715c464f2da90585718aa8afedf69b4e1c282265a12a3937044397787404e43286cebaaf1f48efde93d845cd71c1c97cc1b2e9a2a8835 SHA512 3ba1b63002d36a4c0e64f86170d31c4131dc02e8cb8573b39f03ed44d1e5f29c064c472bebad367b875b02e36ced6bfe8c5fb2023bd798b3b79f74a5a2f54189
+EBUILD coq-serapi-0.15.0.ebuild 1364 BLAKE2B ac46f536fb9a0ac3a4c050732545409fa7f2a0ce888895e2b0ead2332317d1b51b3a964b91ba5baa9f86b050a2eb319889bedf20a7b6a1071ac5eb4c43e827e1 SHA512 bc8af4879ac61917ccda943a804f3daea2fe05bf63ccf17fdd4ef130c968702e8179c227e1c176efa2a59620910b366fcc8f4fa65d0398f806ec59931bbec6b9
+MISC metadata.xml 935 BLAKE2B e1444df414ce499df466597f5e0949e8ebf2d6da23d77028546324109659f58c5f0284a315ea062410a2f2e4631aac8d3564664719e89d76ad6ded9bb8ba7a5f SHA512 172fedbb2aa42e2be9aff426d64fcd69d2dfa206bb0e6072c6ecdc14a1923a2f0676303d8d8aebfe9a3e96e0a1e89185d2d4952bdb9ba1fff44b3891f26d6bf7
diff --git a/sci-mathematics/coq-serapi/coq-serapi-0.15.0.ebuild b/sci-mathematics/coq-serapi/coq-serapi-0.15.0.ebuild
new file mode 100644
index 000000000000..2733c490f747
--- /dev/null
+++ b/sci-mathematics/coq-serapi/coq-serapi-0.15.0.ebuild
@@ -0,0 +1,64 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+COQV=8.15.0
+
+inherit elisp-common dune
+
+DESCRIPTION="Serialization library and protocol for interaction with the Coq proof assistant"
+HOMEPAGE="https://github.com/ejgallego/coq-serapi/"
+# The tarball in SRC_URI is comprised of <supported coq>+<package version>
+SRC_URI="https://github.com/ejgallego/${PN}/archive/${COQV}+${PV}.tar.gz
+		-> ${P}.tar.gz"
+S="${WORKDIR}"/${PN}-${COQV}-${PV}
+
+LICENSE="GPL-3+"
+SLOT="0/${PV}"
+KEYWORDS="~amd64"
+IUSE="emacs +ocamlopt test"
+RESTRICT="!test? ( test )"
+
+RDEPEND="
+	>=sci-mathematics/coq-${COQV}:=
+	dev-ml/cmdliner:=
+	dev-ml/ppx_deriving:=
+	dev-ml/ppx_deriving_yojson:=
+	dev-ml/ppx_import:=
+	dev-ml/ppx_sexp_conv:=
+	dev-ml/sexplib:=
+	dev-ml/yojson:=
+"
+DEPEND="${RDEPEND}"
+BDEPEND="
+	emacs? ( >=app-editors/emacs-23.1:* )
+	test? ( sci-mathematics/coq-mathcomp )
+"
+
+PATCHES=( "${FILESDIR}"/${PN}-sertop.el-path.patch )
+SITEFILE="50sertop-gentoo.el"
+
+src_compile() {
+	dune_src_compile
+
+	use emacs && elisp-compile sertop.el
+}
+
+src_install() {
+	dune_src_install
+
+	rm -r "${D}"/usr/share/emacs || die
+	if use emacs ; then
+		elisp-install sertop sertop.el{,c}
+		elisp-site-file-install "${FILESDIR}/${SITEFILE}"
+	fi
+}
+
+pkg_postinst() {
+	use emacs && elisp-site-regen
+}
+
+pkg_postrm() {
+	use emacs && elisp-site-regen
+}
diff --git a/sci-mathematics/coq-serapi/files/50sertop-gentoo.el b/sci-mathematics/coq-serapi/files/50sertop-gentoo.el
new file mode 100644
index 000000000000..b630f718aa19
--- /dev/null
+++ b/sci-mathematics/coq-serapi/files/50sertop-gentoo.el
@@ -0,0 +1,2 @@
+(add-to-list 'load-path "@SITELISP@")
+(autoload 'sertop "sertop" "Launch sertop." t)
diff --git a/sci-mathematics/coq-serapi/files/coq-serapi-sertop.el-path.patch b/sci-mathematics/coq-serapi/files/coq-serapi-sertop.el-path.patch
new file mode 100644
index 000000000000..628ed22a64ff
--- /dev/null
+++ b/sci-mathematics/coq-serapi/files/coq-serapi-sertop.el-path.patch
@@ -0,0 +1,12 @@
+index 300a22f..63f7dcc 100644
+--- a/sertop.el
++++ b/sertop.el
+@@ -37,7 +37,7 @@
+                            (buffer-file-name))))
+ 
+ (defvar sertop-executable-path
+-  (or (expand-file-name "sertop.native" sertop--root)
++  (or (executable-find "sertop.native")
+       (executable-find "sertop"))
+   "Path to sertop.")
+ 
diff --git a/sci-mathematics/coq-serapi/metadata.xml b/sci-mathematics/coq-serapi/metadata.xml
new file mode 100644
index 000000000000..fd440ed6e397
--- /dev/null
+++ b/sci-mathematics/coq-serapi/metadata.xml
@@ -0,0 +1,21 @@
+<?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>
+    SerAPI is a library for machine-to-machine interaction with the Coq proof
+    assistant, with particular emphasis on applications in IDEs, code analysis
+    tools, and machine learning. SerAPI provides automatic serialization of
+    Coq's internal OCaml datatypes from/to JSON or S-expressions (sexps).
+    SerAPI is a proof-of-concept and should be considered alpha-quality.
+  </longdescription>
+  <upstream>
+    <changelog>https://github.com/ejgallego/coq-serapi/releases/</changelog>
+    <bugs-to>https://github.com/ejgallego/coq-serapi/issues/</bugs-to>
+    <remote-id type="github">ejgallego/coq-serapi</remote-id>
+  </upstream>
+</pkgmetadata>