From ad391b961414c99124b93cb86695c04bd8d57937 Mon Sep 17 00:00:00 2001 From: V3n3RiX Date: Wed, 11 Jan 2023 05:43:34 +0000 Subject: gentoo auto-resync : 11:01:2023 - 05:43:34 --- sci-mathematics/cubicle/Manifest | 4 ++ sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild | 71 +++++++++++++++++++++++ sci-mathematics/cubicle/files/50cubicle-gentoo.el | 4 ++ sci-mathematics/cubicle/metadata.xml | 31 ++++++++++ 4 files changed, 110 insertions(+) create mode 100644 sci-mathematics/cubicle/Manifest create mode 100644 sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild create mode 100644 sci-mathematics/cubicle/files/50cubicle-gentoo.el create mode 100644 sci-mathematics/cubicle/metadata.xml (limited to 'sci-mathematics/cubicle') diff --git a/sci-mathematics/cubicle/Manifest b/sci-mathematics/cubicle/Manifest new file mode 100644 index 000000000000..aa9a2c6b901b --- /dev/null +++ b/sci-mathematics/cubicle/Manifest @@ -0,0 +1,4 @@ +AUX 50cubicle-gentoo.el 185 BLAKE2B 76ef002c52bd0d6ef8ce5474e5cf9032cffe861d273a88176c3a8eae17f6176896bc1a4cb099d1f793b63f1ad3e0b7fb6d4b066317f160a0a4fd586e0a61ec64 SHA512 c9a93fec3f1f12cbe326940a79dfe950b56c82e7bdd24a6bf5923d1c4fe6245b8fec4c399f3e60c16cc4757f290f9cbeab606a20b5844f4228a4f29b0ed669f4 +DIST cubicle-1.2.0.tar.gz 866004 BLAKE2B 4fd944acb394165396344b7a9d4b29ffcb7b61571e1ac9cb90aacf1a5ddb0521d399f301a51af6b37461e5a47244fb095ad69ab0041440c240257522ba4de4a7 SHA512 e2815b4b7b4feda30df91eabebae741d14a2c822f5efea972676bc7a941454ea368e9dc003f754c2edb1c6b1db5a5c86a354b3612c2d47a9095f8fc348dfb692 +EBUILD cubicle-1.2.0-r1.ebuild 1332 BLAKE2B 7dbbb9ed042dd4ecabb00ee3ccc050e39174b01e7131f90b6bbd5dde249299071e30eee3f2cfd5576f8504b7a3f27ab1430428935b4012e0da69c8cbc67409b7 SHA512 a9018679ffa0b2481fd3629518317e8ceab2494d66d1688e1a95ff41b73964a62f17b4d2c6e2ad17e130c09e93b84bb1d23f360e5eebdb8f6f87f154a4069f9d +MISC metadata.xml 1503 BLAKE2B d67f3f6524234cf3be4b0118aced6f4e3424a25754d91b13eb5c8250aedb6a57a6f7faabe6539875953874f48b2d8349fe3adfe431b72675fdd6723cb9ff3c52 SHA512 96540a56c6ef839924fa93f49e4ffdeb8a5eb3b83ef43bd62ccbed72dfa522f1b0acad4132650f67387915af5be8fe432fd6d01f8c9a76271c53f7f3a33f476d diff --git a/sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild b/sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild new file mode 100644 index 000000000000..8159f9f60a4a --- /dev/null +++ b/sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild @@ -0,0 +1,71 @@ +# 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 + + doman doc/${PN}.1 + + 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 @@ + + + + + + ml@gentoo.org + ML + + + sci-mathematics@gentoo.org + Gentoo Mathematics Project + + + 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. + + + https://github.com/cubicle-model-checker/cubicle/issues/ + cubicle-model-checker/cubicle + + -- cgit v1.2.3