dev-lang/dafny: bump to 4.6.0

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

2 files changed, 628 insertions, 0 deletions

diff --git a/dev-lang/dafny/Manifest b/dev-lang/dafny/Manifest
index a020a031eeda..c408c2033349 100644
--- a/dev-lang/dafny/Manifest
+++ b/dev-lang/dafny/Manifest
@@ -29,6 +29,7 @@ DIST commandlineparser.2.9.1.nupkg 496069 BLAKE2B e2c4b38841f83d6bc10432b8055af9
 DIST coverlet.collector.3.2.0.nupkg 2209480 BLAKE2B 175bcfcb9d6e5177d44f2d607f2411cbe77d6009d096bbc84372e33d7be972d3e39ec39d7f2669b4b91f4bcf44f6ddd46bc91541c0cc4843426e2dd1073bf5c2 SHA512 b63d02a5d3233805b42f0b8cc76f40c8d9f5a0117beb6bdb2ab147f5521bb99919b29d51ff91767ce0bfcab92d25fc8fe794133cadc60da3e009ae18d10fc920
 DIST dafny-4.4.0.tar.gz 6241907 BLAKE2B 43f5b6bed5ea0bc6f8de04650b2f97c0092df1df47aba9bf0c6b9210677077427c67cc80364f659305b7d851c178439a1536864dfb7c6396b4ac6517789fc83d SHA512 33789f10b75a1946aab552f11f40296682156bab7cb08cae431f00f6fdb6b12d3211ec2f423a42adb78a3245b19ab8f772dafca4d1448cb30077268680f73534
 DIST dafny-4.5.0.tar.gz 6365137 BLAKE2B 6233107e680e04ecc5a0d730bab4d5f2228ff04f9d83fe33688731c4226ae03b06a2c08447beda025e2e34e7d92bf6fbb57de5b6913e8cde9f61ae255d09722d SHA512 d56ba0a28bb235ad2c4baba526b4de1757a6574b9d04a195e541189ba5c24a82a7ca4d3ebbcc50244b7f35043aa80101210568f20656f21169c4cf42c41abce0
+DIST dafny-4.6.0.tar.gz 6373177 BLAKE2B 9348a9b170dd694885efe4682f05abe60240e6f7df7bde7bb53e8955c1c75a332ca6e7d6d6f38eb1aa9a83a9a5dfccea13b7683e99873c1fce12181d47679548 SHA512 abac500a27a811b434d32036ff7d877dd337a0a5917a07a7ac1fceffb1dd5d493bd07b7d518875243674b7919862a25f628fe62052983a8ff8f1450669c49b69
 DIST diffplex.1.7.0.nupkg 69699 BLAKE2B 9c7d6eab09e7df1d791183bbfc4cc46b7bea8dd4b5d09fd3e7e3dc1734e6a8973f92a34387e1a2a0e3a4cbf11ffb89f8138844b2b46d2e94010932ed47158911 SHA512 a0f7a30c59889d71eba97db9bda2efbf1b458ca439d129b52ba3eae32626325e73ec13d46018603a81a33cf18a25a5b08a1b2e6a89c7e716faa47eb9db6d6474
 DIST humanizer.core.2.2.0.nupkg 104728 BLAKE2B 6c383abbbed9250f2a7eeec4478ead8f23ad53aa62a5b0f22e71fed9157aa6644a9a7518842d637885b7b63a4300754e1a7e9f3f9968725607ad30bf18e27a21 SHA512 e232459f914c8e7fc3f8dee69a85e66beb8c44515d4c83a976ee24084a91f32aae61c6f845ff38edcae02d0bcab44f9ec253277dccf2f4ae7e82235047bc6ade
 DIST jetbrains.annotations.2021.1.0.nupkg 122595 BLAKE2B 59b994b58df9c4ef12d130543ae85ae0a368b92fae8c1d106675bcb4a55da9a13ee6da5fd5940b51c2a101470226007b05a1670b085d0f2f0b66f143e67f3051 SHA512 3b17599f6fc4413dd3811a32216f742596da5c6d8709134d85d292cd28ace7dc72aecef8a2bf64a5dfd31796787468e70e3936ea2eb9ed0505c7c6130d66db17
diff --git a/dev-lang/dafny/dafny-4.6.0.ebuild b/dev-lang/dafny/dafny-4.6.0.ebuild
new file mode 100644
index 000000000000..ca5c0f6861e7
--- /dev/null
+++ b/dev-lang/dafny/dafny-4.6.0.ebuild
@@ -0,0 +1,627 @@
+# Copyright 1999-2024 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+PYTHON_COMPAT=( python3_{10..12} )
+
+DOTNET_PKG_COMPAT=6.0
+NUGETS="
+boogie.abstractinterpretation@3.1.3
+boogie.basetypes@3.1.3
+boogie.codecontractsextender@3.1.3
+boogie.concurrency@3.1.3
+boogie.core@3.1.3
+boogie.executionengine@3.1.3
+boogie.graph@3.1.3
+boogie.houdini@3.1.3
+boogie.model@3.1.3
+boogie.provers.smtlib@3.1.3
+boogie.vcexpr@3.1.3
+boogie.vcgeneration@3.1.3
+castle.core@4.4.0
+commandlineparser@2.8.0
+commandlineparser@2.9.1
+coverlet.collector@3.2.0
+diffplex@1.7.0
+humanizer.core@2.2.0
+jetbrains.annotations@2021.1.0
+mediatr@8.1.0
+microsoft.bcl.asyncinterfaces@1.1.1
+microsoft.bcl.asyncinterfaces@5.0.0
+microsoft.bcl.asyncinterfaces@6.0.0
+microsoft.build.framework@17.0.0
+microsoft.build.locator@1.4.1
+microsoft.build.tasks.core@17.0.0
+microsoft.build.utilities.core@17.0.0
+microsoft.build@17.0.0
+microsoft.codeanalysis.analyzers@3.0.0
+microsoft.codeanalysis.analyzers@3.3.2
+microsoft.codeanalysis.common@3.7.0
+microsoft.codeanalysis.common@4.0.1
+microsoft.codeanalysis.csharp.workspaces@4.0.1
+microsoft.codeanalysis.csharp@3.7.0
+microsoft.codeanalysis.csharp@4.0.1
+microsoft.codeanalysis.visualbasic.workspaces@4.0.1
+microsoft.codeanalysis.visualbasic@4.0.1
+microsoft.codeanalysis.workspaces.common@4.0.1
+microsoft.codeanalysis.workspaces.msbuild@4.0.1
+microsoft.codeanalysis@4.0.1
+microsoft.codecoverage@16.11.0
+microsoft.codecoverage@16.9.4
+microsoft.codecoverage@17.1.0
+microsoft.csharp@4.0.1
+microsoft.dotnet.platformabstractions@2.0.4
+microsoft.extensions.configuration.abstractions@2.0.0
+microsoft.extensions.configuration.abstractions@5.0.0
+microsoft.extensions.configuration.binder@2.0.0
+microsoft.extensions.configuration.binder@5.0.0
+microsoft.extensions.configuration.commandline@5.0.0
+microsoft.extensions.configuration.fileextensions@5.0.0
+microsoft.extensions.configuration.json@5.0.0
+microsoft.extensions.configuration@2.0.0
+microsoft.extensions.configuration@5.0.0
+microsoft.extensions.dependencyinjection.abstractions@2.0.0
+microsoft.extensions.dependencyinjection.abstractions@5.0.0
+microsoft.extensions.dependencyinjection@2.0.0
+microsoft.extensions.dependencyinjection@5.0.0
+microsoft.extensions.dependencymodel@2.0.4
+microsoft.extensions.fileproviders.abstractions@5.0.0
+microsoft.extensions.fileproviders.physical@5.0.0
+microsoft.extensions.filesystemglobbing@5.0.0
+microsoft.extensions.logging.abstractions@2.0.0
+microsoft.extensions.logging.abstractions@5.0.0
+microsoft.extensions.logging.configuration@5.0.0
+microsoft.extensions.logging.console@5.0.0
+microsoft.extensions.logging@2.0.0
+microsoft.extensions.logging@5.0.0
+microsoft.extensions.options.configurationextensions@2.0.0
+microsoft.extensions.options.configurationextensions@5.0.0
+microsoft.extensions.options@2.0.0
+microsoft.extensions.options@5.0.0
+microsoft.extensions.primitives@2.0.0
+microsoft.extensions.primitives@5.0.0
+microsoft.net.stringtools@1.0.0
+microsoft.net.test.sdk@16.11.0
+microsoft.net.test.sdk@16.9.4
+microsoft.net.test.sdk@17.1.0
+microsoft.netcore.platforms@1.0.1
+microsoft.netcore.platforms@1.1.0
+microsoft.netcore.platforms@2.1.2
+microsoft.netcore.platforms@3.0.0
+microsoft.netcore.platforms@3.1.0
+microsoft.netcore.targets@1.0.1
+microsoft.netcore.targets@1.1.0
+microsoft.netframework.referenceassemblies.net452@1.0.2
+microsoft.netframework.referenceassemblies@1.0.2
+microsoft.testplatform.extensions.trxlogger@17.9.0
+microsoft.testplatform.objectmodel@16.11.0
+microsoft.testplatform.objectmodel@16.9.4
+microsoft.testplatform.objectmodel@17.1.0
+microsoft.testplatform.objectmodel@17.9.0
+microsoft.testplatform.testhost@16.11.0
+microsoft.testplatform.testhost@16.9.4
+microsoft.testplatform.testhost@17.1.0
+microsoft.testplatform.testhost@17.9.0
+microsoft.visualstudio.threading.analyzers@16.7.56
+microsoft.visualstudio.threading@16.7.56
+microsoft.visualstudio.validation@15.5.31
+microsoft.win32.primitives@4.3.0
+microsoft.win32.registry@4.3.0
+microsoft.win32.registry@4.6.0
+microsoft.win32.systemevents@4.7.0
+microsoft.win32.systemevents@6.0.0
+moq@4.16.1
+nerdbank.streams@2.6.81
+netstandard.library@1.6.1
+netstandard.library@2.0.3
+newtonsoft.json@11.0.2
+newtonsoft.json@13.0.1
+newtonsoft.json@9.0.1
+nuget.frameworks@5.0.0
+nuget.frameworks@5.11.0
+omnisharp.extensions.jsonrpc.generators@0.19.5
+omnisharp.extensions.jsonrpc.testing@0.19.5
+omnisharp.extensions.jsonrpc@0.19.5
+omnisharp.extensions.languageclient@0.19.5
+omnisharp.extensions.languageprotocol.testing@0.19.5
+omnisharp.extensions.languageprotocol@0.19.5
+omnisharp.extensions.languageserver.shared@0.19.5
+omnisharp.extensions.languageserver@0.19.5
+rangetree@3.0.1
+runtime.any.system.collections@4.3.0
+runtime.any.system.diagnostics.tools@4.3.0
+runtime.any.system.diagnostics.tracing@4.3.0
+runtime.any.system.globalization.calendars@4.3.0
+runtime.any.system.globalization@4.3.0
+runtime.any.system.io@4.3.0
+runtime.any.system.reflection.extensions@4.3.0
+runtime.any.system.reflection.primitives@4.3.0
+runtime.any.system.reflection@4.3.0
+runtime.any.system.resources.resourcemanager@4.3.0
+runtime.any.system.runtime.handles@4.3.0
+runtime.any.system.runtime.interopservices@4.3.0
+runtime.any.system.runtime@4.3.0
+runtime.any.system.text.encoding.extensions@4.3.0
+runtime.any.system.text.encoding@4.3.0
+runtime.any.system.threading.tasks@4.3.0
+runtime.any.system.threading.timer@4.3.0
+runtime.debian.8-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.fedora.23-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.fedora.24-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.native.system.io.compression@4.3.0
+runtime.native.system.net.http@4.3.0
+runtime.native.system.security.cryptography.apple@4.3.0
+runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.native.system@4.0.0
+runtime.native.system@4.3.0
+runtime.opensuse.13.2-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.opensuse.42.1-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.osx.10.10-x64.runtime.native.system.security.cryptography.apple@4.3.0
+runtime.osx.10.10-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.rhel.7-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.ubuntu.14.04-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.ubuntu.16.04-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.ubuntu.16.10-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.unix.microsoft.win32.primitives@4.3.0
+runtime.unix.system.console@4.3.0
+runtime.unix.system.diagnostics.debug@4.3.0
+runtime.unix.system.io.filesystem@4.3.0
+runtime.unix.system.net.primitives@4.3.0
+runtime.unix.system.net.sockets@4.3.0
+runtime.unix.system.private.uri@4.3.0
+runtime.unix.system.runtime.extensions@4.3.0
+serilog.extensions.logging@3.0.1
+serilog.settings.configuration@3.1.0
+serilog.sinks.debug@2.0.0
+serilog.sinks.file@5.0.0
+serilog.sinks.inmemory@0.11.0
+serilog@2.12.0
+system.appcontext@4.1.0
+system.appcontext@4.3.0
+system.buffers@4.3.0
+system.buffers@4.4.0
+system.codedom@4.4.0
+system.collections.concurrent@4.3.0
+system.collections.immutable@1.5.0
+system.collections.immutable@1.7.0
+system.collections.immutable@1.7.1
+system.collections.immutable@5.0.0
+system.collections.nongeneric@4.3.0
+system.collections.specialized@4.3.0
+system.collections@4.0.11
+system.collections@4.3.0
+system.commandline@2.0.0-beta4.22272.1
+system.componentmodel.primitives@4.3.0
+system.componentmodel.typeconverter@4.3.0
+system.componentmodel@4.3.0
+system.composition.attributedmodel@1.0.31
+system.composition.convention@1.0.31
+system.composition.hosting@1.0.31
+system.composition.runtime@1.0.31
+system.composition.typedparts@1.0.31
+system.composition@1.0.31
+system.configuration.configurationmanager@4.7.0
+system.configuration.configurationmanager@6.0.0
+system.console@4.3.0
+system.diagnostics.debug@4.0.11
+system.diagnostics.debug@4.3.0
+system.diagnostics.diagnosticsource@4.3.0
+system.diagnostics.tools@4.0.1
+system.diagnostics.tools@4.3.0
+system.diagnostics.tracesource@4.3.0
+system.diagnostics.tracing@4.3.0
+system.drawing.common@4.7.0
+system.drawing.common@6.0.0
+system.dynamic.runtime@4.0.11
+system.dynamic.runtime@4.3.0
+system.globalization.calendars@4.3.0
+system.globalization.extensions@4.3.0
+system.globalization@4.0.11
+system.globalization@4.3.0
+system.io.compression.zipfile@4.3.0
+system.io.compression@4.3.0
+system.io.filesystem.primitives@4.0.1
+system.io.filesystem.primitives@4.3.0
+system.io.filesystem@4.0.1
+system.io.filesystem@4.3.0
+system.io.pipelines@4.7.3
+system.io.pipelines@5.0.1
+system.io@4.1.0
+system.io@4.3.0
+system.linq.async@6.0.1
+system.linq.expressions@4.1.0
+system.linq.expressions@4.3.0
+system.linq@4.1.0
+system.linq@4.3.0
+system.memory@4.5.3
+system.memory@4.5.4
+system.net.http@4.3.0
+system.net.nameresolution@4.3.0
+system.net.primitives@4.3.0
+system.net.sockets@4.3.0
+system.net.websockets@4.3.0
+system.numerics.vectors@4.4.0
+system.objectmodel@4.0.12
+system.objectmodel@4.3.0
+system.private.uri@4.3.0
+system.reactive@4.4.1
+system.reflection.emit.ilgeneration@4.0.1
+system.reflection.emit.ilgeneration@4.3.0
+system.reflection.emit.lightweight@4.0.1
+system.reflection.emit.lightweight@4.3.0
+system.reflection.emit@4.0.1
+system.reflection.emit@4.3.0
+system.reflection.extensions@4.0.1
+system.reflection.extensions@4.3.0
+system.reflection.metadata@1.6.0
+system.reflection.metadata@5.0.0
+system.reflection.primitives@4.0.1
+system.reflection.primitives@4.3.0
+system.reflection.typeextensions@4.1.0
+system.reflection.typeextensions@4.3.0
+system.reflection@4.1.0
+system.reflection@4.3.0
+system.resources.extensions@4.6.0
+system.resources.resourcemanager@4.0.1
+system.resources.resourcemanager@4.3.0
+system.runtime.caching@6.0.0
+system.runtime.compilerservices.unsafe@4.4.0
+system.runtime.compilerservices.unsafe@4.5.2
+system.runtime.compilerservices.unsafe@4.7.0
+system.runtime.compilerservices.unsafe@4.7.1
+system.runtime.compilerservices.unsafe@5.0.0
+system.runtime.extensions@4.1.0
+system.runtime.extensions@4.3.0
+system.runtime.handles@4.0.1
+system.runtime.handles@4.3.0
+system.runtime.interopservices.runtimeinformation@4.0.0
+system.runtime.interopservices.runtimeinformation@4.3.0
+system.runtime.interopservices@4.1.0
+system.runtime.interopservices@4.3.0
+system.runtime.numerics@4.3.0
+system.runtime.serialization.primitives@4.1.1
+system.runtime@4.1.0
+system.runtime@4.3.0
+system.security.accesscontrol@4.6.0
+system.security.accesscontrol@4.7.0
+system.security.accesscontrol@6.0.0
+system.security.claims@4.3.0
+system.security.cryptography.algorithms@4.3.0
+system.security.cryptography.cng@4.3.0
+system.security.cryptography.cng@4.7.0
+system.security.cryptography.csp@4.3.0
+system.security.cryptography.encoding@4.3.0
+system.security.cryptography.openssl@4.3.0
+system.security.cryptography.pkcs@4.7.0
+system.security.cryptography.primitives@4.3.0
+system.security.cryptography.protecteddata@4.7.0
+system.security.cryptography.protecteddata@6.0.0
+system.security.cryptography.x509certificates@4.3.0
+system.security.cryptography.xml@4.7.0
+system.security.permissions@4.7.0
+system.security.permissions@6.0.0
+system.security.principal.windows@4.3.0
+system.security.principal.windows@4.6.0
+system.security.principal.windows@4.7.0
+system.security.principal@4.3.0
+system.text.encoding.codepages@4.0.1
+system.text.encoding.codepages@4.5.1
+system.text.encoding.extensions@4.0.11
+system.text.encoding.extensions@4.3.0
+system.text.encoding@4.0.11
+system.text.encoding@4.3.0
+system.text.json@4.7.0
+system.text.json@5.0.2
+system.text.regularexpressions@4.1.0
+system.text.regularexpressions@4.3.0
+system.threading.channels@4.7.1
+system.threading.tasks.dataflow@4.9.0
+system.threading.tasks.extensions@4.0.0
+system.threading.tasks.extensions@4.3.0
+system.threading.tasks.extensions@4.5.3
+system.threading.tasks.extensions@4.5.4
+system.threading.tasks@4.0.11
+system.threading.tasks@4.3.0
+system.threading.threadpool@4.3.0
+system.threading.timer@4.3.0
+system.threading@4.0.11
+system.threading@4.3.0
+system.windows.extensions@4.7.0
+system.windows.extensions@6.0.0
+system.xml.readerwriter@4.0.11
+system.xml.readerwriter@4.3.0
+system.xml.xdocument@4.0.11
+system.xml.xdocument@4.3.0
+system.xml.xmldocument@4.3.0
+tomlyn@0.16.2
+validation@2.4.18
+xunit.abstractions@2.0.2
+xunit.abstractions@2.0.3
+xunit.analyzers@0.10.0
+xunit.analyzers@1.0.0
+xunit.assert@2.4.1
+xunit.assert@2.4.2
+xunit.assertmessages@2.4.0
+xunit.core@2.4.1
+xunit.core@2.4.2
+xunit.extensibility.core@2.4.0
+xunit.extensibility.core@2.4.1
+xunit.extensibility.core@2.4.2
+xunit.extensibility.execution@2.4.0
+xunit.extensibility.execution@2.4.1
+xunit.extensibility.execution@2.4.2
+xunit.runner.visualstudio@2.4.3
+xunit.runner.visualstudio@2.5.1
+xunit.skippablefact@1.4.8
+xunit@2.4.1
+xunit@2.4.2
+"
+
+inherit check-reqs dotnet-pkg edo java-pkg-2 multiprocessing python-any-r1 optfeature
+
+DESCRIPTION="Dafny is a verification-aware programming language"
+HOMEPAGE="https://dafny.org/
+	https://github.com/dafny-lang/dafny/"
+
+if [[ "${PV}" == *9999* ]] ; then
+	inherit git-r3
+
+	EGIT_REPO_URI="https://github.com/dafny-lang/${PN}.git"
+else
+	SRC_URI="https://github.com/dafny-lang/${PN}/archive/v${PV}.tar.gz
+		-> ${P}.tar.gz"
+
+	KEYWORDS="~amd64"
+fi
+
+SRC_URI+="
+	${NUGET_URIS}
+	test? ( https://registry.npmjs.org/bignumber.js/-/bignumber.js-9.1.2.tgz )
+"
+
+LICENSE="MIT"
+SLOT="0"
+IUSE="test"
+RESTRICT="!test? ( test )"
+
+RDEPEND="
+	!dev-lang/dafny-bin
+	>=virtual/jre-1.8:*
+	sci-mathematics/z3
+"
+DEPEND="
+	>=virtual/jdk-1.8:*
+"
+BDEPEND="
+	${RDEPEND}
+	dev-dotnet/coco
+	test? (
+		${PYTHON_DEPS}
+		dev-go/go-tools
+		dev-lang/boogie
+		dev-lang/go
+		dev-python/OutputCheck
+		dev-python/lit
+		dev-python/psutil
+		net-libs/nodejs[npm]
+	)
+"
+
+CHECKREQS_DISK_BUILD="2G"
+DOTNET_PKG_PROJECTS=(
+	"${S}/Source/Dafny/Dafny.csproj"
+)
+
+PATCHES=(
+	"${FILESDIR}/${PN}-3.12.0-DafnyCore-csproj.patch"
+	"${FILESDIR}/${PN}-3.12.0-DafnyRuntime-csproj.patch"
+	"${FILESDIR}/${PN}-4.5.0-lit-config.patch"
+)
+
+DOCS=(
+	CODE_OF_CONDUCT.md
+	CONTRIBUTING.md
+	NOTICES.txt
+	README.md
+	RELEASE_NOTES.md
+	docs/DafnyCheatsheet.pdf
+	docs/DafnyRef/out/DafnyRef.pdf
+)
+
+TEST_S="${S}/Source/IntegrationTests/TestFiles/LitTests/LitTest"
+
+pkg_setup() {
+	# Clean the environment.
+	unset NPM_CONFIG_USERCONFIG
+
+	if [[ -n "${_JAVA_OPTIONS}" ]] ; then
+		ewarn "Cleaning _JAVA_OPTIONS because when set compile and test may fail"
+
+		unset _JAVA_OPTIONS
+	fi
+
+	check-reqs_pkg_setup
+	dotnet-pkg_pkg_setup
+	java-pkg-2_pkg_setup
+
+	# We need to set up Python only for running test tools (called via lit).
+	if use test ; then
+		python-any-r1_pkg_setup
+	fi
+}
+
+src_unpack() {
+	dotnet-pkg_src_unpack
+
+	if [[ -n "${EGIT_REPO_URI}" ]] ; then
+		git-r3_src_unpack
+	fi
+}
+
+src_prepare() {
+	# Using "for-each-compiler" will fail because of Cargo requiring network access.
+	while read -r test_file ; do
+		if grep "// RUN: %testDafnyForEachCompiler" "${test_file}" >/dev/null ; then
+			rm "${test_file}" || die "failed to remove test ${bad_test}"
+		fi
+	done < <(find "${TEST_S}" -type f -name "*.dfy")
+
+	# Remove bad tests (recursive).
+	local -a bad_tests=(
+		# Following tests fail:
+		VSComp2010/Problem2-Invert.dfy
+		auditor/TestAuditor.dfy
+		benchmarks/sequence-race/SequenceRace.dfy
+		cli/runArgument.dfy
+		comp/CoverageReport.dfy
+		concurrency/06-ThreadOwnership.dfy
+		dafny0/Fuel.legacy.dfy
+		dafny0/Stdin.dfy
+		dafny1/MoreInduction.dfy
+		dafny4/Lucas-up.legacy.dfy
+		dafny4/Primes.dfy
+		examples/Simple_compiler/Compiler.dfy
+		git-issues/git-issue-2026.dfy
+		git-issues/git-issue-2299.dfy
+		git-issues/git-issue-2301.dfy
+		git-issues/git-issue-505.dfy
+		metatests/InconsistentCompilerBehavior.dfy
+		metatests/TestBeyondVerifierExpect.dfy
+		separate-verification/assumptions.dfy
+		server/counterexample_none.transcript
+		triggers/emptyTrigger.dfy
+		unicodechars/DafnyTests/RunAllTestsOption.dfy
+		verification/isolate-assertions.dfy
+		verification/progress.dfy
+		vstte2012/Combinators.dfy
+		wishlist/exists-b-exists-not-b.dfy
+
+		# Following tests are very slow:
+		DafnyTests/RunAllTests/RunAllTestsOption.dfy
+		VSI-Benchmarks/b4.dfy
+		blogposts/TestGenerationNoInliningEnumerativeDefinitions.dfy
+		comp/BranchCoverage.dfy
+		comp/CompileWithArguments.dfy
+		comp/Extern.dfy
+		comp/MainMethod.dfy
+		comp/Print.dfy
+		comp/SequenceConcatOptimization.dfy
+		comp/compile1quiet/CompileRunQuietly.dfy
+		comp/compile1verbose/CompileAndThenRun.dfy
+		comp/compile3/JustRun.dfy
+		comp/manualcompile/ManualCompile.dfy
+		comp/replaceables/complex/user.dfy
+		concurrency/07-CounterThreadOwnership.dfy
+		concurrency/08-CounterNoTermination.dfy
+		concurrency/09-CounterNoStateMachine.dfy
+		concurrency/10-SequenceInvariant.dfy
+		concurrency/12-MutexLifetime-short.dfy
+		dafny0/RlimitMultiplier.dfy
+		dafny1/SchorrWaite.dfy
+		dafny2/SnapshotableTrees.dfy
+		dafny4/git-issue250.dfy
+		git-issues/git-issue-Main4.dfy
+		git-issues/git-issue-MainE.dfy
+		unicodechars/comp/CompileWithArguments.dfy
+	)
+	local bad_test
+	for bad_test in "${bad_tests[@]}" ; do
+		if [[ -f "${TEST_S}/${bad_test}" ]] ; then
+			rm "${TEST_S}/${bad_test}" || die "failed to remove test ${bad_test}"
+		else
+			ewarn "Test file ${bad_test} does not exist"
+		fi
+	done
+
+	dotnet-pkg_src_prepare
+
+	# Update lit's "lit.site.cfg" file.
+	local dotnet_exec="${DOTNET_PKG_EXECUTABLE} exec ${DOTNET_PKG_OUTPUT}"
+	local lit_config="${TEST_S}/lit.site.cfg"
+
+	sed -i "${lit_config}" \
+		-e "/^defaultDafnyExecutable/s|=.*|= '${dotnet_exec}/Dafny.dll '|" \
+		-e "/^dafnyExecutable/s|=.*|= '${dotnet_exec}/Dafny.dll '|" \
+		-e "/^defaultServerExecutable/s|=.*|= '${dotnet_exec}/DafnyServer.dll'|" \
+		-e "/^serverExecutable/s|=.*|= '${dotnet_exec}/DafnyServer.dll'|" \
+		-e "s|dotnet run |${DOTNET_PKG_EXECUTABLE} run |g" \
+		|| die "failed to update ${lit_config}"
+}
+
+src_compile () {
+	einfo "Building DafnyRuntimeJava JAR."
+	local dafny_runtime_java="${S}/Source/DafnyRuntime/DafnyRuntimeJava"
+	mkdir -p "${dafny_runtime_java}/build/libs/" || die
+	pushd "${dafny_runtime_java}/build" || die
+
+	ejavac -d ./ $(find "${dafny_runtime_java}/src/main" -type f -name "*.java")
+	edo jar cvf "DafnyRuntime-${PV}.jar" dafny/*
+
+	cp "DafnyRuntime-${PV}.jar" "${dafny_runtime_java}/build/libs/" || die
+	popd || die
+
+	# Build main dotnet package.
+	dotnet-pkg_src_compile
+
+	if use test ; then
+		# Build "TestDafny" without saving artifacts.
+		edotnet build										\
+				--configuration Debug						\
+				--no-self-contained							\
+				-maxCpuCount:$(makeopts_jobs)				\
+				"${S}/Source/TestDafny/TestDafny.csproj"
+	fi
+}
+
+src_test() {
+	# Dafny GOLang transpiler tests need "goimports" from "/usr/lib/go/bin".
+	local -x PATH="${EPREFIX}/usr/lib/go/bin:${PATH}"
+
+	einfo "Installing bignumber.js package required for tests using NodeJS."
+	local -a npm_opts=(
+		--audit false
+		--color false
+		--foreground-scripts
+		--offline
+		--progress false
+		--verbose
+	)
+	edob npm "${npm_opts[@]}" install "${DISTDIR}/bignumber.js-9.1.2.tgz"
+
+	einfo "Starting tests using the lit test tool."
+	local -a lit_opts=(
+		--order=lexical
+		--time-tests
+		--timeout 1800          # Let one test take no mere than half a hour.
+		--verbose
+		--workers="$(makeopts_jobs)"
+	)
+	edob lit "${lit_opts[@]}" "${TEST_S}"
+}
+
+src_install() {
+	dotnet-pkg-base_install
+
+	local -a dafny_exes=(
+		Dafny
+		DafnyDriver
+		DafnyLanguageServer
+		DafnyServer
+		TestDafny
+	)
+	local dafny_exe
+	for dafny_exe in "${dafny_exes[@]}" ; do
+		dotnet-pkg-base_dolauncher "/usr/share/${P}/${dafny_exe}" "${dafny_exe}"
+	done
+
+	dosym -r /usr/bin/Dafny /usr/bin/dafny
+	dosym -r /usr/bin/DafnyServer /usr/bin/dafny-server
+
+	einstalldocs
+}
+
+pkg_postinst() {
+	optfeature "Dafny GO language backend" dev-go/go-tools
+	optfeature "Dafny Rust language backend" virtual/rust
+}