Compare commits
No commits in common. "cadef1c88d2651757dc7c1a92406825852be8144" and "83e700cc02c82500784202ca0a006c61586a6411" have entirely different histories.
cadef1c88d
...
83e700cc02
@ -1 +0,0 @@
|
|||||||
DIST boogie-2.9.6.tar.gz 1508725 BLAKE2B 6226789a95d5a762db27b386eb1e6e3fdd4ff541f43bb6ae2a66bed2d2eb35cd0d948a9235d9b60f9c9538ab3a1701f36c601f834c177585c021e7900052071c SHA512 40ab3fd259031a4006279b16ca2912bfbf898cd8e283bb8900a74a31cde2fec2c0a0fc787a94164cbdcc76e61de83d8afcecb876fe77db60de636c2864b827e1
|
|
@ -1,64 +0,0 @@
|
|||||||
# 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}
|
|
||||||
}
|
|
@ -1,24 +0,0 @@
|
|||||||
<?xml version="1.0" encoding="UTF-8"?>
|
|
||||||
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
|
|
||||||
|
|
||||||
<pkgmetadata>
|
|
||||||
<maintainer type="person">
|
|
||||||
<email>xgqt@riseup.net</email>
|
|
||||||
<name>Maciej Barć</name>
|
|
||||||
</maintainer>
|
|
||||||
<longdescription lang="en">
|
|
||||||
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>
|
|
@ -3,7 +3,7 @@
|
|||||||
|
|
||||||
EAPI=8
|
EAPI=8
|
||||||
|
|
||||||
DOTNET_FRAMEWORK="5.0"
|
DOTNET="5.0"
|
||||||
|
|
||||||
DESCRIPTION="Verification-aware programming language"
|
DESCRIPTION="Verification-aware programming language"
|
||||||
HOMEPAGE="https://dafny-lang.github.io/dafny/"
|
HOMEPAGE="https://dafny-lang.github.io/dafny/"
|
||||||
@ -22,12 +22,13 @@ LICENSE="MIT"
|
|||||||
SLOT="0"
|
SLOT="0"
|
||||||
IUSE="debug"
|
IUSE="debug"
|
||||||
|
|
||||||
|
# TODO: add dev-java/gradle when available
|
||||||
BDEPEND="
|
BDEPEND="
|
||||||
|| ( dev-java/gradle-bin dev-java/gradle )
|
dev-java/gradle-bin
|
||||||
"
|
"
|
||||||
DEPEND="
|
DEPEND="
|
||||||
>=virtual/jdk-1.8.0:*
|
>=virtual/jdk-1.8.0:*
|
||||||
virtual/dotnet-sdk:${DOTNET_FRAMEWORK}
|
virtual/dotnet-sdk:${DOTNET}
|
||||||
"
|
"
|
||||||
RDEPEND="
|
RDEPEND="
|
||||||
${DEPEND}
|
${DEPEND}
|
||||||
@ -42,31 +43,21 @@ DAFNY_EXES="
|
|||||||
|
|
||||||
QA_PREBUILT="${DAFNY_EXES}"
|
QA_PREBUILT="${DAFNY_EXES}"
|
||||||
|
|
||||||
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/Dafny.sln ||
|
|
||||||
die "dotnet restore filed"
|
|
||||||
}
|
|
||||||
|
|
||||||
src_compile() {
|
src_compile() {
|
||||||
dotnet build --configuration "${DOTNET_CONFIGURATION}" ./Source/Dafny.sln ||
|
local configuration
|
||||||
|
if use debug; then
|
||||||
|
configuration="Debug"
|
||||||
|
else
|
||||||
|
configuration="Release"
|
||||||
|
fi
|
||||||
|
|
||||||
|
dotnet build --configuration "${configuration}" ./Source/Dafny.sln ||
|
||||||
die "dotnet build failed"
|
die "dotnet build failed"
|
||||||
}
|
}
|
||||||
|
|
||||||
src_install() {
|
src_install() {
|
||||||
insinto /usr/share/${PN}
|
insinto /usr/share/${PN}
|
||||||
doins -r ./Binaries/net${DOTNET_FRAMEWORK}/*
|
doins -r ./Binaries/net${DOTNET}/*
|
||||||
|
|
||||||
local exe
|
local exe
|
||||||
for exe in ${DAFNY_EXES}; do
|
for exe in ${DAFNY_EXES}; do
|
||||||
|
Loading…
Reference in New Issue
Block a user