commit: f6f7c1b270ceb94292a91628505bdfe5b6cebcb4 Author: Maciej Barć <xgqt <AT> gentoo <DOT> org> AuthorDate: Sat Mar 5 02:38:53 2022 +0000 Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org> CommitDate: Sat Mar 5 04:40:57 2022 +0000 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=f6f7c1b2
sci-mathematics/coq-serapi: new package; add 0.15.0 Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org> sci-mathematics/coq-serapi/Manifest | 1 + .../coq-serapi/coq-serapi-0.15.0.ebuild | 64 ++++++++++++++++++++++ .../coq-serapi/files/50sertop-gentoo.el | 2 + .../files/coq-serapi-sertop.el-path.patch | 12 ++++ sci-mathematics/coq-serapi/metadata.xml | 21 +++++++ 5 files changed, 100 insertions(+) diff --git a/sci-mathematics/coq-serapi/Manifest b/sci-mathematics/coq-serapi/Manifest new file mode 100644 index 000000000000..512540a49757 --- /dev/null +++ b/sci-mathematics/coq-serapi/Manifest @@ -0,0 +1 @@ +DIST coq-serapi-0.15.0.tar.gz 268083 BLAKE2B aeea2cb8ed0f648f307715c464f2da90585718aa8afedf69b4e1c282265a12a3937044397787404e43286cebaaf1f48efde93d845cd71c1c97cc1b2e9a2a8835 SHA512 3ba1b63002d36a4c0e64f86170d31c4131dc02e8cb8573b39f03ed44d1e5f29c064c472bebad367b875b02e36ced6bfe8c5fb2023bd798b3b79f74a5a2f54189 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-mathemat...@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>
