summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaciej Barć <xgqt@gentoo.org>2023-06-03 18:51:22 +0200
committerMaciej Barć <xgqt@gentoo.org>2023-06-03 18:55:36 +0200
commit267fe5e4e1b5c504da69597a3fe054220a033234 (patch)
treed26fa9144d3876b765ef952e576e047af0cd810c /sci-mathematics/kind2
parentdev-lang/perl: update dual-script versions (diff)
downloadgentoo-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/Manifest1
-rw-r--r--sci-mathematics/kind2/kind2-1.9.0.ebuild36
-rw-r--r--sci-mathematics/kind2/metadata.xml28
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>