* [gentoo-commits] repo/gentoo:master commit in: dev-lang/dafny/, dev-lang/dafny/files/
@ 2023-12-13 17:17 Maciej Barć
0 siblings, 0 replies; 4+ messages in thread
From: Maciej Barć @ 2023-12-13 17:17 UTC (permalink / raw
To: gentoo-commits
commit: 4a647d38ea7fa3703a216d12e5c679b327d00583
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Wed Dec 13 12:05:55 2023 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Wed Dec 13 17:17:55 2023 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=4a647d38
dev-lang/dafny: bring Java support back
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
.../{dafny-4.4.0.ebuild => dafny-4.4.0-r1.ebuild} | 56 +++++++++++++++++-----
dev-lang/dafny/files/dafny-4.4.0-no-copy-jar.patch | 21 --------
.../dafny/files/dafny-4.4.0-no-output-jar.patch | 18 -------
3 files changed, 45 insertions(+), 50 deletions(-)
diff --git a/dev-lang/dafny/dafny-4.4.0.ebuild b/dev-lang/dafny/dafny-4.4.0-r1.ebuild
similarity index 93%
rename from dev-lang/dafny/dafny-4.4.0.ebuild
rename to dev-lang/dafny/dafny-4.4.0-r1.ebuild
index 50a6fd8da3c2..617b0a373ba8 100644
--- a/dev-lang/dafny/dafny-4.4.0.ebuild
+++ b/dev-lang/dafny/dafny-4.4.0-r1.ebuild
@@ -361,7 +361,7 @@ xunit@2.4.1
xunit@2.4.2
"
-inherit check-reqs dotnet-pkg edo multiprocessing python-any-r1
+inherit check-reqs dotnet-pkg edo java-pkg-2 multiprocessing python-any-r1
DESCRIPTION="Dafny is a verification-aware programming language"
HOMEPAGE="https://dafny.org/
@@ -390,8 +390,12 @@ 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
@@ -416,8 +420,6 @@ PATCHES=(
"${FILESDIR}/${PN}-3.12.0-DafnyRuntime-csproj.patch"
"${FILESDIR}/${PN}-4.4.0-lit-config.patch"
"${FILESDIR}/${PN}-4.4.0-lit-system-boogie.patch"
- "${FILESDIR}/${PN}-4.4.0-no-copy-jar.patch"
- "${FILESDIR}/${PN}-4.4.0-no-output-jar.patch"
)
DOCS=(
@@ -436,8 +438,15 @@ 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
@@ -459,41 +468,52 @@ src_prepare() {
if grep "// RUN: %testDafnyForEachCompiler" "${test_file}" >/dev/null ; then
rm "${test_file}" || die
fi
- done < <(find "${TEST_S}" -type f -name "*.dfy")
+ done < <(find "${TEST_S}" -type f -name "*.dfy")
# Remove bad tests (recursive).
local -a bad_tests=(
# Following tests fail:
- DafnyTests/TestAttribute.dfy
VSComp2010/Problem2-Invert.dfy
auditor/TestAuditor.dfy
benchmarks/sequence-race/SequenceRace.dfy
- comp/CoverageReport.dfy
dafny0/Fuel.legacy.dfy
dafny0/JavaUseRuntimeLib.dfy
dafny0/Stdin.dfy
dafny4/Lucas-up.legacy.dfy
- examples/Simple_compiler/Compiler.dfy
git-issues/git-issue-2026.dfy
git-issues/git-issue-2299.dfy
git-issues/git-issue-2301.dfy
- metatests/InconsistentCompilerBehavior.dfy
- metatests/TestBeyondVerifierExpect.dfy
separate-verification/assumptions.dfy
server/counterexample_none.transcript
- unicodechars/expectations/Expect.dfy
wishlist/exists-b-exists-not-b.dfy
# Following tests are very slow:
+ VSI-Benchmarks/b4.dfy
+ comp/CompileWithArguments.dfy
+ comp/MainMethod.dfy
+ comp/compile3/JustRun.dfy
+ concurrency/07-CounterThreadOwnership.dfy
+ concurrency/09-CounterNoStateMachine.dfy
+ concurrency/10-SequenceInvariant.dfy
+ concurrency/12-MutexLifetime-short.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
rm "${TEST_S}/${bad_test}" || die "failed to remove test ${bad_test}"
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 "/^defaultDafnyExecutable/s|=.*|= '${dotnet_exec}/Dafny.dll '|" \
-i "${lit_config}" || die "failed to update ${lit_config}"
sed "/^dafnyExecutable/s|=.*|= '${dotnet_exec}/Dafny.dll '|" \
@@ -506,8 +526,22 @@ src_prepare() {
-i "${lit_config}" || die "failed to update ${lit_config}"
sed "/^serverExecutable/s|=.*|= '${dotnet_exec}/DafnyServer.dll'|" \
-i "${lit_config}" || die "failed to update ${lit_config}"
+}
- dotnet-pkg_src_prepare
+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
}
src_test() {
diff --git a/dev-lang/dafny/files/dafny-4.4.0-no-copy-jar.patch b/dev-lang/dafny/files/dafny-4.4.0-no-copy-jar.patch
deleted file mode 100644
index 96ab9fc4a723..000000000000
--- a/dev-lang/dafny/files/dafny-4.4.0-no-copy-jar.patch
+++ /dev/null
@@ -1,21 +0,0 @@
---- a/Source/DafnyPipeline/DafnyPipeline.csproj
-+++ b/Source/DafnyPipeline/DafnyPipeline.csproj
-@@ -89,11 +89,6 @@
- <LinkBase>DafnyRuntimeJava</LinkBase>
- <CopyToOutputDirectory>Always</CopyToOutputDirectory>
- </EmbeddedResource>
-- <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntimeJava\build\libs\DafnyRuntime-4.4.0.jar">
-- <LogicalName>DafnyRuntime.jar</LogicalName>
-- <Link>DafnyRuntime.jar</Link>
-- <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
-- </EmbeddedResource>
- <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntime.cs">
- <LinkBase>DafnyRuntimeCsharp</LinkBase>
- <CopyToOutputDirectory>Always</CopyToOutputDirectory>
-@@ -128,4 +123,4 @@
- <EmbeddedResource Remove="..\DafnyRuntime\DafnyRuntimeRust\target\**"/>
- </ItemGroup>
-
--</Project>
-\ No newline at end of file
-+</Project>
diff --git a/dev-lang/dafny/files/dafny-4.4.0-no-output-jar.patch b/dev-lang/dafny/files/dafny-4.4.0-no-output-jar.patch
deleted file mode 100644
index 332fc4ffb49f..000000000000
--- a/dev-lang/dafny/files/dafny-4.4.0-no-output-jar.patch
+++ /dev/null
@@ -1,18 +0,0 @@
---- a/Source/DafnyRuntime/DafnyRuntime.csproj
-+++ b/Source/DafnyRuntime/DafnyRuntime.csproj
-@@ -28,15 +28,5 @@
- <PropertyGroup>
- <DafnyRuntimeJar>DafnyRuntimeJava/build/libs/DafnyRuntime-4.4.0.jar</DafnyRuntimeJar>
- </PropertyGroup>
-- <Target Name="BuildDafnyRuntimeJar" AfterTargets="ResolveReferences" BeforeTargets="CoreCompile" Inputs="$(MSBuildProjectFile);@(DafnyRuntimeJavaInputFile)" Outputs="$(DafnyRuntimeJar)">
--
-- <Message Text="Compiling DafnyRuntimeJava to $(DafnyRuntimeJar)..." Importance="high" />
-- <!-- For some reason the DafnyRuntime.jar was often not (yet?) created after this Target was run, leading to build failures.
-- We've removed the 'clean' step that was before 'build', so the DafnyRuntime.jar from a previous run can be used. -->
-- <ItemGroup>
-- <!-- Register the generated file to be deleted when cleaning -->
-- <FileWrites Include="$(DafnyRuntimeJar)" />
-- </ItemGroup>
-- </Target>
-
- </Project>
^ permalink raw reply related [flat|nested] 4+ messages in thread* [gentoo-commits] repo/gentoo:master commit in: dev-lang/dafny/, dev-lang/dafny/files/
@ 2024-02-10 16:24 Maciej Barć
0 siblings, 0 replies; 4+ messages in thread
From: Maciej Barć @ 2024-02-10 16:24 UTC (permalink / raw
To: gentoo-commits
commit: ddfc17b77a56706feee2307d495746aa05c3ea59
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Feb 10 13:39:45 2024 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Feb 10 16:24:49 2024 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ddfc17b7
dev-lang/dafny: drop old 4.3.0-r1
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
dev-lang/dafny/Manifest | 13 -
dev-lang/dafny/dafny-4.3.0-r1.ebuild | 609 ---------------------
dev-lang/dafny/files/dafny-4.1.0-lit.patch | 14 -
.../files/dafny-4.2.0-lit-use-system-boogie.patch | 11 -
.../dafny/files/dafny-4.3.0-net6.0-upgrade.patch | 22 -
5 files changed, 669 deletions(-)
diff --git a/dev-lang/dafny/Manifest b/dev-lang/dafny/Manifest
index 563bf2845273..b1836de83ec8 100644
--- a/dev-lang/dafny/Manifest
+++ b/dev-lang/dafny/Manifest
@@ -1,33 +1,20 @@
DIST bignumber.js-9.1.2.tgz 79226 BLAKE2B 3d2ff19d73a6fcfbcc0d03d1e9808796baae639e19973cbe0c26af4b514abc299129b8a7bc3e4e803c61af44b76f4381b1965d8fa331ea43e8a4c8fc7f98d8e7 SHA512 dbf98ac991fd2bce5bcce11f8570c11594c6775093b3ee481e9785428f65ba2046ee1821742f39d4f8f658085be84dd1e9bf6d663fd72a16e0e1fba6f8a7a9ba
-DIST boogie.abstractinterpretation.2.16.8.nupkg 29244 BLAKE2B 0e8deed122c8109b145bd2fe8f4134dbb9dfac1b934081b45e5ce89ce9147d47e6b26f6408fe47a9fb3228f8eaf783e289062991d07580d21b4092b36e6571e7 SHA512 04dcf0db58ced0f65ded090a7429bb213c9f45c7387ea0cf20f4c37ecd7630d03ead35e8029cd416296df6c5e9d2ca0cbd1c329b90fe96c19669cbf0be8828e6
DIST boogie.abstractinterpretation.3.0.9.nupkg 29646 BLAKE2B 20b0e150d3a9a6ed11a24cd9920a97971d515207d86864a9b1cd4d554b2b3c34e27778051a9bf6d8b3178352a6cfbb33c363b2d69958f6503e17e366ca3e1147 SHA512 26b75a409b4bfe5dd4ac982ca2c1b03df2118254a9becaab74f4d44b652746faa0448ab943ee9177f6a0fd105f8ce015a4403b6ff58df12201b542c50618b222
-DIST boogie.basetypes.2.16.8.nupkg 25567 BLAKE2B d4bbadd546e856f7eb308555f9cf14e5e60e97a442ba38b4f7cc563f41f2f8c33c441b34df65a05823c91201056f391dfeb89f268697475ec8cb0666a4a1a68f SHA512 34854b8ddaf94fc88ce459b8eb7164e1aa0b8fc1274b5772f44bbafd70996f1b68fc06d1c0575492ec6cb7d9878574dc0ceb27b6345b66b224cca1da5de7fa3d
DIST boogie.basetypes.3.0.9.nupkg 25717 BLAKE2B c1e549c6d7c675fd3b1acbe1a39fb5854d182b70ebab734350439dfd0cfd2be879b1d2b9c91ad832dae8e6f695fbc41510285bc7573b11fd51a170d4bbc50780 SHA512 d561f66a89af09cc07596bd1079993010a325ab2f22f2cc85408d12fd1286b15b0d7774b2e4037465a3b78aa829205f77b8b0b2efae9b9f3145eca6e82ced4d0
-DIST boogie.codecontractsextender.2.16.8.nupkg 17326 BLAKE2B 8b530bcc0d090f79d0dc24ddc89079468e7718c90f198dbe014b80a34a112253d35fcb7cd77495059bba71a1b30c8c86d27ae4902a76f20a57c53bd8edaa4dc5 SHA512 da0a8ed7bff2aff245a5c9fd1e2600cc4813e7f87ba9d135df57ee2ace433611f4a2007c860662f330b785add73939302d27623482feaf400eb0aa40fae6b1ef
DIST boogie.codecontractsextender.3.0.9.nupkg 17455 BLAKE2B 6a6f060e16942750e52bb72630b306cb591212ddd9960ac9778efe44239300f19b5793bb0cb94cb66e01a16f0337bf77bc6f39d2ce680f5ae94c566e2420331b SHA512 b15d7b0d24d5464189daf797e02b7e6342841de5c7cc3a15c954ee270d805afe0dfc3e5268dba5abbb636e2de2c859bf7a3f442180fd3a7cd2f70ec227fdfc24
-DIST boogie.concurrency.2.16.8.nupkg 93380 BLAKE2B 5c156974dd56e4cdb1162f99fd7af6d2440877139be008ebf812cd394b52396eb0dad2afd02718248246b6adbb8a497e31faf96aa5239c99eac37d31acbd550d SHA512 fe2f4890f462508d71d440ebc07ac00b7717ceb16ebf6689f5f684f6bfa7e589a36a73fefb751aa129092dbf81dd7052a1c74c1186d5b7e28325e93a7f38fefe
DIST boogie.concurrency.3.0.9.nupkg 93215 BLAKE2B aa8e969eea49750503249b1f196ed3c4f388fae2a39c46c61c4dcc343feb15b3d98d0b87065afe1f82fa0d8bbeea895b3362bc2ecca26daba0b0316ab8fad648 SHA512 618e4e3c06354b8ff8e6c23341915f1bd92366aa99dd8f9ef217110191f653be2a4d30cb83d004d4a34dcd7244e9f0603179859d1371109f1ae7706046643cbf
-DIST boogie.core.2.16.8.nupkg 201194 BLAKE2B 05e543b5dd70bdf78eab971a8648d5873a386c9b50574d011a7e815f45c95d506c8a1d1416f571a6dd418a9c4165d4e55f17c89ea55e6eb10cc83da1f2c29d74 SHA512 7a2969b3be2cee011f2683b190a4d1e7db254ba9078963d3f77e8d6de091c8e3f67be25b89d123f33266818834072ebfc853f9d384c626400215e8353fab324c
DIST boogie.core.3.0.9.nupkg 208520 BLAKE2B 180b099ac167eb4cdc2b96ebfecc0e70789d0bcb01fe2842b69520b1757efbc8cf0ca56846dee6ab17d5a88c38920273368803d646a143f4010926de81c420c1 SHA512 eaa0289840caed37aee889a66b60e0389729f2233b568c58de22790fd3eb3e93478b17d58d290c1622ccb7bf788f8a98cb942ed6124c8aa3efe5beb44889fbe0
-DIST boogie.executionengine.2.16.8.nupkg 83164 BLAKE2B 90af3c4ef8da9ad0bb38ffe82257b7615ed11d6f42c8c77534f91b4cf137819640b686898170725f7efbfa1277e8f8a2d7138a6980f09498af17f02b7ce50101 SHA512 c58be956eed537d8f1455ec70b4845982201595cf4c75f60437cf2edc1ab31e67fb9cd718c86c5bd311049a4f5c4305ba32f66595992e2e24c45c808a1fde709
DIST boogie.executionengine.3.0.9.nupkg 83903 BLAKE2B c3b8caf6097ab8f2b81b72593d7802674a8f6069f5601431a709095e0c785dea07c8b7b4033954ee7786e518973c9fe275d59be698918bcb5177bd90e3583525 SHA512 d80374d6df8f663ddef0a2bf004e9f414ca9d79e02861344f5878a1033db17a7d5102f92c4299e16ad5d1cf421a7cec4702dc320a5969a7699bcd2c31e933a1e
-DIST boogie.graph.2.16.8.nupkg 27805 BLAKE2B c76003c7d961103766957f46f0730cec6a888b942840c0f8e4b2a8b5d2e49e13c734849671c150e80027179b5c0bf132b8af3f5f88e8975e656c13b92dbea461 SHA512 89c80a4a9f3810a3d42578c4576a63fc3d735710f7da62776ba6272c8ae2dbb44fd92dadc152a718af6200a1b7bcdb32b4fe0c2ebdb6f2eccad565ae36de5a78
DIST boogie.graph.3.0.9.nupkg 27933 BLAKE2B 5ba929366367792f0288655c5f304ac6ad88d3a89c84df5082d78939306bd6e3441a1c517a060fd1c32eaa7d25e14a3eccf7c40873d413b68a5c36a109353ba8 SHA512 1b65fbf349c9516a18e2cdb876a343ee037096ee528933edc2565e43c5e79bcb2dcc56b7e095b150f6c70aa55b217789d04e6c4109e369cd2e9d96c465fd76f8
-DIST boogie.houdini.2.16.8.nupkg 52498 BLAKE2B aa93321fd931d5bcaa37f1a71dd07da904fe0a508a1455a049873b6b79bc8c34429e828260f4a15939c915c73cc2e811cc4a46e06f7e569d9fe6001247e45dfe SHA512 c32a7763f398499282115dfe83e9424c453a4f54dd43d4aab6bfdc082f2011e588d850ab6de95b59ceb069f12bd3a24c6ac67a96d510b7c21dee0b18d0b08fc5
DIST boogie.houdini.3.0.9.nupkg 52700 BLAKE2B 686c532de540e11d70be62bf95f6398c21e12ff9386a295b21d58882d105933068524d865b93eba8996bc29f80b05285196a2253493ddcaee13217797b0506ba SHA512 6ea2874623a582529e2e6921ca4c05e76602e6bf11f53323dbb5269e6201b1e1d2ec9bba7641a4918a95fb64f5a488841fab92da8ecc7c3fb033d0e286a4d0a9
-DIST boogie.model.2.16.8.nupkg 26750 BLAKE2B 2ea73b107c2261de30bd9f97985af96fad15506d3694f4eca83ae6a0e634a77c6aeea56f6587fe7e8ed6f2edf8f7ad487ec189deed86f9f553ec517fd734b73f SHA512 a4b780baddb8760843cdb55816ad8328e427cd6e6af3fb314e634291217a0fb30a1083b8a66e6e21cea5cd655cbabec68230fd2af919c7e1c03fab9e828d789e
DIST boogie.model.3.0.9.nupkg 26904 BLAKE2B ebc9e26fe815a7133e87febf8e4bf7af5af4b565e099dc2dfc45515e4e1a4559643d189c1ba5d0d21d230be958e3751306735c533fc99ed95acca740b22887ca SHA512 54a13e45ff1d53eed7cd372997525008c49075783df30a6159958c319c0ae661599bf08ec6bf9ebcdc45c85c97e2ca1d4cb33139db78a5abc50bd018a55c125b
-DIST boogie.provers.smtlib.2.16.8.nupkg 70449 BLAKE2B 18dfb53301792e6f1c300251c2dbb0e97305302e6a37b8d265c46089e9454cc27836542a1a1e4cb53663973c8a5052cfc01500ffa6bb33f27c855d31fe05e4f4 SHA512 c02db395a05d85595e8ce03a4cb114cc67722c2083f7a9f4c9c794edc8f664db1c5d9094ab1a831f7da723fdc953bff9e39e756b320f46853698c165f6ac3d33
DIST boogie.provers.smtlib.3.0.9.nupkg 70598 BLAKE2B 49195c7478a7c82fef6e15fb57bea2ddc891f5145fb7e655fc5b84fa4989d209aa0eff6bca8d57da9d08f6df026ee8cfb14d37953267048f5e191ad0520dcd74 SHA512 1c290058568cb170c0774779c8264f5e05700784bf21369852c0b0dd581665e64f9d23f98cd2ee22124b5a2866af56ad59fa56925212eae5b7ba26833d7034f1
-DIST boogie.vcexpr.2.16.8.nupkg 73410 BLAKE2B a47f0badc0881fe6e200992e04ec1b8e153ae20fe9f10c5967ef8c2437c322e942b396c2d10c1ae867d9259739eec4070b9235008666c39ec4f1bf3aeee5d530 SHA512 826fdb450d0e362edf79b9149eb2d9c999eab3c8236f2fb566b0af0f8cedf4b30ed24a4e181a409af004edf5bac23e2ffa7b218c55ca95f89b90eafb92fd6bb3
DIST boogie.vcexpr.3.0.9.nupkg 74092 BLAKE2B 978887817f7d48d26d999b2f0a37adee927506aa6eb2e7a93b78567b8fc67411e1cd56e0ee0876d95473edc0dc5068f69524093f8ffd7b4f109490c815a28b80 SHA512 024e898e35c933e4b1c55547624d5a3c531245ac1a8b9c03a2d5955d702bc1d51cbfcac0aaf214e9f0f3decfafaab02761490b02bc6ec5c385c2a20778c33de2
-DIST boogie.vcgeneration.2.16.8.nupkg 89218 BLAKE2B fdd76f0946962ac7d4c71498592f7309d706f932301ba5d2dd19a609426691c3ca8294845dadf47d6f33fb8ca54b915793174a3fbcf58cb2c2eb6f2b32460e49 SHA512 8cc9b1d373dd1e52141c32170de058474037eac398e2b3a3bc3de1cb4ae71776ad4a6cf6d486ece9a64ce48850295210b1d244081bf1f70c2f9eff83e7c811b7
DIST boogie.vcgeneration.3.0.9.nupkg 90650 BLAKE2B 435902e5892351f6aba902d3e3cf89c719c68ccff2075500fab607b6af64dda7837864284a3c44fc3a3ac17201355c1249c5ac2ed4ed61a2f1c3867b1338f18d SHA512 a9bb6155275f6f86ef5be7d26be560c8fd1f6f976da552cb038dd7eb41331ebcfb694f0b6367f73a778550e0545dd695c8a35d568cd0c9bd78fcf30c894cc490
DIST castle.core.4.4.0.nupkg 916004 BLAKE2B 7404f946c140bc4c22132282a4a12694328bac2f37f3cae06c595076068dbedc808465e352f083450cea3e3869698f91b7a5b2b55c08f29f4a9feba7f15abf74 SHA512 7626c347f82038bc29b0b2ae399937047aead260ed85ff8c107d36adbe901d729be59cd89a5f98ef45da2d1883c8374b6f286c81c044a5a2b69ab4b5dde9ce98
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.3.0.tar.gz 5922075 BLAKE2B ba5888f64c194fefaabe4e817422d87093de373920fa66ed6ef9bce5471fa2b32681aaf16bcd7b6a1933fd822747843da9f3208c8a9ea9e8e5b9463e3abb12d9 SHA512 2989c7c7030ca6dd3df0a43e2c099e3d0b383ac23058a1f6a6a7579e764c2842f241f17594f3b385945b4f59aa17039b5c34a9165be86a15d8441dc3ea09ca58
DIST dafny-4.4.0.tar.gz 6241907 BLAKE2B 43f5b6bed5ea0bc6f8de04650b2f97c0092df1df47aba9bf0c6b9210677077427c67cc80364f659305b7d851c178439a1536864dfb7c6396b4ac6517789fc83d SHA512 33789f10b75a1946aab552f11f40296682156bab7cb08cae431f00f6fdb6b12d3211ec2f423a42adb78a3245b19ab8f772dafca4d1448cb30077268680f73534
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.3.0-r1.ebuild b/dev-lang/dafny/dafny-4.3.0-r1.ebuild
deleted file mode 100644
index 77736aeb8863..000000000000
--- a/dev-lang/dafny/dafny-4.3.0-r1.ebuild
+++ /dev/null
@@ -1,609 +0,0 @@
-# Copyright 1999-2023 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@2.16.8
-boogie.basetypes@2.16.8
-boogie.codecontractsextender@2.16.8
-boogie.concurrency@2.16.8
-boogie.core@2.16.8
-boogie.executionengine@2.16.8
-boogie.graph@2.16.8
-boogie.houdini@2.16.8
-boogie.model@2.16.8
-boogie.provers.smtlib@2.16.8
-boogie.vcexpr@2.16.8
-boogie.vcgeneration@2.16.8
-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.testplatform.extensions.trxlogger@17.0.0
-microsoft.testplatform.objectmodel@16.11.0
-microsoft.testplatform.objectmodel@16.9.4
-microsoft.testplatform.objectmodel@17.0.0
-microsoft.testplatform.objectmodel@17.1.0
-microsoft.testplatform.testhost@16.11.0
-microsoft.testplatform.testhost@16.9.4
-microsoft.testplatform.testhost@17.1.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.10.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.0.1
-system.collections.nongeneric@4.3.0
-system.collections.specialized@4.0.1
-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.0.1
-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
-
-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
- dev-lang/go
- dev-python/OutputCheck
- dev-python/lit
- net-libs/nodejs[npm]
- )
-"
-
-CHECKREQS_DISK_BUILD="2G"
-DOTNET_PKG_PROJECTS=(
- "${S}/Source/Dafny/Dafny.csproj"
- "${S}/Source/TestDafny/TestDafny.csproj"
-)
-PATCHES=(
- "${FILESDIR}/${PN}-3.12.0-DafnyCore-csproj.patch"
- "${FILESDIR}/${PN}-3.12.0-DafnyRuntime-csproj.patch"
- "${FILESDIR}/${PN}-4.1.0-lit.patch"
- "${FILESDIR}/${PN}-4.2.0-lit-use-system-boogie.patch"
- "${FILESDIR}/${PN}-4.3.0-net6.0-upgrade.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() {
- dotnet-pkg_src_unpack
-
- if [[ -n ${EGIT_REPO_URI} ]] ; then
- git-r3_src_unpack
- fi
-}
-
-src_prepare() {
- # Remove bad tests (recursive).
- local -a bad_tests
- bad_tests=(
- # Following tests fail:
- DafnyTestGeneration/TestGeneration.dfy
- DafnyTests/TestAttribute.dfy
- auditor/TestAuditor.dfy
- benchmarks/sequence-race/SequenceRace.dfy
- dafny0/Fuel.dfy
- dafny0/JavaUseRuntimeLib.dfy
- dafny0/Stdin.dfy
- examples/Simple_compiler/Compiler.dfy
- separate-verification/assumptions.dfy
- server/counterexample_none.transcript
- unicodechars/comp/Arrays.dfy
- unicodechars/comp/Collections.dfy
- unicodechars/comp/Comprehensions.dfy
- unicodechars/expectations/Expect.dfy
-
- # Following tests are very slow:
- comp/Arrays.dfy
- comp/BranchCoverage.dfy
- comp/Collections.dfy
- comp/CompileWithArguments.dfy
- comp/Comprehensions.dfy
- comp/Extern.dfy
- comp/MainMethod.dfy
- comp/Print.dfy
- comp/TailRecursion.dfy
- comp/UnicodeStrings.dfy
- comp/Uninitialized.dfy
- comp/compile1quiet/CompileRunQuietly.dfy
- comp/compile3/JustRun.dfy
- comp/manualcompile/ManualCompile.dfy
- concurrency/06-ThreadOwnership.dfy
- concurrency/07-CounterThreadOwnership.dfy
- concurrency/09-CounterNoStateMachine.dfy
- concurrency/10-SequenceInvariant.dfy
- concurrency/11-MutexGuard2.dfy
- concurrency/12-MutexLifetime-short.dfy
- dafny0/RlimitMultiplier.dfy
- dafny0/Strings.dfy
- dafny1/SchorrWaite.dfy
- dafny2/MinWindowMax.dfy
- dafny2/SmallestMissingNumber-functional.dfy
- dafny2/SnapshotableTrees.dfy
- dafny4/UnionFind.dfy
- dafny4/git-issue250.dfy
- expectations/Expect.dfy
- git-issues/git-issue-356.dfy
- git-issues/git-issue-Main0.dfy
- git-issues/git-issue-Main4.dfy
- git-issues/git-issue-MainE.dfy
- hofs/VectorUpdate.dfy
- metatests/ConsistentWhenSupported.dfy
- separate-verification/app.dfy
- traits/TraitCompile.dfy
- unicodechars/comp/CompileWithArguments.dfy
- )
- local bad_test
- for bad_test in "${bad_tests[@]}" ; do
- rm -r "${S}/Test/${bad_test}" \
- || die "failed to remove test ${bad_test}"
- done
-
- # Update lit's "lit.site.cfg" file.
- local dotnet_exec="${DOTNET_PKG_EXECUTABLE} exec ${DOTNET_PKG_OUTPUT}"
- local lit_config="${S}/Test/lit.site.cfg"
- sed "/^defaultDafnyExecutable/s|=.*|= '${dotnet_exec}/Dafny.dll '|" \
- -i "${lit_config}" || die "failed to update ${lit_config}"
- sed "/^dafnyExecutable/s|=.*|= '${dotnet_exec}/Dafny.dll '|" \
- -i "${lit_config}" || die "failed to update ${lit_config}"
- sed "/^testDafnyExecutableCompiler/s|=.*|= '${dotnet_exec}/TestDafny.dll for-each-compiler '|" \
- -i "${lit_config}" || die "failed to update ${lit_config}"
- sed "/^testDafnyExecutableResolver/s|=.*|= '${dotnet_exec}/TestDafny.dll for-each-resolver '|" \
- -i "${lit_config}" || die "failed to update ${lit_config}"
- sed "/^defaultServerExecutable/s|=.*|= '${dotnet_exec}/DafnyServer.dll'|" \
- -i "${lit_config}" || die "failed to update ${lit_config}"
- sed "/^serverExecutable/s|=.*|= '${dotnet_exec}/DafnyServer.dll'|" \
- -i "${lit_config}" || die "failed to update ${lit_config}"
-
- dotnet-pkg_src_prepare
- java-pkg-2_src_prepare
-}
-
-src_compile () {
- # In 4.3.0 the DafnyRuntime JAR has mismatched version, by mistake?
-
- einfo "Building dependency-less DafnyRuntime 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 ./ "${dafny_runtime_java}/src/main/java/dafny"/*.java
- edo jar cvf "DafnyRuntime-4.2.0.jar" dafny/*
- cp "DafnyRuntime-4.2.0.jar" "${dafny_runtime_java}/build/libs/" || die
- popd || die
-
- # Build main dotnet package.
- dotnet-pkg_src_compile
-}
-
-src_test() {
- # The test "dafny0/DafnyLibClient.dfy" expects to use "DafnyRuntime.dll"
- # from the "Binaries" directory.
- ln -s "${DOTNET_PKG_OUTPUT}/DafnyRuntime.dll" "${S}/Binaries/" || die
-
- einfo "Installing bignumber.js package required for tests using NodeJS."
- local -a npm_opts
- 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
- lit_opts=(
- --order=lexical
- --time-tests
- --verbose
- --workers="$(makeopts_jobs)"
- )
- edob lit "${lit_opts[@]}" "${S}/Test"
-}
-
-src_install() {
- dotnet-pkg-base_install
-
- local -a dafny_exes
- 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
-}
diff --git a/dev-lang/dafny/files/dafny-4.1.0-lit.patch b/dev-lang/dafny/files/dafny-4.1.0-lit.patch
deleted file mode 100644
index c64dab367664..000000000000
--- a/dev-lang/dafny/files/dafny-4.1.0-lit.patch
+++ /dev/null
@@ -1,14 +0,0 @@
---- a/Test/lit.site.cfg
-+++ b/Test/lit.site.cfg
-@@ -215,9 +215,9 @@ def find(name, rooot):
- return name
- return ""
-
-+import shutil
- solverPath = \
-- find("z3-4.12.1", binaryDir) or \
-- find("cvc4", binaryDir)
-+ shutil.which("z3")
-
- if not solverPath:
- lit_config.fatal('Could not find solver')
diff --git a/dev-lang/dafny/files/dafny-4.2.0-lit-use-system-boogie.patch b/dev-lang/dafny/files/dafny-4.2.0-lit-use-system-boogie.patch
deleted file mode 100644
index 68c3157f6809..000000000000
--- a/dev-lang/dafny/files/dafny-4.2.0-lit-use-system-boogie.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- a/Test/lit.site.cfg
-+++ b/Test/lit.site.cfg
-@@ -107,7 +107,7 @@ testDafnyExecutable = 'dotnet-bin-6.0 exec /var/tmp/portage/dev-lang/dafny-4.2.0
- defaultServerExecutable = 'dotnet-bin-6.0 exec /var/tmp/portage/dev-lang/dafny-4.2.0/work/dafny-4.2.0_net6.0_Release/DafnyServer.dll'
- serverExecutable = 'dotnet-bin-6.0 exec /var/tmp/portage/dev-lang/dafny-4.2.0/work/dafny-4.2.0_net6.0_Release/DafnyServer.dll'
-
--boogieExecutable = 'dotnet tool run boogie'
-+boogieExecutable = 'boogie'
-
- config.suffixes.append('.transcript')
-
diff --git a/dev-lang/dafny/files/dafny-4.3.0-net6.0-upgrade.patch b/dev-lang/dafny/files/dafny-4.3.0-net6.0-upgrade.patch
deleted file mode 100644
index 5c43ca90ae0e..000000000000
--- a/dev-lang/dafny/files/dafny-4.3.0-net6.0-upgrade.patch
+++ /dev/null
@@ -1,22 +0,0 @@
---- a/Source/DafnyRuntime/DafnyRuntime.csproj.orig
-+++ b/Source/DafnyRuntime/DafnyRuntime.csproj
-@@ -6,7 +6,7 @@
- <GeneratePackageOnBuild>true</GeneratePackageOnBuild>
- <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
- <DefineConstants>TRACE;ISDAFNYRUNTIMELIB</DefineConstants>
-- <TargetFrameworks>netstandard2.0;net452</TargetFrameworks>
-+ <TargetFrameworks>net6.0</TargetFrameworks>
- <OutputPath>..\..\Binaries\</OutputPath>
- <LangVersion>7.3</LangVersion>
- <PackageLicenseExpression>MIT</PackageLicenseExpression>
---- a/Test/comp/separate-compilation/Inputs/producer/TimesTwo.csproj.orig
-+++ b/Test/comp/separate-compilation/Inputs/producer/TimesTwo.csproj
-@@ -2,7 +2,7 @@
- <Project Sdk="Microsoft.NET.Sdk">
-
- <PropertyGroup>
-- <TargetFramework>netstandard2.0</TargetFramework>
-+ <TargetFramework>net6.0</TargetFramework>
- </PropertyGroup>
-
- <ItemGroup>
^ permalink raw reply related [flat|nested] 4+ messages in thread* [gentoo-commits] repo/gentoo:master commit in: dev-lang/dafny/, dev-lang/dafny/files/
@ 2023-12-13 2:27 Maciej Barć
0 siblings, 0 replies; 4+ messages in thread
From: Maciej Barć @ 2023-12-13 2:27 UTC (permalink / raw
To: gentoo-commits
commit: 394afbb93c7086cdb0e39ef9e12964ca78fdf6e8
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Wed Dec 13 01:55:44 2023 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Wed Dec 13 02:27:13 2023 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=394afbb9
dev-lang/dafny: bump to 4.4.0
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
dev-lang/dafny/Manifest | 15 +
dev-lang/dafny/dafny-4.4.0.ebuild | 558 +++++++++++++++++++++
dev-lang/dafny/files/dafny-4.4.0-lit-config.patch | 14 +
.../files/dafny-4.4.0-lit-system-boogie.patch | 11 +
dev-lang/dafny/files/dafny-4.4.0-no-copy-jar.patch | 21 +
.../dafny/files/dafny-4.4.0-no-output-jar.patch | 18 +
6 files changed, 637 insertions(+)
diff --git a/dev-lang/dafny/Manifest b/dev-lang/dafny/Manifest
index f3a77f80609e..563bf2845273 100644
--- a/dev-lang/dafny/Manifest
+++ b/dev-lang/dafny/Manifest
@@ -1,21 +1,34 @@
DIST bignumber.js-9.1.2.tgz 79226 BLAKE2B 3d2ff19d73a6fcfbcc0d03d1e9808796baae639e19973cbe0c26af4b514abc299129b8a7bc3e4e803c61af44b76f4381b1965d8fa331ea43e8a4c8fc7f98d8e7 SHA512 dbf98ac991fd2bce5bcce11f8570c11594c6775093b3ee481e9785428f65ba2046ee1821742f39d4f8f658085be84dd1e9bf6d663fd72a16e0e1fba6f8a7a9ba
DIST boogie.abstractinterpretation.2.16.8.nupkg 29244 BLAKE2B 0e8deed122c8109b145bd2fe8f4134dbb9dfac1b934081b45e5ce89ce9147d47e6b26f6408fe47a9fb3228f8eaf783e289062991d07580d21b4092b36e6571e7 SHA512 04dcf0db58ced0f65ded090a7429bb213c9f45c7387ea0cf20f4c37ecd7630d03ead35e8029cd416296df6c5e9d2ca0cbd1c329b90fe96c19669cbf0be8828e6
+DIST boogie.abstractinterpretation.3.0.9.nupkg 29646 BLAKE2B 20b0e150d3a9a6ed11a24cd9920a97971d515207d86864a9b1cd4d554b2b3c34e27778051a9bf6d8b3178352a6cfbb33c363b2d69958f6503e17e366ca3e1147 SHA512 26b75a409b4bfe5dd4ac982ca2c1b03df2118254a9becaab74f4d44b652746faa0448ab943ee9177f6a0fd105f8ce015a4403b6ff58df12201b542c50618b222
DIST boogie.basetypes.2.16.8.nupkg 25567 BLAKE2B d4bbadd546e856f7eb308555f9cf14e5e60e97a442ba38b4f7cc563f41f2f8c33c441b34df65a05823c91201056f391dfeb89f268697475ec8cb0666a4a1a68f SHA512 34854b8ddaf94fc88ce459b8eb7164e1aa0b8fc1274b5772f44bbafd70996f1b68fc06d1c0575492ec6cb7d9878574dc0ceb27b6345b66b224cca1da5de7fa3d
+DIST boogie.basetypes.3.0.9.nupkg 25717 BLAKE2B c1e549c6d7c675fd3b1acbe1a39fb5854d182b70ebab734350439dfd0cfd2be879b1d2b9c91ad832dae8e6f695fbc41510285bc7573b11fd51a170d4bbc50780 SHA512 d561f66a89af09cc07596bd1079993010a325ab2f22f2cc85408d12fd1286b15b0d7774b2e4037465a3b78aa829205f77b8b0b2efae9b9f3145eca6e82ced4d0
DIST boogie.codecontractsextender.2.16.8.nupkg 17326 BLAKE2B 8b530bcc0d090f79d0dc24ddc89079468e7718c90f198dbe014b80a34a112253d35fcb7cd77495059bba71a1b30c8c86d27ae4902a76f20a57c53bd8edaa4dc5 SHA512 da0a8ed7bff2aff245a5c9fd1e2600cc4813e7f87ba9d135df57ee2ace433611f4a2007c860662f330b785add73939302d27623482feaf400eb0aa40fae6b1ef
+DIST boogie.codecontractsextender.3.0.9.nupkg 17455 BLAKE2B 6a6f060e16942750e52bb72630b306cb591212ddd9960ac9778efe44239300f19b5793bb0cb94cb66e01a16f0337bf77bc6f39d2ce680f5ae94c566e2420331b SHA512 b15d7b0d24d5464189daf797e02b7e6342841de5c7cc3a15c954ee270d805afe0dfc3e5268dba5abbb636e2de2c859bf7a3f442180fd3a7cd2f70ec227fdfc24
DIST boogie.concurrency.2.16.8.nupkg 93380 BLAKE2B 5c156974dd56e4cdb1162f99fd7af6d2440877139be008ebf812cd394b52396eb0dad2afd02718248246b6adbb8a497e31faf96aa5239c99eac37d31acbd550d SHA512 fe2f4890f462508d71d440ebc07ac00b7717ceb16ebf6689f5f684f6bfa7e589a36a73fefb751aa129092dbf81dd7052a1c74c1186d5b7e28325e93a7f38fefe
+DIST boogie.concurrency.3.0.9.nupkg 93215 BLAKE2B aa8e969eea49750503249b1f196ed3c4f388fae2a39c46c61c4dcc343feb15b3d98d0b87065afe1f82fa0d8bbeea895b3362bc2ecca26daba0b0316ab8fad648 SHA512 618e4e3c06354b8ff8e6c23341915f1bd92366aa99dd8f9ef217110191f653be2a4d30cb83d004d4a34dcd7244e9f0603179859d1371109f1ae7706046643cbf
DIST boogie.core.2.16.8.nupkg 201194 BLAKE2B 05e543b5dd70bdf78eab971a8648d5873a386c9b50574d011a7e815f45c95d506c8a1d1416f571a6dd418a9c4165d4e55f17c89ea55e6eb10cc83da1f2c29d74 SHA512 7a2969b3be2cee011f2683b190a4d1e7db254ba9078963d3f77e8d6de091c8e3f67be25b89d123f33266818834072ebfc853f9d384c626400215e8353fab324c
+DIST boogie.core.3.0.9.nupkg 208520 BLAKE2B 180b099ac167eb4cdc2b96ebfecc0e70789d0bcb01fe2842b69520b1757efbc8cf0ca56846dee6ab17d5a88c38920273368803d646a143f4010926de81c420c1 SHA512 eaa0289840caed37aee889a66b60e0389729f2233b568c58de22790fd3eb3e93478b17d58d290c1622ccb7bf788f8a98cb942ed6124c8aa3efe5beb44889fbe0
DIST boogie.executionengine.2.16.8.nupkg 83164 BLAKE2B 90af3c4ef8da9ad0bb38ffe82257b7615ed11d6f42c8c77534f91b4cf137819640b686898170725f7efbfa1277e8f8a2d7138a6980f09498af17f02b7ce50101 SHA512 c58be956eed537d8f1455ec70b4845982201595cf4c75f60437cf2edc1ab31e67fb9cd718c86c5bd311049a4f5c4305ba32f66595992e2e24c45c808a1fde709
+DIST boogie.executionengine.3.0.9.nupkg 83903 BLAKE2B c3b8caf6097ab8f2b81b72593d7802674a8f6069f5601431a709095e0c785dea07c8b7b4033954ee7786e518973c9fe275d59be698918bcb5177bd90e3583525 SHA512 d80374d6df8f663ddef0a2bf004e9f414ca9d79e02861344f5878a1033db17a7d5102f92c4299e16ad5d1cf421a7cec4702dc320a5969a7699bcd2c31e933a1e
DIST boogie.graph.2.16.8.nupkg 27805 BLAKE2B c76003c7d961103766957f46f0730cec6a888b942840c0f8e4b2a8b5d2e49e13c734849671c150e80027179b5c0bf132b8af3f5f88e8975e656c13b92dbea461 SHA512 89c80a4a9f3810a3d42578c4576a63fc3d735710f7da62776ba6272c8ae2dbb44fd92dadc152a718af6200a1b7bcdb32b4fe0c2ebdb6f2eccad565ae36de5a78
+DIST boogie.graph.3.0.9.nupkg 27933 BLAKE2B 5ba929366367792f0288655c5f304ac6ad88d3a89c84df5082d78939306bd6e3441a1c517a060fd1c32eaa7d25e14a3eccf7c40873d413b68a5c36a109353ba8 SHA512 1b65fbf349c9516a18e2cdb876a343ee037096ee528933edc2565e43c5e79bcb2dcc56b7e095b150f6c70aa55b217789d04e6c4109e369cd2e9d96c465fd76f8
DIST boogie.houdini.2.16.8.nupkg 52498 BLAKE2B aa93321fd931d5bcaa37f1a71dd07da904fe0a508a1455a049873b6b79bc8c34429e828260f4a15939c915c73cc2e811cc4a46e06f7e569d9fe6001247e45dfe SHA512 c32a7763f398499282115dfe83e9424c453a4f54dd43d4aab6bfdc082f2011e588d850ab6de95b59ceb069f12bd3a24c6ac67a96d510b7c21dee0b18d0b08fc5
+DIST boogie.houdini.3.0.9.nupkg 52700 BLAKE2B 686c532de540e11d70be62bf95f6398c21e12ff9386a295b21d58882d105933068524d865b93eba8996bc29f80b05285196a2253493ddcaee13217797b0506ba SHA512 6ea2874623a582529e2e6921ca4c05e76602e6bf11f53323dbb5269e6201b1e1d2ec9bba7641a4918a95fb64f5a488841fab92da8ecc7c3fb033d0e286a4d0a9
DIST boogie.model.2.16.8.nupkg 26750 BLAKE2B 2ea73b107c2261de30bd9f97985af96fad15506d3694f4eca83ae6a0e634a77c6aeea56f6587fe7e8ed6f2edf8f7ad487ec189deed86f9f553ec517fd734b73f SHA512 a4b780baddb8760843cdb55816ad8328e427cd6e6af3fb314e634291217a0fb30a1083b8a66e6e21cea5cd655cbabec68230fd2af919c7e1c03fab9e828d789e
+DIST boogie.model.3.0.9.nupkg 26904 BLAKE2B ebc9e26fe815a7133e87febf8e4bf7af5af4b565e099dc2dfc45515e4e1a4559643d189c1ba5d0d21d230be958e3751306735c533fc99ed95acca740b22887ca SHA512 54a13e45ff1d53eed7cd372997525008c49075783df30a6159958c319c0ae661599bf08ec6bf9ebcdc45c85c97e2ca1d4cb33139db78a5abc50bd018a55c125b
DIST boogie.provers.smtlib.2.16.8.nupkg 70449 BLAKE2B 18dfb53301792e6f1c300251c2dbb0e97305302e6a37b8d265c46089e9454cc27836542a1a1e4cb53663973c8a5052cfc01500ffa6bb33f27c855d31fe05e4f4 SHA512 c02db395a05d85595e8ce03a4cb114cc67722c2083f7a9f4c9c794edc8f664db1c5d9094ab1a831f7da723fdc953bff9e39e756b320f46853698c165f6ac3d33
+DIST boogie.provers.smtlib.3.0.9.nupkg 70598 BLAKE2B 49195c7478a7c82fef6e15fb57bea2ddc891f5145fb7e655fc5b84fa4989d209aa0eff6bca8d57da9d08f6df026ee8cfb14d37953267048f5e191ad0520dcd74 SHA512 1c290058568cb170c0774779c8264f5e05700784bf21369852c0b0dd581665e64f9d23f98cd2ee22124b5a2866af56ad59fa56925212eae5b7ba26833d7034f1
DIST boogie.vcexpr.2.16.8.nupkg 73410 BLAKE2B a47f0badc0881fe6e200992e04ec1b8e153ae20fe9f10c5967ef8c2437c322e942b396c2d10c1ae867d9259739eec4070b9235008666c39ec4f1bf3aeee5d530 SHA512 826fdb450d0e362edf79b9149eb2d9c999eab3c8236f2fb566b0af0f8cedf4b30ed24a4e181a409af004edf5bac23e2ffa7b218c55ca95f89b90eafb92fd6bb3
+DIST boogie.vcexpr.3.0.9.nupkg 74092 BLAKE2B 978887817f7d48d26d999b2f0a37adee927506aa6eb2e7a93b78567b8fc67411e1cd56e0ee0876d95473edc0dc5068f69524093f8ffd7b4f109490c815a28b80 SHA512 024e898e35c933e4b1c55547624d5a3c531245ac1a8b9c03a2d5955d702bc1d51cbfcac0aaf214e9f0f3decfafaab02761490b02bc6ec5c385c2a20778c33de2
DIST boogie.vcgeneration.2.16.8.nupkg 89218 BLAKE2B fdd76f0946962ac7d4c71498592f7309d706f932301ba5d2dd19a609426691c3ca8294845dadf47d6f33fb8ca54b915793174a3fbcf58cb2c2eb6f2b32460e49 SHA512 8cc9b1d373dd1e52141c32170de058474037eac398e2b3a3bc3de1cb4ae71776ad4a6cf6d486ece9a64ce48850295210b1d244081bf1f70c2f9eff83e7c811b7
+DIST boogie.vcgeneration.3.0.9.nupkg 90650 BLAKE2B 435902e5892351f6aba902d3e3cf89c719c68ccff2075500fab607b6af64dda7837864284a3c44fc3a3ac17201355c1249c5ac2ed4ed61a2f1c3867b1338f18d SHA512 a9bb6155275f6f86ef5be7d26be560c8fd1f6f976da552cb038dd7eb41331ebcfb694f0b6367f73a778550e0545dd695c8a35d568cd0c9bd78fcf30c894cc490
DIST castle.core.4.4.0.nupkg 916004 BLAKE2B 7404f946c140bc4c22132282a4a12694328bac2f37f3cae06c595076068dbedc808465e352f083450cea3e3869698f91b7a5b2b55c08f29f4a9feba7f15abf74 SHA512 7626c347f82038bc29b0b2ae399937047aead260ed85ff8c107d36adbe901d729be59cd89a5f98ef45da2d1883c8374b6f286c81c044a5a2b69ab4b5dde9ce98
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.3.0.tar.gz 5922075 BLAKE2B ba5888f64c194fefaabe4e817422d87093de373920fa66ed6ef9bce5471fa2b32681aaf16bcd7b6a1933fd822747843da9f3208c8a9ea9e8e5b9463e3abb12d9 SHA512 2989c7c7030ca6dd3df0a43e2c099e3d0b383ac23058a1f6a6a7579e764c2842f241f17594f3b385945b4f59aa17039b5c34a9165be86a15d8441dc3ea09ca58
+DIST dafny-4.4.0.tar.gz 6241907 BLAKE2B 43f5b6bed5ea0bc6f8de04650b2f97c0092df1df47aba9bf0c6b9210677077427c67cc80364f659305b7d851c178439a1536864dfb7c6396b4ac6517789fc83d SHA512 33789f10b75a1946aab552f11f40296682156bab7cb08cae431f00f6fdb6b12d3211ec2f423a42adb78a3245b19ab8f772dafca4d1448cb30077268680f73534
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
@@ -85,6 +98,8 @@ DIST microsoft.netcore.platforms.3.0.0.nupkg 29497 BLAKE2B eb1e21bb3a3d3d3a65b13
DIST microsoft.netcore.platforms.3.1.0.nupkg 29544 BLAKE2B 2739d62e92e61677964f9ef380ef2f72ddb6879444d7e744c283a73fdf4ad69c07c36a0b3c4030312b0a4c622aa91dc09cfa828ab8dcd9cf0c5506aa2fac5c8c SHA512 636a1e3768f782ced193b18ec61616c122b5b756395bbec3ede805b172ce62db2d631407deebba73bf136234479be4824f0268a57f52ff4f8d7d37d4370cd966
DIST microsoft.netcore.targets.1.0.1.nupkg 18189 BLAKE2B d43a064d4c6f836be5164708ff0401913b32fc3340cad7c8fd08f421ea553805ac150a134a0d60a55d41eec124514a5e5197eebcc85aa6595cc6b91e33025d61 SHA512 6ed8e75f945a18651066fe9ee31cf6c8257a5974340fe4d262438903c4959a479f4a515a4d1389e6d3d3ab34f09a3c7bc2009aada2e8a7f697b6655a82d3bfc9
DIST microsoft.netcore.targets.1.1.0.nupkg 18162 BLAKE2B 419d19e0da934ab4b9db75dd66cc22b83a003f34e93cf7a92feccf4f32d3d695e18b826b1aba13073dd4ec53aa7905a67346921d1055516647ddcde0d79009f1 SHA512 1ef033a68688aab9997ec1c0378acb1638b4afb618e533fcaf749d93389737ba94f4a0a94481becdf701c7e988ae2fe390136a8eae225887ee60db45063490fe
+DIST microsoft.netframework.referenceassemblies.1.0.2.nupkg 20957 BLAKE2B e521646690b142a703d943cb0528552a669ceed16fa71e3a04300da1eb58d5428b168628c85b8e963e963cf0041b0a02d7442414248e6f506ff3d7ae452a85cb SHA512 8bf3922b695856059b8eec696a7ace03a7269d71d4c456cbdfb21bd3f6e69f2a9fa25e46acd5c29ad872829a07cc05ec083c3a6ee942bca21afd47ce3bc533e3
+DIST microsoft.netframework.referenceassemblies.net452.1.0.2.nupkg 19845441 BLAKE2B c2be1acfd4207984ba33a5ed468fea39299d61d6af99ef9cfc7df16096c0ecfb6133a3c970ffc150f79566710a589c5a387a5d2da8d5ce25f23173cfcfcc7661 SHA512 f4b099aa012c3d117c58dafcaa3edfc273ad7d5acf30c84d213eb15ae101559e7da3f1810285909153e85d73ac58dfedc34e6730c264cb0ae013e19a1213d691
DIST microsoft.testplatform.extensions.trxlogger.17.0.0.nupkg 361862 BLAKE2B 7315293c1ab965bbcc299a842a2e1f462e4821168f79f3036f7a14a4116f3d73c00f5b645bd1d16fc963f595e65ae11d7658544a6482c0e5926b36528644b259 SHA512 d72f41fbe9d4155b85d0e20e6a476d41ea55e355c61561270f241a1b2ef5b9d8dc9c81ca43d14c550a50bff0a301923e9e84a5035e5b31006a9639ba0221e907
DIST microsoft.testplatform.objectmodel.16.11.0.nupkg 2966263 BLAKE2B 5bf6464154b639b478c4000dd64e7570d124a446680583bceafee1cf3eafdc6a7bc10cacc665327a562a28fe0268c5d749dad0ef11376880f76310f1e3cb055c SHA512 105ec3c2d2d476abfa9fec73b25a701d815b743512b575e7ee2373ef7e459f767688be7ecdb555849a8342e07e922ab819dfae637e8b23b36ed918655d9a7471
DIST microsoft.testplatform.objectmodel.16.9.4.nupkg 2224614 BLAKE2B c8b0899000db731c0041f6209e4f85d2bbee5a7ebe3d3addd4405a33e1036bef52098c3fe8146123db262e71868d7bbe541149ef7443c7fc718ca78f916d384b SHA512 a1fc8192007d0d1a852393eadea26b8400df81a50d8a29549f79f726694696b2c361460561a3910f66dc195044b7773addc25642f9c7389b7152489e162f9ad9
diff --git a/dev-lang/dafny/dafny-4.4.0.ebuild b/dev-lang/dafny/dafny-4.4.0.ebuild
new file mode 100644
index 000000000000..50a6fd8da3c2
--- /dev/null
+++ b/dev-lang/dafny/dafny-4.4.0.ebuild
@@ -0,0 +1,558 @@
+# Copyright 1999-2023 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.0.9
+boogie.basetypes@3.0.9
+boogie.codecontractsextender@3.0.9
+boogie.concurrency@3.0.9
+boogie.core@3.0.9
+boogie.executionengine@3.0.9
+boogie.graph@3.0.9
+boogie.houdini@3.0.9
+boogie.model@3.0.9
+boogie.provers.smtlib@3.0.9
+boogie.vcexpr@3.0.9
+boogie.vcgeneration@3.0.9
+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.0.0
+microsoft.testplatform.objectmodel@16.11.0
+microsoft.testplatform.objectmodel@16.9.4
+microsoft.testplatform.objectmodel@17.0.0
+microsoft.testplatform.objectmodel@17.1.0
+microsoft.testplatform.testhost@16.11.0
+microsoft.testplatform.testhost@16.9.4
+microsoft.testplatform.testhost@17.1.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.10.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.0.1
+system.collections.nongeneric@4.3.0
+system.collections.specialized@4.0.1
+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.0.1
+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 multiprocessing python-any-r1
+
+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
+ sci-mathematics/z3
+"
+BDEPEND="
+ ${RDEPEND}
+ dev-dotnet/coco
+ test? (
+ ${PYTHON_DEPS}
+ dev-lang/boogie
+ dev-lang/go
+ dev-python/OutputCheck
+ dev-python/lit
+ net-libs/nodejs[npm]
+ )
+"
+
+CHECKREQS_DISK_BUILD="2G"
+DOTNET_PKG_PROJECTS=(
+ "${S}/Source/Dafny/Dafny.csproj"
+ "${S}/Source/TestDafny/TestDafny.csproj"
+)
+
+PATCHES=(
+ "${FILESDIR}/${PN}-3.12.0-DafnyCore-csproj.patch"
+ "${FILESDIR}/${PN}-3.12.0-DafnyRuntime-csproj.patch"
+ "${FILESDIR}/${PN}-4.4.0-lit-config.patch"
+ "${FILESDIR}/${PN}-4.4.0-lit-system-boogie.patch"
+ "${FILESDIR}/${PN}-4.4.0-no-copy-jar.patch"
+ "${FILESDIR}/${PN}-4.4.0-no-output-jar.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
+
+ check-reqs_pkg_setup
+ dotnet-pkg_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
+ fi
+ done < <(find "${TEST_S}" -type f -name "*.dfy")
+
+ # Remove bad tests (recursive).
+ local -a bad_tests=(
+ # Following tests fail:
+ DafnyTests/TestAttribute.dfy
+ VSComp2010/Problem2-Invert.dfy
+ auditor/TestAuditor.dfy
+ benchmarks/sequence-race/SequenceRace.dfy
+ comp/CoverageReport.dfy
+ dafny0/Fuel.legacy.dfy
+ dafny0/JavaUseRuntimeLib.dfy
+ dafny0/Stdin.dfy
+ dafny4/Lucas-up.legacy.dfy
+ examples/Simple_compiler/Compiler.dfy
+ git-issues/git-issue-2026.dfy
+ git-issues/git-issue-2299.dfy
+ git-issues/git-issue-2301.dfy
+ metatests/InconsistentCompilerBehavior.dfy
+ metatests/TestBeyondVerifierExpect.dfy
+ separate-verification/assumptions.dfy
+ server/counterexample_none.transcript
+ unicodechars/expectations/Expect.dfy
+ wishlist/exists-b-exists-not-b.dfy
+
+ # Following tests are very slow:
+ )
+ local bad_test
+ for bad_test in "${bad_tests[@]}" ; do
+ rm "${TEST_S}/${bad_test}" || die "failed to remove test ${bad_test}"
+ done
+
+ # 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 "/^defaultDafnyExecutable/s|=.*|= '${dotnet_exec}/Dafny.dll '|" \
+ -i "${lit_config}" || die "failed to update ${lit_config}"
+ sed "/^dafnyExecutable/s|=.*|= '${dotnet_exec}/Dafny.dll '|" \
+ -i "${lit_config}" || die "failed to update ${lit_config}"
+ sed "/^testDafnyExecutableCompiler/s|=.*|= '${dotnet_exec}/TestDafny.dll for-each-compiler '|" \
+ -i "${lit_config}" || die "failed to update ${lit_config}"
+ sed "/^testDafnyExecutableResolver/s|=.*|= '${dotnet_exec}/TestDafny.dll for-each-resolver '|" \
+ -i "${lit_config}" || die "failed to update ${lit_config}"
+ sed "/^defaultServerExecutable/s|=.*|= '${dotnet_exec}/DafnyServer.dll'|" \
+ -i "${lit_config}" || die "failed to update ${lit_config}"
+ sed "/^serverExecutable/s|=.*|= '${dotnet_exec}/DafnyServer.dll'|" \
+ -i "${lit_config}" || die "failed to update ${lit_config}"
+
+ dotnet-pkg_src_prepare
+}
+
+src_test() {
+ # The test "dafny0/DafnyLibClient.dfy" expects to use "DafnyRuntime.dll"
+ # from the "Binaries" directory.
+ ln -s "${DOTNET_PKG_OUTPUT}/DafnyRuntime.dll" "${S}/Binaries/" || die
+
+ 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
+ --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
+}
diff --git a/dev-lang/dafny/files/dafny-4.4.0-lit-config.patch b/dev-lang/dafny/files/dafny-4.4.0-lit-config.patch
new file mode 100644
index 000000000000..31e6619c0c44
--- /dev/null
+++ b/dev-lang/dafny/files/dafny-4.4.0-lit-config.patch
@@ -0,0 +1,14 @@
+--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg
++++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg
+@@ -215,9 +215,9 @@ def find(name, rooot):
+ return name
+ return ""
+
++import shutil
+ solverPath = \
+- find("z3-4.12.1", binaryDir) or \
+- find("cvc4", binaryDir)
++ shutil.which("z3")
+
+ if not solverPath:
+ lit_config.fatal('Could not find solver')
diff --git a/dev-lang/dafny/files/dafny-4.4.0-lit-system-boogie.patch b/dev-lang/dafny/files/dafny-4.4.0-lit-system-boogie.patch
new file mode 100644
index 000000000000..b661ccf96af6
--- /dev/null
+++ b/dev-lang/dafny/files/dafny-4.4.0-lit-system-boogie.patch
@@ -0,0 +1,11 @@
+--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg
++++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg
+@@ -107,7 +107,7 @@ testDafnyExecutable = 'dotnet-bin-6.0 exec /var/tmp/portage/dev-lang/dafny-4.2.0
+ defaultServerExecutable = 'dotnet-bin-6.0 exec /var/tmp/portage/dev-lang/dafny-4.2.0/work/dafny-4.2.0_net6.0_Release/DafnyServer.dll'
+ serverExecutable = 'dotnet-bin-6.0 exec /var/tmp/portage/dev-lang/dafny-4.2.0/work/dafny-4.2.0_net6.0_Release/DafnyServer.dll'
+
+-boogieExecutable = 'dotnet tool run boogie'
++boogieExecutable = 'boogie'
+
+ config.suffixes.append('.transcript')
+
diff --git a/dev-lang/dafny/files/dafny-4.4.0-no-copy-jar.patch b/dev-lang/dafny/files/dafny-4.4.0-no-copy-jar.patch
new file mode 100644
index 000000000000..96ab9fc4a723
--- /dev/null
+++ b/dev-lang/dafny/files/dafny-4.4.0-no-copy-jar.patch
@@ -0,0 +1,21 @@
+--- a/Source/DafnyPipeline/DafnyPipeline.csproj
++++ b/Source/DafnyPipeline/DafnyPipeline.csproj
+@@ -89,11 +89,6 @@
+ <LinkBase>DafnyRuntimeJava</LinkBase>
+ <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+ </EmbeddedResource>
+- <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntimeJava\build\libs\DafnyRuntime-4.4.0.jar">
+- <LogicalName>DafnyRuntime.jar</LogicalName>
+- <Link>DafnyRuntime.jar</Link>
+- <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+- </EmbeddedResource>
+ <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntime.cs">
+ <LinkBase>DafnyRuntimeCsharp</LinkBase>
+ <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+@@ -128,4 +123,4 @@
+ <EmbeddedResource Remove="..\DafnyRuntime\DafnyRuntimeRust\target\**"/>
+ </ItemGroup>
+
+-</Project>
+\ No newline at end of file
++</Project>
diff --git a/dev-lang/dafny/files/dafny-4.4.0-no-output-jar.patch b/dev-lang/dafny/files/dafny-4.4.0-no-output-jar.patch
new file mode 100644
index 000000000000..332fc4ffb49f
--- /dev/null
+++ b/dev-lang/dafny/files/dafny-4.4.0-no-output-jar.patch
@@ -0,0 +1,18 @@
+--- a/Source/DafnyRuntime/DafnyRuntime.csproj
++++ b/Source/DafnyRuntime/DafnyRuntime.csproj
+@@ -28,15 +28,5 @@
+ <PropertyGroup>
+ <DafnyRuntimeJar>DafnyRuntimeJava/build/libs/DafnyRuntime-4.4.0.jar</DafnyRuntimeJar>
+ </PropertyGroup>
+- <Target Name="BuildDafnyRuntimeJar" AfterTargets="ResolveReferences" BeforeTargets="CoreCompile" Inputs="$(MSBuildProjectFile);@(DafnyRuntimeJavaInputFile)" Outputs="$(DafnyRuntimeJar)">
+-
+- <Message Text="Compiling DafnyRuntimeJava to $(DafnyRuntimeJar)..." Importance="high" />
+- <!-- For some reason the DafnyRuntime.jar was often not (yet?) created after this Target was run, leading to build failures.
+- We've removed the 'clean' step that was before 'build', so the DafnyRuntime.jar from a previous run can be used. -->
+- <ItemGroup>
+- <!-- Register the generated file to be deleted when cleaning -->
+- <FileWrites Include="$(DafnyRuntimeJar)" />
+- </ItemGroup>
+- </Target>
+
+ </Project>
^ permalink raw reply related [flat|nested] 4+ messages in thread* [gentoo-commits] repo/gentoo:master commit in: dev-lang/dafny/, dev-lang/dafny/files/
@ 2023-10-30 23:15 Maciej Barć
0 siblings, 0 replies; 4+ messages in thread
From: Maciej Barć @ 2023-10-30 23:15 UTC (permalink / raw
To: gentoo-commits
commit: 467b53be7e33f8c51436b04116c94f331131f527
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Mon Oct 30 19:26:53 2023 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Mon Oct 30 23:15:54 2023 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=467b53be
dev-lang/dafny: patch out .NET framework
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
dev-lang/dafny/Manifest | 2 --
.../{dafny-4.3.0.ebuild => dafny-4.3.0-r1.ebuild} | 3 +--
.../dafny/files/dafny-4.3.0-net6.0-upgrade.patch | 22 ++++++++++++++++++++++
3 files changed, 23 insertions(+), 4 deletions(-)
diff --git a/dev-lang/dafny/Manifest b/dev-lang/dafny/Manifest
index a5d0ea69c4ad..f3a77f80609e 100644
--- a/dev-lang/dafny/Manifest
+++ b/dev-lang/dafny/Manifest
@@ -85,8 +85,6 @@ DIST microsoft.netcore.platforms.3.0.0.nupkg 29497 BLAKE2B eb1e21bb3a3d3d3a65b13
DIST microsoft.netcore.platforms.3.1.0.nupkg 29544 BLAKE2B 2739d62e92e61677964f9ef380ef2f72ddb6879444d7e744c283a73fdf4ad69c07c36a0b3c4030312b0a4c622aa91dc09cfa828ab8dcd9cf0c5506aa2fac5c8c SHA512 636a1e3768f782ced193b18ec61616c122b5b756395bbec3ede805b172ce62db2d631407deebba73bf136234479be4824f0268a57f52ff4f8d7d37d4370cd966
DIST microsoft.netcore.targets.1.0.1.nupkg 18189 BLAKE2B d43a064d4c6f836be5164708ff0401913b32fc3340cad7c8fd08f421ea553805ac150a134a0d60a55d41eec124514a5e5197eebcc85aa6595cc6b91e33025d61 SHA512 6ed8e75f945a18651066fe9ee31cf6c8257a5974340fe4d262438903c4959a479f4a515a4d1389e6d3d3ab34f09a3c7bc2009aada2e8a7f697b6655a82d3bfc9
DIST microsoft.netcore.targets.1.1.0.nupkg 18162 BLAKE2B 419d19e0da934ab4b9db75dd66cc22b83a003f34e93cf7a92feccf4f32d3d695e18b826b1aba13073dd4ec53aa7905a67346921d1055516647ddcde0d79009f1 SHA512 1ef033a68688aab9997ec1c0378acb1638b4afb618e533fcaf749d93389737ba94f4a0a94481becdf701c7e988ae2fe390136a8eae225887ee60db45063490fe
-DIST microsoft.netframework.referenceassemblies.1.0.2.nupkg 20957 BLAKE2B e521646690b142a703d943cb0528552a669ceed16fa71e3a04300da1eb58d5428b168628c85b8e963e963cf0041b0a02d7442414248e6f506ff3d7ae452a85cb SHA512 8bf3922b695856059b8eec696a7ace03a7269d71d4c456cbdfb21bd3f6e69f2a9fa25e46acd5c29ad872829a07cc05ec083c3a6ee942bca21afd47ce3bc533e3
-DIST microsoft.netframework.referenceassemblies.net452.1.0.2.nupkg 19845441 BLAKE2B c2be1acfd4207984ba33a5ed468fea39299d61d6af99ef9cfc7df16096c0ecfb6133a3c970ffc150f79566710a589c5a387a5d2da8d5ce25f23173cfcfcc7661 SHA512 f4b099aa012c3d117c58dafcaa3edfc273ad7d5acf30c84d213eb15ae101559e7da3f1810285909153e85d73ac58dfedc34e6730c264cb0ae013e19a1213d691
DIST microsoft.testplatform.extensions.trxlogger.17.0.0.nupkg 361862 BLAKE2B 7315293c1ab965bbcc299a842a2e1f462e4821168f79f3036f7a14a4116f3d73c00f5b645bd1d16fc963f595e65ae11d7658544a6482c0e5926b36528644b259 SHA512 d72f41fbe9d4155b85d0e20e6a476d41ea55e355c61561270f241a1b2ef5b9d8dc9c81ca43d14c550a50bff0a301923e9e84a5035e5b31006a9639ba0221e907
DIST microsoft.testplatform.objectmodel.16.11.0.nupkg 2966263 BLAKE2B 5bf6464154b639b478c4000dd64e7570d124a446680583bceafee1cf3eafdc6a7bc10cacc665327a562a28fe0268c5d749dad0ef11376880f76310f1e3cb055c SHA512 105ec3c2d2d476abfa9fec73b25a701d815b743512b575e7ee2373ef7e459f767688be7ecdb555849a8342e07e922ab819dfae637e8b23b36ed918655d9a7471
DIST microsoft.testplatform.objectmodel.16.9.4.nupkg 2224614 BLAKE2B c8b0899000db731c0041f6209e4f85d2bbee5a7ebe3d3addd4405a33e1036bef52098c3fe8146123db262e71868d7bbe541149ef7443c7fc718ca78f916d384b SHA512 a1fc8192007d0d1a852393eadea26b8400df81a50d8a29549f79f726694696b2c361460561a3910f66dc195044b7773addc25642f9c7389b7152489e162f9ad9
diff --git a/dev-lang/dafny/dafny-4.3.0.ebuild b/dev-lang/dafny/dafny-4.3.0-r1.ebuild
similarity index 99%
rename from dev-lang/dafny/dafny-4.3.0.ebuild
rename to dev-lang/dafny/dafny-4.3.0-r1.ebuild
index 216aec617ebc..78bc91322e3f 100644
--- a/dev-lang/dafny/dafny-4.3.0.ebuild
+++ b/dev-lang/dafny/dafny-4.3.0-r1.ebuild
@@ -92,8 +92,6 @@ 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.0.0
microsoft.testplatform.objectmodel@16.11.0
microsoft.testplatform.objectmodel@16.9.4
@@ -417,6 +415,7 @@ PATCHES=(
"${FILESDIR}/${PN}-3.12.0-DafnyRuntime-csproj.patch"
"${FILESDIR}/${PN}-4.1.0-lit.patch"
"${FILESDIR}/${PN}-4.2.0-lit-use-system-boogie.patch"
+ "${FILESDIR}/${PN}-4.3.0-net6.0-upgrade.patch"
)
DOCS=(
diff --git a/dev-lang/dafny/files/dafny-4.3.0-net6.0-upgrade.patch b/dev-lang/dafny/files/dafny-4.3.0-net6.0-upgrade.patch
new file mode 100644
index 000000000000..5c43ca90ae0e
--- /dev/null
+++ b/dev-lang/dafny/files/dafny-4.3.0-net6.0-upgrade.patch
@@ -0,0 +1,22 @@
+--- a/Source/DafnyRuntime/DafnyRuntime.csproj.orig
++++ b/Source/DafnyRuntime/DafnyRuntime.csproj
+@@ -6,7 +6,7 @@
+ <GeneratePackageOnBuild>true</GeneratePackageOnBuild>
+ <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
+ <DefineConstants>TRACE;ISDAFNYRUNTIMELIB</DefineConstants>
+- <TargetFrameworks>netstandard2.0;net452</TargetFrameworks>
++ <TargetFrameworks>net6.0</TargetFrameworks>
+ <OutputPath>..\..\Binaries\</OutputPath>
+ <LangVersion>7.3</LangVersion>
+ <PackageLicenseExpression>MIT</PackageLicenseExpression>
+--- a/Test/comp/separate-compilation/Inputs/producer/TimesTwo.csproj.orig
++++ b/Test/comp/separate-compilation/Inputs/producer/TimesTwo.csproj
+@@ -2,7 +2,7 @@
+ <Project Sdk="Microsoft.NET.Sdk">
+
+ <PropertyGroup>
+- <TargetFramework>netstandard2.0</TargetFramework>
++ <TargetFramework>net6.0</TargetFramework>
+ </PropertyGroup>
+
+ <ItemGroup>
^ permalink raw reply related [flat|nested] 4+ messages in thread
end of thread, other threads:[~2024-02-10 16:25 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2023-12-13 17:17 [gentoo-commits] repo/gentoo:master commit in: dev-lang/dafny/, dev-lang/dafny/files/ Maciej Barć
-- strict thread matches above, loose matches on Subject: below --
2024-02-10 16:24 Maciej Barć
2023-12-13 2:27 Maciej Barć
2023-10-30 23:15 Maciej Barć
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox