[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/kind2/

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/kind2/

[Maciej Barć]

commit:     267fe5e4e1b5c504da69597a3fe054220a033234
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Jun  3 16:51:22 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Jun  3 16:55:36 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=267fe5e4

sci-mathematics/kind2: new package; add 1.9.0

Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>

 sci-mathematics/kind2/Manifest           |  1 +
 sci-mathematics/kind2/kind2-1.9.0.ebuild | 36 ++++++++++++++++++++++++++++++++
 sci-mathematics/kind2/metadata.xml       | 28 +++++++++++++++++++++++++
 3 files changed, 65 insertions(+)

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>