[gentoo-commits] repo/gentoo:master commit in: dev-lang/dafny/files/, dev-lang/dafny/

[Maciej Barć]

commit:     3caad7d601b6fbdbf25e17d445db7f6361570d8f
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sun Mar 17 17:01:28 2024 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sun Mar 17 21:53:18 2024 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=3caad7d6

dev-lang/dafny: bump to 4.5.0

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

 dev-lang/dafny/Manifest                           |  16 +
 dev-lang/dafny/dafny-4.5.0.ebuild                 | 620 ++++++++++++++++++++++
 dev-lang/dafny/files/dafny-4.5.0-lit-config.patch |  20 +
 3 files changed, 656 insertions(+)

diff --git a/dev-lang/dafny/Manifest b/dev-lang/dafny/Manifest
index b1836de83ec8..a020a031eeda 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.3.0.9.nupkg 29646 BLAKE2B 
20b0e150d3a9a6ed11a24cd9920a97971d515207d86864a9b1cd4d554b2b3c34e27778051a9bf6d8b3178352a6cfbb33c363b2d69958f6503e17e366ca3e1147
 SHA512 
26b75a409b4bfe5dd4ac982ca2c1b03df2118254a9becaab74f4d44b652746faa0448ab943ee9177f6a0fd105f8ce015a4403b6ff58df12201b542c50618b222
+DIST boogie.abstractinterpretation.3.1.3.nupkg 29640 BLAKE2B 
6ebadfc92014018649ba1998f878ca8d8cda2df25d8b7f5243becd27bcafbcc166c071769adabdc99098b4fbf4aee8a6de8be9f8da43b3a3e1511dba96bbf2d1
 SHA512 
b950ceab224aca2a6d9a0202d2f79dc59f5e8f18f710933d843e8eb6dae9badadf6f78e79297f74bbe35a9d9170f2c928174c93a6edfd70e79aa282348b4be58
 DIST boogie.basetypes.3.0.9.nupkg 25717 BLAKE2B 
c1e549c6d7c675fd3b1acbe1a39fb5854d182b70ebab734350439dfd0cfd2be879b1d2b9c91ad832dae8e6f695fbc41510285bc7573b11fd51a170d4bbc50780
 SHA512 
d561f66a89af09cc07596bd1079993010a325ab2f22f2cc85408d12fd1286b15b0d7774b2e4037465a3b78aa829205f77b8b0b2efae9b9f3145eca6e82ced4d0
+DIST boogie.basetypes.3.1.3.nupkg 25710 BLAKE2B 
e45663df336757dcc448f2ebe4f150948504047a1d5e4814fba81b0c08d7480aa717a42ebaa1ef9714276093a0d2755780669d0af410dda4806181c513874bf0
 SHA512 
ce3bbdf67d1332a51dbfffc21f12cde720b6583638dd7b6bc1fb68e5e6a7d1d6f0a191e795728b79adc1f113102996475c0290afb7062bd1122a17c1d6d1605f
 DIST boogie.codecontractsextender.3.0.9.nupkg 17455 BLAKE2B 
6a6f060e16942750e52bb72630b306cb591212ddd9960ac9778efe44239300f19b5793bb0cb94cb66e01a16f0337bf77bc6f39d2ce680f5ae94c566e2420331b
 SHA512 
b15d7b0d24d5464189daf797e02b7e6342841de5c7cc3a15c954ee270d805afe0dfc3e5268dba5abbb636e2de2c859bf7a3f442180fd3a7cd2f70ec227fdfc24
+DIST boogie.codecontractsextender.3.1.3.nupkg 17458 BLAKE2B 
2005168450015740d0afd9415c47674bb55f99b2a717ad03f56e0571be1f5532a9abb0a662b3b3f785dab32914684dc0046854c4286ea9be338aa0dcad0e4618
 SHA512 
1508e11342e88ef0fe3a6f7dc758924987b6edcc30f62d0a7e43aaba09cc14b26b999eb0d59faa13e26f246e91b9c176f4c983fdeb653892cff655f40b5bd24f
 DIST boogie.concurrency.3.0.9.nupkg 93215 BLAKE2B 
aa8e969eea49750503249b1f196ed3c4f388fae2a39c46c61c4dcc343feb15b3d98d0b87065afe1f82fa0d8bbeea895b3362bc2ecca26daba0b0316ab8fad648
 SHA512 
618e4e3c06354b8ff8e6c23341915f1bd92366aa99dd8f9ef217110191f653be2a4d30cb83d004d4a34dcd7244e9f0603179859d1371109f1ae7706046643cbf
+DIST boogie.concurrency.3.1.3.nupkg 92168 BLAKE2B 
81ff170058924043a10c83aed60ea38951bca7ff35de3d8be29fcf68fea9da2d658ba0abf36f0fa93e4c9f96b0a81f96b550396ca55e3ac204b4e21e49d112bd
 SHA512 
069c34b152ccfa9ab8903b6beda6090fcbfbad243d79dc473c01e30d19a6a5ed15528120180ad271d28b43eb520dae6e221a9256680b7e241a6bb83415988d93
 DIST boogie.core.3.0.9.nupkg 208520 BLAKE2B 
180b099ac167eb4cdc2b96ebfecc0e70789d0bcb01fe2842b69520b1757efbc8cf0ca56846dee6ab17d5a88c38920273368803d646a143f4010926de81c420c1
 SHA512 
eaa0289840caed37aee889a66b60e0389729f2233b568c58de22790fd3eb3e93478b17d58d290c1622ccb7bf788f8a98cb942ed6124c8aa3efe5beb44889fbe0
+DIST boogie.core.3.1.3.nupkg 208304 BLAKE2B 
c3affd650c0c81c61e39e5bba0e3f88684fe43169c59b60aa15ef532747ed624d3b4d2a1ebf1fef6d216bb380b535c62a48cce072bf4a3ff57feea907c48ca8c
 SHA512 
ae611fe91b8189ba55315db75be7fd927d08ae096305d099aa5b51ef692b4c5f4633c7cdcc95f9344791f7e11414e4078a8640127e2442f667594b335338eb1e
 DIST boogie.executionengine.3.0.9.nupkg 83903 BLAKE2B 
c3b8caf6097ab8f2b81b72593d7802674a8f6069f5601431a709095e0c785dea07c8b7b4033954ee7786e518973c9fe275d59be698918bcb5177bd90e3583525
 SHA512 
d80374d6df8f663ddef0a2bf004e9f414ca9d79e02861344f5878a1033db17a7d5102f92c4299e16ad5d1cf421a7cec4702dc320a5969a7699bcd2c31e933a1e
+DIST boogie.executionengine.3.1.3.nupkg 85951 BLAKE2B 
4dc3e7c442d2fc8f79b8f17c5139bf28453205f7fbb22caf35cdff40ff5294e940820e44029669e4f2103ae4dda56ad34b5d3d76dc73327d8925e6c5384859af
 SHA512 
d06372aa80356ee5b07dd6cd30495246a5d900727fd7c6bba52faef25aabc191b5d89f479ba3c936a2a31a0045c8c195e9099d4c87231c14705ff00ac37b8c84
 DIST boogie.graph.3.0.9.nupkg 27933 BLAKE2B 
5ba929366367792f0288655c5f304ac6ad88d3a89c84df5082d78939306bd6e3441a1c517a060fd1c32eaa7d25e14a3eccf7c40873d413b68a5c36a109353ba8
 SHA512 
1b65fbf349c9516a18e2cdb876a343ee037096ee528933edc2565e43c5e79bcb2dcc56b7e095b150f6c70aa55b217789d04e6c4109e369cd2e9d96c465fd76f8
+DIST boogie.graph.3.1.3.nupkg 27927 BLAKE2B 
66694f02030c943892514881969c05be58d2a9cc4e4ca44a7b6115908a2e04e104350b706b19346e5ea7d659101532ffba2cf0ac919157102c7832185f4cf112
 SHA512 
f50c932d6ca907f359f698c02cdf857cf21b47ec6671ec917f4ae5a03db5b02cfdf3bc075b4ad840ab31c44db343aac2fe0d623d555f17e3ce2d9cf0f5efe9e3
 DIST boogie.houdini.3.0.9.nupkg 52700 BLAKE2B 
686c532de540e11d70be62bf95f6398c21e12ff9386a295b21d58882d105933068524d865b93eba8996bc29f80b05285196a2253493ddcaee13217797b0506ba
 SHA512 
6ea2874623a582529e2e6921ca4c05e76602e6bf11f53323dbb5269e6201b1e1d2ec9bba7641a4918a95fb64f5a488841fab92da8ecc7c3fb033d0e286a4d0a9
+DIST boogie.houdini.3.1.3.nupkg 52727 BLAKE2B 
4a37e98bc0ab9bc8956e81df2541bf1bcfb50c32258b94818a5c8cafbcc74c76d4cfc5432a2e1ee94db5fc503dddd020123cc4f5f4a47c6b3bc8743b47784a04
 SHA512 
0f83ea50aa6f453d741cc7ff28a00ab9e9205a90caecaf7ccbd49d5b9217ec3bf9f5e1a7e9cce83314f48f25ee32c682c9509d00ed7bdcee602827f78712ce31
 DIST boogie.model.3.0.9.nupkg 26904 BLAKE2B 
ebc9e26fe815a7133e87febf8e4bf7af5af4b565e099dc2dfc45515e4e1a4559643d189c1ba5d0d21d230be958e3751306735c533fc99ed95acca740b22887ca
 SHA512 
54a13e45ff1d53eed7cd372997525008c49075783df30a6159958c319c0ae661599bf08ec6bf9ebcdc45c85c97e2ca1d4cb33139db78a5abc50bd018a55c125b
+DIST boogie.model.3.1.3.nupkg 26902 BLAKE2B 
f384227782a32efa4083412a0820343e301337df11bcf4dc4611ce9022a63387b66a350d921dab484230d29f6a33006e1e56ebbd1818e8d5a4b0b34e61912211
 SHA512 
f6e52696ded95d9be9ec4046917c171cddda7429f63d2a0f188b960950bd9684285ce6eb21d1181b4f582b2d400117bf810a8b5a11a654f43a40c22fef4abbf4
 DIST boogie.provers.smtlib.3.0.9.nupkg 70598 BLAKE2B 
49195c7478a7c82fef6e15fb57bea2ddc891f5145fb7e655fc5b84fa4989d209aa0eff6bca8d57da9d08f6df026ee8cfb14d37953267048f5e191ad0520dcd74
 SHA512 
1c290058568cb170c0774779c8264f5e05700784bf21369852c0b0dd581665e64f9d23f98cd2ee22124b5a2866af56ad59fa56925212eae5b7ba26833d7034f1
+DIST boogie.provers.smtlib.3.1.3.nupkg 70581 BLAKE2B 
ade8aaf77a42dc7aa8ab7a7dcf2eacd00db612b032a7e62d2ddb5f96431e43ac16df282e55fe2cc46b104b721bb1183421b98a22e8823746c6f655c7f7789fc6
 SHA512 
50368434be8277c5dd84edce72fcb1ba107737cedcac0f6ff7cbad32b44bc749912b576e4c1076a840239cf5f84d93354fc8a5fe649121f5ff339316cd53c1c4
 DIST boogie.vcexpr.3.0.9.nupkg 74092 BLAKE2B 
978887817f7d48d26d999b2f0a37adee927506aa6eb2e7a93b78567b8fc67411e1cd56e0ee0876d95473edc0dc5068f69524093f8ffd7b4f109490c815a28b80
 SHA512 
024e898e35c933e4b1c55547624d5a3c531245ac1a8b9c03a2d5955d702bc1d51cbfcac0aaf214e9f0f3decfafaab02761490b02bc6ec5c385c2a20778c33de2
+DIST boogie.vcexpr.3.1.3.nupkg 74142 BLAKE2B 
d523aecb82111a712fe619a69c159213ee4bef8182b1dd5708ff2b84ecd7690bceed5eaa825f8735c373ae7d3cf5ba4385e552f4a332d68fa5740cf862992bce
 SHA512 
540e15a2830b739921e72165a39633bbc5b0a820463d79d7a2a915d2d902d242d9221e12026b6c8f6796d2309f5bff672dae50ff9d27834f2660fb433ce5809b
 DIST boogie.vcgeneration.3.0.9.nupkg 90650 BLAKE2B 
435902e5892351f6aba902d3e3cf89c719c68ccff2075500fab607b6af64dda7837864284a3c44fc3a3ac17201355c1249c5ac2ed4ed61a2f1c3867b1338f18d
 SHA512 
a9bb6155275f6f86ef5be7d26be560c8fd1f6f976da552cb038dd7eb41331ebcfb694f0b6367f73a778550e0545dd695c8a35d568cd0c9bd78fcf30c894cc490
+DIST boogie.vcgeneration.3.1.3.nupkg 90517 BLAKE2B 
d5f0271491a37f7ba806c2a46894c474b0c65d5bc66a659241e9ebffbf63c77a75a3533a615957ced4af1ee0363a34fd2c6803beca59e1fe656a1ba29c5fb309
 SHA512 
e402de9912b9d788520ef615fd80b8dba2eca9938f8321fb9e3f53bf158baedfd4c69f3aa4eaa3fe8f685d3ed9556982001117014279f9440605bac368b521c5
 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.4.0.tar.gz 6241907 BLAKE2B 
43f5b6bed5ea0bc6f8de04650b2f97c0092df1df47aba9bf0c6b9210677077427c67cc80364f659305b7d851c178439a1536864dfb7c6396b4ac6517789fc83d
 SHA512 
33789f10b75a1946aab552f11f40296682156bab7cb08cae431f00f6fdb6b12d3211ec2f423a42adb78a3245b19ab8f772dafca4d1448cb30077268680f73534
+DIST dafny-4.5.0.tar.gz 6365137 BLAKE2B 
6233107e680e04ecc5a0d730bab4d5f2228ff04f9d83fe33688731c4226ae03b06a2c08447beda025e2e34e7d92bf6fbb57de5b6913e8cde9f61ae255d09722d
 SHA512 
d56ba0a28bb235ad2c4baba526b4de1757a6574b9d04a195e541189ba5c24a82a7ca4d3ebbcc50244b7f35043aa80101210568f20656f21169c4cf42c41abce0
 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
@@ -88,13 +101,16 @@ DIST microsoft.netcore.targets.1.1.0.nupkg 18162 BLAKE2B 
419d19e0da934ab4b9db75d
 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.extensions.trxlogger.17.9.0.nupkg 441869 BLAKE2B 
a250401ca8d21f51ee8fae91dc3b83b5453280b22f10b77a481e0e27735ae5cd1c7f0f04dcb0b5b0e74192c3e171e8d7fcad1a5f771835a7ce846d0cc7042105
 SHA512 
9b6c67ded3f150a2daae6f5a6db52d86e0338b3aea60a07dfeec67ca630e3ca9a5a8715c71c5bb0508760b877f5e2bd2f135d7f18f9bab9c81991a2fd44f00a6
 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
 DIST microsoft.testplatform.objectmodel.17.0.0.nupkg 2963393 BLAKE2B 
106eddcbc897147fabc6a7c5509e7800ed4af37fcbd7a05771a1fd752e354677d7f8ff4856015b2cb1cd2ad54ed5eba1d0cc62f58962830e0b84d71bb6b049bb
 SHA512 
19ad56cad83f5897c5b93608be9d357c83ddd5f97f2f7751f40fc017236ae2ef3b0517147e4dba2c4395511a9f4f5b262a4f660a25974e7b34f220c275af9c4e
 DIST microsoft.testplatform.objectmodel.17.1.0.nupkg 3191688 BLAKE2B 
26be3f32f39257044cf0947aaf68b486befeded4901e5344fc7d1df1bba1f8d8e564d310fc946e5d5d4b3462aba1734bb44274f6f471bc27f1a493e2e0480dac
 SHA512 
fb7333c71906dc2a13a3bdb33363e926d0c6066addd1ef43b2b5067a616b754798f32f515cadc58bc2a9c6e157c05e6d36ef79bf602e9da9b37089644933240a
+DIST microsoft.testplatform.objectmodel.17.9.0.nupkg 1655717 BLAKE2B 
5ae125e4fee8770a6a9f18a8566eeeacbbcac42cfd5eed4e407fd2cc2b1d773e20ad0dea461483fa3525cf113ea97dfbad6763a7afa354cf3d438057310d0140
 SHA512 
637048c70b190a0269d7e0761d7cbec7da8d306f5770480cb91286c06047d7f4f1666556dfc4494ec090db011b03fb736ca03313479b566019a5a54567e05f37
 DIST microsoft.testplatform.testhost.16.11.0.nupkg 7327788 BLAKE2B 
eab31bacbbf159a128db837076c2057b4a68b912e4dbc1583f5042b0333bbec78e2718ab2db0a6900c41d984a913115573444695d117f270b272141402db55d9
 SHA512 
17b0956e03edf7660dc31d59d5cd9fb141b3d002149aeed824a2d3381bab2f6a5ccfbcc2fd6c37e960bfd29e33e734db14cd1862799fadc80154f3d8ac3825a5
 DIST microsoft.testplatform.testhost.16.9.4.nupkg 6913327 BLAKE2B 
a82e3aa0cc930a12ecb7d2b8baff82dad9357c6a72bdb2b7cff0e36b5b8cc09ff058f016dcdf21eb1803dbce1759a1179405a0756f88579ec2645568b3cc9a8a
 SHA512 
a5f780bc300d9bfc0c08feb978c36cd5e629207e54abc9d1d80202bf366bdeb13c882ef7a29bd52b50b5b9eb4e5a04737e880e817a853aa178d093ec9aefcda3
 DIST microsoft.testplatform.testhost.17.1.0.nupkg 7692160 BLAKE2B 
4df352512bf2c7ca38e3fdb351dec4e7c9307bc88d83e242e34a1139a8f37fa60e0d4af58cc52d74ac0b82b557917c90057d30a83b06a5d8c7e7db17771bd285
 SHA512 
c661a1581faa059af1886e6dd2d02fb4d9417655758fe73c3dd594f6c6f944ea1a81921379fb02c5832a97c50f8124d0032aa99130bc204481707e76d47dd0de
+DIST microsoft.testplatform.testhost.17.9.0.nupkg 2859892 BLAKE2B 
f7fb36494032105a390f6be4e8655c1d1c92a0b7c5d6da2964537b74f8f19e45e4ac650f8b202f8573d75783a032c68f89b9f4d6c17fbaba681445da0964360b
 SHA512 
c8246c9b365a8afebf35317357125563819a3ea68b1a2ec4d95cd44838efb2f121be5710250a68ceb06c7a052606bff1c202a9504ee2d20cf65f66463b43d31a
 DIST microsoft.visualstudio.threading.16.7.56.nupkg 989616 BLAKE2B 
03e41384a3c1dd2ff4faca011b714d66130fa4f7088eebb925d57b5df0329ba79a3066289e2c1a20ba6daf833671f3ae1c6224e24c2a80f37b05fbf6d7bcce0b
 SHA512 
0b31f9457e9778e3fde9ee612f8dfb065c6b51299b4f9e6af0c75f68e692e53409a064d0d53fcea466c9a41df096f7d121509ffcfcd12039393c30766ace11f1
 DIST microsoft.visualstudio.threading.analyzers.16.7.56.nupkg 502163 BLAKE2B 
9bcb2044060ef67d81a1d8b08a7042621dc05113e176b1f2a0fa7c961ad74491c9612e0d115c823655161769b25ddd7afbcbc6a20d2ea0fe16794984b2dabbde
 SHA512 
b2021b6e8bd2bd703bd928fbabfcd9763106c85e4c97e3c7a894da3a23ad9e0a3c8a8c7b0b4c42469c1566f515ba52bae0827f82a29a4a4cfc3bebafad6339ff
 DIST microsoft.visualstudio.validation.15.5.31.nupkg 262234 BLAKE2B 
8f4714d3daf386a2b40a04d48077b09a4e0c071f4af3c33ceefb3806d6cef3e068a55e9ae092bf6ca345b6e84d57ea9827cad11b16f6ca58c21d0ea324f71a5b
 SHA512 
2e777e6fa306b87c21efe604a6a7e6911299803895ba7f503e3870a58898ee511a32402d38190f6a971053227904f0e97d994c12687f927b77b26bac536da042

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

diff --git a/dev-lang/dafny/files/dafny-4.5.0-lit-config.patch 
b/dev-lang/dafny/files/dafny-4.5.0-lit-config.patch
new file mode 100644
index 000000000000..87ce510a3592
--- /dev/null
+++ b/dev-lang/dafny/files/dafny-4.5.0-lit-config.patch
@@ -0,0 +1,20 @@
+index d7945a9..2a175fe 100644
+--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg
++++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg
+@@ -106,7 +106,7 @@ testDafnyExecutableResolver = 'dotnet run --no-build 
--project ' + quotePath(os.
+ defaultServerExecutable = 'dotnet run --no-build --project ' + 
quotePath(os.path.join(sourceDirectory, 'DafnyServer', 'DafnyServer.csproj'))
+ serverExecutable = lit_config.params.get('serverExecutable', 
defaultServerExecutable)
+ 
+-boogieExecutable = 'dotnet tool run boogie'
++boogieExecutable = 'boogie'
+ 
+ config.suffixes.append('.transcript')
+ 
+@@ -217,6 +217,7 @@ solverRoots = os.pathsep.join(
+ print(solverRoots)
+ 
+ solverPath = \
++    shutil.which("z3") or \
+     lit.util.which("z3-4.8.5", solverRoots) or \
+     lit.util.which("cvc4", solverRoots)
+