commit: 30a0e97a15345909414364403a7af8654b9e72cd Author: Maciej Barć <xgqt <AT> gentoo <DOT> org> AuthorDate: Tue Jan 10 21:30:03 2023 +0000 Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org> CommitDate: Tue Jan 10 23:17:59 2023 +0000 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=30a0e97a
sci-mathematics/cubicle: new package; add 1.2.0 Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org> sci-mathematics/cubicle/Manifest | 1 + sci-mathematics/cubicle/cubicle-1.2.0.ebuild | 69 +++++++++++++++++++++++ sci-mathematics/cubicle/files/50cubicle-gentoo.el | 4 ++ sci-mathematics/cubicle/metadata.xml | 31 ++++++++++ 4 files changed, 105 insertions(+) diff --git a/sci-mathematics/cubicle/Manifest b/sci-mathematics/cubicle/Manifest new file mode 100644 index 000000000000..c5054c4a4157 --- /dev/null +++ b/sci-mathematics/cubicle/Manifest @@ -0,0 +1 @@ +DIST cubicle-1.2.0.tar.gz 866004 BLAKE2B 4fd944acb394165396344b7a9d4b29ffcb7b61571e1ac9cb90aacf1a5ddb0521d399f301a51af6b37461e5a47244fb095ad69ab0041440c240257522ba4de4a7 SHA512 e2815b4b7b4feda30df91eabebae741d14a2c822f5efea972676bc7a941454ea368e9dc003f754c2edb1c6b1db5a5c86a354b3612c2d47a9095f8fc348dfb692 diff --git a/sci-mathematics/cubicle/cubicle-1.2.0.ebuild b/sci-mathematics/cubicle/cubicle-1.2.0.ebuild new file mode 100644 index 000000000000..d2f5d0e356f2 --- /dev/null +++ b/sci-mathematics/cubicle/cubicle-1.2.0.ebuild @@ -0,0 +1,69 @@ +# 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 + + 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>[email protected]</email> + <name>ML</name> + </maintainer> + <maintainer type="project"> + <email>[email protected]</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>
