commit: 105a71a5ce52f2fe24fcffeae2800b71e66ebea1
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sun Feb 9 13:19:38 2025 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sun Feb 9 20:50:52 2025 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=105a71a5
dev-lang/dafny: bump to 4.10.0
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
dev-lang/dafny/Manifest | 2 +
dev-lang/dafny/dafny-4.10.0.ebuild | 627 +++++++++++++++++++++++++++++++++++++
2 files changed, 629 insertions(+)
diff --git a/dev-lang/dafny/Manifest b/dev-lang/dafny/Manifest
index 54e8aefaecf0..a3ed1d78c6a8 100644
--- a/dev-lang/dafny/Manifest
+++ b/dev-lang/dafny/Manifest
@@ -55,6 +55,7 @@ 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.10.0.tar.gz 6815686 BLAKE2B
e6054cd38cbc4edcdb2e6848efd6f09df6b5be7abb22bd9e47d35c71a6d046aee4a10bdefe840d883151b66b4d8075053ba14b5f038d7b1b8104bf40ccc56791
SHA512
fcd3499e4a626db638d2cb1d9c3ed221b559d339171f316c937298ed4c916ddf548ec3a0168b85fbb442e51406040b084799f9770b85c5b836d925568e272cad
DIST dafny-4.8.0.tar.gz 6615281 BLAKE2B
d891a1955554b194e7af231eff9368549bd2686b43dc1aca8034df4502b7b57297a8384db990ca3268bf992ce2ea562d02d936617b0788a58705d2b0cd91aa98
SHA512
8194f2544b411e00874b174ae4036d6ff21e516e342b3ddd9bc00e70a8140037e5a35f10ef797336b1d4f471ea1596829f0d5446d6a93e436690753dc9b19a31
DIST dafny-4.8.1.tar.gz 6693520 BLAKE2B
4cceaba7aec5809c6f714bc5f79fd92656ec0c30e9188aecb5d153575ab06a244fbc248f91ae64e2e1e9ea15914ebc408ebf2ce197edeac8e021770499d3779f
SHA512
cfbeb9d36ee9f63c703048fb8497a54df040d96a3e9d5ee208bb2f6a0795416e49b34ec08052f568b7c50d0a892dc6139c01a2310adbd63d347ddec61c79b56b
DIST dafny-4.9.0.tar.gz 6733045 BLAKE2B
a13eb0716eb6449c8145b25261d97539b04a6310ba24f3dba30938adc46da99b52016e44683bd7521a66cb11e03b92972dee3da6377bc13c6f519f44a91d6c81
SHA512
3d7493467db5006df02fb912d562a7109b225e7eb33e36b02fcb4ddca8cb4353464f668d578017226a22ffed7dac10424dc8fbd73ee13c8108e3bde219562884
@@ -373,6 +374,7 @@ DIST system.xml.xdocument.4.0.11.nupkg 591353 BLAKE2B
8373fa19c6aafbe6e347db7bb1
DIST system.xml.xdocument.4.3.0.nupkg 591350 BLAKE2B
86f910cef36c056f4a9ea9dc26eea6e01070467d27ac80fb8a0af5e1a572ad5d2169e4f1297cd362fddc9e0309458dbd413fca85ef8e56f97781c218e594604a
SHA512
c2d9236a696daf23a29b530b9aa510fb813041685a1bb9a95845a51e61d870a0615e988b150f5be0d0896ef94b123e97f96c8a43ee815cf5b9897593986b1113
DIST system.xml.xmldocument.4.3.0.nupkg 285212 BLAKE2B
0d96ca356543e8e915597e0624dca42f0c7032a2ae9e380a6fba3fbee0dacb9e5f06017893b2b7a8b937dbb4de7d5665fa6648e3bf8df12e0d34e4075c125109
SHA512
22251b3f16de9aa06e091b24baea1b8c95752f0d22266faf34e1fb76b347b23f7910cdaf567058e23d06b7079961090ca70805070a2491add5da4d0271afd133
DIST tomlyn.0.16.2.nupkg 146842 BLAKE2B
5292d6abae6eb514d6a0cf7b69e9ab47599fc1540c83a9861985293267c8137f856a1ec573d7f3b327c9a383905de4572f54d03c889951227549cc1bb8979f78
SHA512
69a4f67cd9a9cf593f79fd8cc0530a030a24a9a04e5b67ba39460668e5125d6859f54f3a3d485ec1e8d0be996f14ef14fb9e380e63c6e648bd1141dc31c58141
+DIST tomlyn.0.17.0.nupkg 147066 BLAKE2B
d5507882a8e5f7bd7f2e30c3a4aab342046c0339b884b6527a9e616cd48c603aa97ed411a63cf1e92852994c9dc2768f35edb5854aa5b21f865b17783fc43ba5
SHA512
0dd5717101262fd7833cbb74ab5b95f0f39e39d2b32c90775d6e54359643d17d5c1675b9ef65260b01f5b89c81c3d446ae3bffd598b0a53e6b3a10149f9e01fb
DIST validation.2.4.18.nupkg 90984 BLAKE2B
3f319bd60a0b1d6b6d08188b1132c01fd417d7e205bc587edd7ffa0dfba4dc01b9e956df46ef03b0f909ff5b9a859a9620d1ededd8eef21fb6522aab2f12f1f2
SHA512
b49e4b992b40bb656821a7a6dd67fe464af14f0781cf677f58412d108678963f9f9347bd2e1091343c1aa522148ea187a25b45ef0eae5e7ffeb8f833396fcff2
DIST xunit.2.4.1.nupkg 20733 BLAKE2B
ee83156610dc4ade1f15c05d97725e1913a9dde04e474c11fe396c37df5d438ab934776e4660d3d139fe34949eb890dae67c0145d3815a8a25cc976b9d2cca7b
SHA512
3b0061a5ecfd49166f123aa27375956c00aedb0b22f6ee6a8be629cd583a0532f7476e51ffacad3385245139f1f9d4990c9dc850fc7ef7d097fd85e7c6b40058
DIST xunit.2.4.2.nupkg 25547 BLAKE2B
bc9bc5049e9feaa9b658ff11ad3ed277c43089b5c341768425d401b98f5ca212d3f3828232a58716f7ea75e39007fb8ee04498208afed60d28e91ecfff31f1d6
SHA512
f57b8d3bbd04cc285c7913b5697a1b00cf0d6f2c70e35a592d61c8c866d79f3f6a913fa933b39224484bba439e6eee0ab917bf66cd19cbcb1dc3731437556c48
diff --git a/dev-lang/dafny/dafny-4.10.0.ebuild
b/dev-lang/dafny/dafny-4.10.0.ebuild
new file mode 100644
index 000000000000..4943c4a1f162
--- /dev/null
+++ b/dev-lang/dafny/dafny-4.10.0.ebuild
@@ -0,0 +1,627 @@
+# Copyright 1999-2025 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+PYTHON_COMPAT=( python3_{11..13} )
+
+DOTNET_PKG_COMPAT="8.0"
+NUGETS="
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
+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
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
+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
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
+"
+
+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-lang/boogie-3.4.3
+ dev-go/go-tools
+ dev-lang/go
+ dev-python/outputcheck
+ dev-python/lit
+ dev-python/psutil
+ net-libs/nodejs[npm]
+ )
+"
+
+CHECKREQS_DISK_BUILD="2G"
+DOTNET_PKG_PROJECTS=( Source/Dafny/Dafny.csproj )
+TEST_S="${S}/Source/IntegrationTests/TestFiles/LitTests/LitTest"
+
+PATCHES=(
+ "${FILESDIR}/dafny-3.12.0-DafnyCore-csproj.patch"
+ "${FILESDIR}/dafny-3.12.0-DafnyRuntime-csproj.patch"
+ "${FILESDIR}/dafny-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
+)
+
+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() {
+ # Unpack manually to skip additional archives, eg "bignumber.js".
+ nuget_link-system-nugets
+ nuget_link-nuget-archives
+
+ if [[ -n "${EGIT_REPO_URI}" ]] ; then
+ git-r3_src_unpack
+ else
+ unpack "${P}.tar.gz"
+ fi
+}
+
+src_prepare() {
+ 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"
+
+ local -a lit_dotnet_run_opts=(
+ --configuration "${DOTNET_PKG_CONFIGURATION}"
+ --no-build
+ --no-restore
+ --no-self-contained
+ --runtime "${DOTNET_PKG_RUNTIME}"
+ )
+ sed -i "${lit_config}" \
+ -e "s|dotnet run |${DOTNET_PKG_EXECUTABLE} run
${lit_dotnet_run_opts[*]} |g" \
+ || die "failed to update ${lit_config}"
+
+ # 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=(
+ # Unsupported test build (and those that need network access):
+ comp/rust
+
+ # Following tests fail:
+ HigherOrderIntrinsicSpecification
+ VSComp2010
+ ast/function.dfy
+ auditor/TestAuditor.dfy
+ benchmarks
+ blogposts
+ c++
+ cli
+ comp
+ concurrency
+ dafny{0,1,3,4}
+ doofiles
+ examples
+ exports
+ git-issues
+ gomodule/{multimodule,publishedruntime,singlemodule}
+ lambdas
+ metatests
+ printing
+ pythonmodule
+ separate-verification
+ server
+ triggers
+ unicodecharsFalse
+ verification
+ vstte2012
+ wishlist
+ )
+ local bad_test=""
+ for bad_test in "${bad_tests[@]}" ; do
+ if [[ -e "${TEST_S}/${bad_test}" ]] ; then
+ rm -r "${TEST_S}/${bad_test}" \
+ || eerror "failed to remove test ${bad_test}"
+ else
+ ewarn "Test file ${bad_test} does not exist"
+ fi
+ done
+}
+
+src_configure() {
+ dotnet-pkg_src_configure
+
+ if use test ; then
+ dotnet-pkg-base_restore ./Source/TestDafny/TestDafny.csproj
+ fi
+}
+
+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")
+ edob 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
+
+ # Build "TestDafny" without saving artifacts.
+ if use test ; then
+ # This is where Dafny test suite expects to find compiled
sources.
+ rm -r ./Binaries || die
+ cp -r "${DOTNET_PKG_OUTPUT}" ./Binaries || die
+
+ local -a build_test_opts=(
+ --configuration "${DOTNET_PKG_CONFIGURATION}"
+ --no-restore
+ --no-self-contained
+ --runtime "${DOTNET_PKG_RUNTIME}"
+ -maxCpuCount:$(makeopts_jobs)
+ )
+ edotnet build "${build_test_opts[@]}"
./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
+ )
+ 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" dev-lang/rust dev-lang/rust-bin
+}