From 69a8b079142d16bd6d9718b62d7b1c1bbc806c8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maciej=20Bar=C4=87?= Date: Tue, 26 Oct 2021 09:10:20 +0200 Subject: [PATCH] dev-lang/boogie: add verison 2.9.6 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Package-Manager: Portage-3.0.20, Repoman-3.0.3 Signed-off-by: Maciej Barć --- dev-lang/boogie/Manifest | 1 + dev-lang/boogie/boogie-2.9.6.ebuild | 64 +++++++++++++++++++++++++++++ dev-lang/boogie/metadata.xml | 24 +++++++++++ 3 files changed, 89 insertions(+) create mode 100644 dev-lang/boogie/Manifest create mode 100644 dev-lang/boogie/boogie-2.9.6.ebuild create mode 100644 dev-lang/boogie/metadata.xml diff --git a/dev-lang/boogie/Manifest b/dev-lang/boogie/Manifest new file mode 100644 index 0000000..a71dd87 --- /dev/null +++ b/dev-lang/boogie/Manifest @@ -0,0 +1 @@ +DIST boogie-2.9.6.tar.gz 1508725 BLAKE2B 6226789a95d5a762db27b386eb1e6e3fdd4ff541f43bb6ae2a66bed2d2eb35cd0d948a9235d9b60f9c9538ab3a1701f36c601f834c177585c021e7900052071c SHA512 40ab3fd259031a4006279b16ca2912bfbf898cd8e283bb8900a74a31cde2fec2c0a0fc787a94164cbdcc76e61de83d8afcecb876fe77db60de636c2864b827e1 diff --git a/dev-lang/boogie/boogie-2.9.6.ebuild b/dev-lang/boogie/boogie-2.9.6.ebuild new file mode 100644 index 0000000..485a0c1 --- /dev/null +++ b/dev-lang/boogie/boogie-2.9.6.ebuild @@ -0,0 +1,64 @@ +# Copyright 1999-2021 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +DOTNET_FRAMEWORK="5.0" + +DESCRIPTION="Intermediate verification language built on .NET" +HOMEPAGE="https://github.com/boogie-org/boogie" + +if [[ "${PV}" == *9999* ]]; then + inherit git-r3 + EGIT_REPO_URI="https://github.com/boogie-org/${PN}.git" +else + SRC_URI="https://github.com/boogie-org/${PN}/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz" + KEYWORDS="~amd64" +fi + +# TODO: src_test +RESTRICT="network-sandbox test" +LICENSE="MIT" +SLOT="0" +IUSE="debug" + +DEPEND=" + virtual/dotnet-sdk:${DOTNET_FRAMEWORK} +" +RDEPEND=" + ${DEPEND} + sci-mathematics/z3 +" + +# Generated via dotnet +QA_PREBUILT="usr/share/boogie/BoogieDriver" + +src_prepare() { + if use debug; then + DOTNET_CONFIGURATION="Debug" + else + DOTNET_CONFIGURATION="Release" + fi + export DOTNET_CONFIGURATION + einfo "DOTNET_CONFIGURATION=${DOTNET_CONFIGURATION}" + + default +} + +src_configure() { + dotnet restore --no-cache ./Source/Boogie.sln || + die "dotnet restore filed" +} + +src_compile() { + dotnet build --configuration "${DOTNET_CONFIGURATION}" ./Source/Boogie.sln || + die "dotnet build failed" +} + +src_install() { + insinto /usr/share/${PN} + doins -r ./Source/BoogieDriver/bin/${DOTNET_CONFIGURATION}/net${DOTNET_FRAMEWORK}/* + + fperms +x /usr/share/${PN}/BoogieDriver + dosym ../share/${PN}/BoogieDriver /usr/bin/${PN} +} diff --git a/dev-lang/boogie/metadata.xml b/dev-lang/boogie/metadata.xml new file mode 100644 index 0000000..10a5d44 --- /dev/null +++ b/dev-lang/boogie/metadata.xml @@ -0,0 +1,24 @@ + + + + + + xgqt@riseup.net + Maciej Barć + + + 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. + + + https://github.com/boogie-org/boogie/issues + boogie-org/boogie + +