# 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
"

LICENSE="MIT"
SLOT="0"
KEYWORDS="~amd64"
IUSE="debug test"
RESTRICT="!test? ( test )"

BDEPEND="
	dev-libs/icu
	virtual/dotnet-sdk:${DOTNET_COMPAT}
"
RDEPEND="
	${BDEPEND}
	sci-mathematics/z3
"
BDEPEND+="
	test? (
		dev-python/lit
		dev-python/OutputCheck
	)
"

# Generated by dotnet.
QA_PREBUILT="/usr/share/boogie/BoogieDriver"

src_prepare() {
	export DOTNET_CLI_TELEMETRY_OPTOUT=1
	export DOTNET_NOLOGO=1
	export DOTNET_CONFIGURATION=$(usex debug Debug Release)
	export DOTNET_OUTPUT="${WORKDIR}"/${P}_net${DOTNET_COMPAT}_${DOTNET_CONFIGURATION}/${PN}
	export NUGET_PACKAGES="${S}"/Source/nuget_packages

	default

	# Remove bad tests.
	local bad_tests=(
		civl/inductive-sequentialization/BroadcastConsensus.bpl
		livevars/bla1.bpl
		prover/cvc5.bpl
		test0/MaxKeepGoingSplits.bpl
		test15/CaptureInlineUnroll.bpl
		test15/CaptureState.bpl
		test15/CommonVariablesPruning.bpl
	)
	local bad_test
	for bad_test in ${bad_tests[@]} ; do
		rm "${S}"/Test/${bad_test} || die
	done

	# Update the boogieBinary variable.
	sed "/^boogieBinary/s|= .*|= '${DOTNET_OUTPUT}/BoogieDriver.dll'|" \
		-i "${S}"/Test/lit.site.cfg || die "failed to update lit.site.cfg"
}

src_configure() {
	edob dotnet restore "${S}"/Source \
		--source "${NUGET_PACKAGES}" -p:TargetFramework=net${DOTNET_COMPAT}
}

src_compile() {
	local myopts=(
		--configuration ${DOTNET_CONFIGURATION}
		--no-restore
		--no-self-contained
		--nologo
		--output "${DOTNET_OUTPUT}"
		-consoleLoggerParameters:ErrorsOnly
		-maxCpuCount:$(makeopts_jobs)
	)
	edob dotnet build ${myopts[@]} "${S}"/Source
}

src_test() {
	lit "${S}"/Test || die "tests failed"
}

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
}