diff options
author | Maciej Barć <xgqt@gentoo.org> | 2023-06-03 18:51:22 +0200 |
---|---|---|
committer | Maciej Barć <xgqt@gentoo.org> | 2023-06-03 18:55:36 +0200 |
commit | 267fe5e4e1b5c504da69597a3fe054220a033234 (patch) | |
tree | d26fa9144d3876b765ef952e576e047af0cd810c /sci-mathematics/kind2 | |
parent | dev-lang/perl: update dual-script versions (diff) | |
download | gentoo-267fe5e4e1b5c504da69597a3fe054220a033234.tar.gz gentoo-267fe5e4e1b5c504da69597a3fe054220a033234.tar.bz2 gentoo-267fe5e4e1b5c504da69597a3fe054220a033234.zip |
sci-mathematics/kind2: new package; add 1.9.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Diffstat (limited to 'sci-mathematics/kind2')
-rw-r--r-- | sci-mathematics/kind2/Manifest | 1 | ||||
-rw-r--r-- | sci-mathematics/kind2/kind2-1.9.0.ebuild | 36 | ||||
-rw-r--r-- | sci-mathematics/kind2/metadata.xml | 28 |
3 files changed, 65 insertions, 0 deletions
diff --git a/sci-mathematics/kind2/Manifest b/sci-mathematics/kind2/Manifest new file mode 100644 index 000000000000..f687573f8c7e --- /dev/null +++ b/sci-mathematics/kind2/Manifest @@ -0,0 +1 @@ +DIST kind2-1.9.0.tar.gz 2009655 BLAKE2B 531e019cd9cd6edf5799b4283c56eda677dd16e6feec5ab8047d30cf5399a94789b0fd9b39e1fc83a1794a9cf496657d7a3c5eb156a9d4c8358e8a00057504f3 SHA512 c2b441aed01e1e95ddc0ad59b0097d58b4c90a1cf04adcc3ec27d1383937dddac1999825eb3d02f81e3f9f4d146c8b5f2e9f2b315317b0566f91867bbb3e528a diff --git a/sci-mathematics/kind2/kind2-1.9.0.ebuild b/sci-mathematics/kind2/kind2-1.9.0.ebuild new file mode 100644 index 000000000000..012c60845bd5 --- /dev/null +++ b/sci-mathematics/kind2/kind2-1.9.0.ebuild @@ -0,0 +1,36 @@ +# Copyright 1999-2023 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +inherit dune + +DESCRIPTION="Multi-engine SMT-based automatic model checker" +HOMEPAGE="https://kind2-mc.github.io/kind2/ + https://github.com/kind2-mc/kind2/" + +if [[ ${PV} == *9999* ]] ; then + inherit git-r3 + EGIT_REPO_URI="https://github.com/kind2-mc/${PN}.git" +else + SRC_URI="https://github.com/kind2-mc/${PN}/archive/v${PV}.tar.gz + -> ${P}.tar.gz" + KEYWORDS="~amd64" +fi + +LICENSE="Apache-2.0" +SLOT="0/${PV}" +IUSE="+ocamlopt test" +RESTRICT="!test? ( test )" + +RDEPEND=" + dev-ml/menhir:= + dev-ml/num:= + dev-ml/yojson:= + dev-ml/zmq:= +" +DEPEND="${RDEPEND}" +BDEPEND=" + dev-ml/dune-build-info + test? ( dev-ml/ounit2 ) +" diff --git a/sci-mathematics/kind2/metadata.xml b/sci-mathematics/kind2/metadata.xml new file mode 100644 index 000000000000..faf6e30c3a71 --- /dev/null +++ b/sci-mathematics/kind2/metadata.xml @@ -0,0 +1,28 @@ +<?xml version="1.0" encoding="UTF-8"?> +<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd"> + +<pkgmetadata> + <maintainer type="project"> + <email>ml@gentoo.org</email> + <name>ML</name> + </maintainer> + <maintainer type="project"> + <email>sci-mathematics@gentoo.org</email> + <name>Gentoo Mathematics Project</name> + </maintainer> + <longdescription> + Kind 2 is an open-source, multi-engine, SMT-based automatic model checker + for safety properties of finite-state or infinite-state synchronous + reactive systems expressed as in an extension of the Lustre language. In + its basic configuration it takes as input one or more Lustre files + annotated with properties to be proven invariant, and outputs for each + property either a confirmation or a counterexample, i.e., a sequence inputs + that falsifies the property. More advanced features include contract-based + compositional verification, proof generation for proven properties, and + contract-based test generation. + </longdescription> + <upstream> + <bugs-to>https://github.com/kind2-mc/kind2/issues/</bugs-to> + <remote-id type="github">kind2-mc/kind2</remote-id> + </upstream> +</pkgmetadata> |