commit:     8ac30bce24f027d7124ae09e613997f593a61a8d
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Mon Oct  3 21:15:27 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Mon Oct  3 21:38:09 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=8ac30bce

dev-lang/boogie: new package; add version 2.15.8

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

 dev-lang/boogie/Manifest             |  2 ++
 dev-lang/boogie/boogie-2.15.8.ebuild | 58 ++++++++++++++++++++++++++++++++++++
 dev-lang/boogie/metadata.xml         | 24 +++++++++++++++
 3 files changed, 84 insertions(+)

diff --git a/dev-lang/boogie/Manifest b/dev-lang/boogie/Manifest
new file mode 100644
index 000000000000..0215e7b7d733
--- /dev/null
+++ b/dev-lang/boogie/Manifest
@@ -0,0 +1,2 @@
+DIST boogie-2.15.8-deps.tar.xz 71100772 BLAKE2B 
1249627710fe0cc08c640ac7fe5e518793d237291810dc2df5d26bae2a4fd0fec15f0529b6fb799231002881665c2b2cf66b3a6a88494c780e96e51d78086959
 SHA512 
ee8df5693264c6b6e925f966a85e312e2df80d121c6e81786e7672d1591cdab8a66601c7d740df9db9704330a82f5aa01982d758cc4d5f151838be41c4d0b76f
+DIST boogie-2.15.8.tar.gz 1548233 BLAKE2B 
cd3d46b6702eb9c16cdb94ae9776ee52bb142be57e3b0dfd014e59c2f3a98aec84d891544cbd239d773c49ac6bc0b3e1eb5e1eb5cda1f1a0b9aa029f0ee674f2
 SHA512 
5e214a6451b0ac6a33088797957661cdb35e7fc99f880935f0f1d9329975c11a0849f5ba6244e90f528e6cc31dc2fc83636506130f59464889bf04ecf6130990

diff --git a/dev-lang/boogie/boogie-2.15.8.ebuild 
b/dev-lang/boogie/boogie-2.15.8.ebuild
new file mode 100644
index 000000000000..791a595d8262
--- /dev/null
+++ b/dev-lang/boogie/boogie-2.15.8.ebuild
@@ -0,0 +1,58 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+DOTNET_COMPAT=6.0
+
+inherit edo multiprocessing
+
+DESCRIPTION="SMT-based program verifier"
+HOMEPAGE="https://github.com/boogie-org/boogie/";
+SRC_URI="
+       https://github.com/boogie-org/${PN}/archive/v${PV}.tar.gz -> ${P}.tar.gz
+       https://dev.gentoo.org/~xgqt/distfiles/deps/${P}-deps.tar.xz
+"
+S="${S}"/Source
+
+LICENSE="MIT"
+SLOT="0"
+KEYWORDS="~amd64"
+
+RDEPEND="virtual/dotnet-sdk:${DOTNET_COMPAT}"
+BDEPEND="${RDEPEND}"
+
+# Generated by dotnet.
+QA_PREBUILT="/usr/share/boogie/BoogieDriver"
+
+src_prepare() {
+       export DOTNET_CLI_TELEMETRY_OPTOUT=1
+       export DOTNET_NOLOGO=1
+       export NUGET_PACKAGES="${S}"/nuget_packages
+       export DOTNET_OUTPUT="${WORKDIR}"/${P}_net${DOTNET_COMPAT}_Release/${PN}
+
+       default
+}
+
+src_configure() {
+       edob dotnet restore
+}
+
+src_compile() {
+       local myopts=(
+               --configuration Release
+               --no-restore
+               --no-self-contained
+               --nologo
+               --output "${DOTNET_OUTPUT}"
+               -consoleLoggerParameters:ErrorsOnly
+               -maxCpuCount:$(makeopts_jobs)
+       )
+       edob dotnet build ${myopts[@]}
+}
+
+src_install() {
+       mkdir -p "${ED}"/usr/share/ || die
+       cp -r "${DOTNET_OUTPUT}" "${ED}"/usr/share/ || die
+       dosym -r /usr/share/${PN}/BoogieDriver /usr/bin/boogie
+}

diff --git a/dev-lang/boogie/metadata.xml b/dev-lang/boogie/metadata.xml
new file mode 100644
index 000000000000..e0e4670c63ec
--- /dev/null
+++ b/dev-lang/boogie/metadata.xml
@@ -0,0 +1,24 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd";>
+
+<pkgmetadata>
+  <maintainer type="person">
+    <email>[email protected]</email>
+    <name>Maciej Barć</name>
+  </maintainer>
+  <longdescription>
+    Boogie is an intermediate verification language (IVL), intended as a layer
+    on which to build program verifiers for other languages. Several program
+    verifiers have been built in this way, including the VCC and HAVOC
+    verifiers for C and the verifiers for Dafny, Chalice, and Spec#. For a
+    sample verifier for a toy language built on top of Boogie, see Forro.
+    Boogie is also the name of a tool. The tool accepts the Boogie language as
+    input, optionally infers some invariants in the given Boogie program, and
+    then generates verification conditions that are passed to an SMT solver.
+    The default SMT solver is Z3.
+  </longdescription>
+  <upstream>
+    <bugs-to>https://github.com/boogie-org/boogie/issues/</bugs-to>
+    <remote-id type="github">boogie-org/boogie</remote-id>
+  </upstream>
+</pkgmetadata>

Reply via email to