summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaciej Barć <xgqt@gentoo.org>2024-06-07 13:51:20 +0200
committerMaciej Barć <xgqt@gentoo.org>2024-06-07 14:57:47 +0200
commit6ba5a1b1de27940507492aeeaa8ed79d1e3cab45 (patch)
treea35841d6992e78869aebc7a4e1a912aa89ebd76a /dev-lang/dafny
parentapp-shells/fsh: bump DOTNET_PKG_COMPAT to 8.0 (diff)
downloadgentoo-6ba5a1b1de27940507492aeeaa8ed79d1e3cab45.tar.gz
gentoo-6ba5a1b1de27940507492aeeaa8ed79d1e3cab45.tar.bz2
gentoo-6ba5a1b1de27940507492aeeaa8ed79d1e3cab45.zip
dev-lang/dafny: drop old 4.5.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Diffstat (limited to 'dev-lang/dafny')
-rw-r--r--dev-lang/dafny/Manifest1
-rw-r--r--dev-lang/dafny/dafny-4.5.0.ebuild624
2 files changed, 0 insertions, 625 deletions
diff --git a/dev-lang/dafny/Manifest b/dev-lang/dafny/Manifest
index c44f81bc785e..133f085036b5 100644
--- a/dev-lang/dafny/Manifest
+++ b/dev-lang/dafny/Manifest
@@ -15,7 +15,6 @@ DIST castle.core.4.4.0.nupkg 916004 BLAKE2B 7404f946c140bc4c22132282a4a12694328b
DIST commandlineparser.2.8.0.nupkg 475554 BLAKE2B e55eda3a96441169220e5b081f432d8445d719cbcf8e86527920d44085e6e97934e20aa0266bc5dbdc16ba1a6daa6ece55bc2c63266c9d733ab4992f2fe3e0a1 SHA512 8c276513dfe91e5bc72cfb3b96a0d24411ee3bd2e9832d423f6ade3f3964a011dbb977ca90601750fa133a0a25fe72f66955be7f69a72f5d6b73c7f313094b5f
DIST commandlineparser.2.9.1.nupkg 496069 BLAKE2B e2c4b38841f83d6bc10432b8055af90369f1fe0a10105a58b51b44cd48e5d84cb0b5e4b19f444d8c81b38646a62c7c4d11cbd710e92fea68be3ebea6ab98e3f1 SHA512 4f364e45c9668c7e7cc6a922b488f3fa523033c20d7a432694f0a6af05ce528ea0481d8375e2f4f1032c6990347b4803ce9a0e48068c6fe15ec46fb1254f085d
DIST coverlet.collector.3.2.0.nupkg 2209480 BLAKE2B 175bcfcb9d6e5177d44f2d607f2411cbe77d6009d096bbc84372e33d7be972d3e39ec39d7f2669b4b91f4bcf44f6ddd46bc91541c0cc4843426e2dd1073bf5c2 SHA512 b63d02a5d3233805b42f0b8cc76f40c8d9f5a0117beb6bdb2ab147f5521bb99919b29d51ff91767ce0bfcab92d25fc8fe794133cadc60da3e009ae18d10fc920
-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
diff --git a/dev-lang/dafny/dafny-4.5.0.ebuild b/dev-lang/dafny/dafny-4.5.0.ebuild
deleted file mode 100644
index c20da32b0db8..000000000000
--- a/dev-lang/dafny/dafny-4.5.0.ebuild
+++ /dev/null
@@ -1,624 +0,0 @@
-# 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
- 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
- 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)"
- )
- edo 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
-}