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

["Maciej Barć" <xgqt@gentoo.org>]

commit:     d58a31606e80b160b3ca0f85a28aac902b209072
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Thu Oct 31 19:31:51 2024 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Oct 31 23:17:20 2024 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=d58a3160

dev-lang/dafny: bump to 4.9.0

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

 dev-lang/dafny/Manifest           |  16 +
 dev-lang/dafny/dafny-4.9.0.ebuild | 643 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 659 insertions(+)

diff --git a/dev-lang/dafny/Manifest b/dev-lang/dafny/Manifest
index 7d25e48b5003..440323e040a4 100644
--- a/dev-lang/dafny/Manifest
+++ b/dev-lang/dafny/Manifest
@@ -1,36 +1,50 @@
 DIST bignumber.js-9.1.2.tgz 79226 BLAKE2B 3d2ff19d73a6fcfbcc0d03d1e9808796baae639e19973cbe0c26af4b514abc299129b8a7bc3e4e803c61af44b76f4381b1965d8fa331ea43e8a4c8fc7f98d8e7 SHA512 dbf98ac991fd2bce5bcce11f8570c11594c6775093b3ee481e9785428f65ba2046ee1821742f39d4f8f658085be84dd1e9bf6d663fd72a16e0e1fba6f8a7a9ba
 DIST boogie.abstractinterpretation.3.2.3.nupkg 31090 BLAKE2B aee6df566f9d40c958bb04cbb81f5f7b588f5facdb2bc211f41181bdf0e94f30d00c71202faab9eafafc865cb4d1c073798257f64ec25091fb14e9948b3c4a9b SHA512 dee7af159ac9de16a87cf9636e798d5489ba75815cfa5c911ed1473b4c4a80b1ac0f450efcd73a4e1aded2b89632b8512ab619c9b8ed11bd870d6a9f29bf1693
 DIST boogie.abstractinterpretation.3.2.5.nupkg 31088 BLAKE2B db290f4e6830377d4782cb6afcf8acb9f316668e558d8a403aac45158e39ab229a155f0fad1ff325661a9c4f1cf3dfbba9690fd4155f879ad8ea6367f1cc499f SHA512 e7b988dd72201d4aa9c804d8a44d3b77cc9215310ee360407942526bd5a6ac435b11119406b6264e743cf884c6c31b04f2bb00722d059e2df8ae5f0acb999275
+DIST boogie.abstractinterpretation.3.3.3.nupkg 31066 BLAKE2B 67a25b1fcc9bc86a9603929c8f8e01cb6c387bec1092167ac9d3a69bd5fdf242553514ff3f0395e60ddbb0936a494d4897460f9fdeafe3303d487ec08e796579 SHA512 99199633cc95db44b41bc84382eca1212a2864f7dd900769f259442dfaf1f8554abdc6d2bdbc7280603c074c77185968fff971fb96d635a308329f38f8f8effa
 DIST boogie.basetypes.3.2.3.nupkg 27125 BLAKE2B c83f69ae6e6be944848c2e2280a97c0a8fce63c89f2af3511406731e83ce516d456b5f829b9b41d4188f96632b2321c448274b24c90fe92ba44c12ca11db80af SHA512 2825119e1eaf57c9070ed09ee722e7b10f05450861734edbba3163dd6b4d3d775a4b5ff31e65644a23b525eb5e59db7a36b3dcfc394a81bf820bd8366b52fb12
 DIST boogie.basetypes.3.2.5.nupkg 27123 BLAKE2B ef7e958ff952c03286110de27a5cf9647c97bb4ae454052bdcc305482b6cf19fbe137d0efcae35652bf1f0e62a15c23078634837eab62f76cde9aa99d5fe901f SHA512 988956020be1a8471d11b854a476f3b545423e153aa1cb57d46632a4a55a57013cc54c5d03710793f54d182bc177c6c7c4810ee85da5d01b7ecb4181043a31e5
+DIST boogie.basetypes.3.3.3.nupkg 27107 BLAKE2B 169ee92d8d0d21885ec3fdadf31c498c6f676f93ccfb1225c82703254065f92090a8242fb51bc3eaf5636d43c27264176677e31c791b79ca71914872a53cf0c0 SHA512 4b59336d85a6ef7d236ba0653ad708cffcd53240db1293d9a1df5c5cbdae071091b22c0f4cc6b8385e7569ca5099b520d05196c3f10396ef5cfea1e4666a0664
 DIST boogie.codecontractsextender.3.2.3.nupkg 18877 BLAKE2B b5a05599b2d0d9e63b6599b7eac34f97dda4b1ab4cc1816e9daa646843d3c5ecf4e8a42fbb4f4629805fb331b73e16ac440db8db520323c9c8420b29571a73f8 SHA512 368f3b6273bb4c24e66ddde7ebf3623a5a35bfe57e21e651cd448a80fa62d2376a2c06702938348e86d7b86004f912a9ca86e774cf5bfb6bdbb3ce7146dbf12e
 DIST boogie.codecontractsextender.3.2.5.nupkg 18869 BLAKE2B 633f10027f1ee70e872230658f2bc5128cb4c91659701c9580778d9bcf13f56982b7f1c181109b5cb69fd5ef108befb2c79334dc6445c51e4550453a4f58a4c2 SHA512 c97092e8c855006eebfc0e26feda9d984a63401e4412b3fdf54707fc56ccc5013e21669dc9d43b7159d7559957fc6667355aea5f2b04deaf9f947fa1392126d5
+DIST boogie.codecontractsextender.3.3.3.nupkg 18854 BLAKE2B 68a7ed901692d64065f5264510fe2b93c52b9fd097b8dfba01d9a55b4988165a6c41098d37937f9b4c96434fbd6cc922d826d7d62d2678b535881ee84937d316 SHA512 62a721dcf2f1e7d0a915c5597566b3a6f125fad43fa9e2623ef475226632fe1baacae845065e95dde6967b857900244708d400436301be0da8789d1d23069ade
 DIST boogie.concurrency.3.2.3.nupkg 97612 BLAKE2B 77239e015b92346d31c315e80dcddda8f439ec7238ea10c0f11020eb67cc3ed04363c50a81194321769cdb99b75f37e95acdddbf4f824ece4ba866c8607743a5 SHA512 5924fba9164bbe18aa3b76742d7ad2cc6f12e6744304a7d15e0d55778b8da71bb63ad83bbfce02101302173ada146e1369274d81fc500e0517fa1454bffa1d55
 DIST boogie.concurrency.3.2.5.nupkg 98018 BLAKE2B ae550ef7fabc4e782b1571206610bf6f43acce7a60a46d3ed4f1dc554f2a61b2426be23ddc3a0ba8e206c406762f311c94eaac9b6f830cbd28edc9991a659133 SHA512 47bdaaddbe67e8fb2f873daee2ec2086152a3684ddfd90a6e4dab327be7db58b4419e764e69e1f62658bc643ed621064b5dc537e421de30b9b3ca4fb11e1d652
+DIST boogie.concurrency.3.3.3.nupkg 98537 BLAKE2B 259df99b51fdc2badb00e0a0f5c8ffcfd209024a84536324de51a7f917e20fdab3ce773d70a66514d566f65efbe25a5731c506dcaf483da15c898df458d30c93 SHA512 109468cf5dab7b72f99ece92a396e1fde8a35fa20cf2c1c4fd0d73476418a98a16d4caadbf587c317d3b446f411f91ecf43c0416d7431b87cb87b882e14d3a4c
 DIST boogie.core.3.2.3.nupkg 211644 BLAKE2B 175ed102138abed57b0efe41fa340866b9286c2fc1702d35941ba53307c604329bc41838fed5f4aefc9e878741db325621ac5f5a019681d7055f7ec39b4548df SHA512 1f9fc1d698c248efe4fce7a2fe43d75ccafe1c85c311468343e24ba595ae4cc9a8007fc804572238639e55b43ab980728c5ce52572294223e10f6de4d8feacd7
 DIST boogie.core.3.2.5.nupkg 212325 BLAKE2B af501c8617be9cc0eed2f66eaed27411177aabea82d070a5394e2ff03bcd929fbcc82c3da0c89f894cccfed11356d8d3ac1adcec7062490392a56558039fe9c0 SHA512 1de2e2d3e0476793ff7082145173d2ef6092673cf725f97b5854a516b9493c099bc7cf03371c932bd43d7ca473236e10728ae1d3623aaee44f084de7b7145820
+DIST boogie.core.3.3.3.nupkg 212137 BLAKE2B fc14029a416a6fd3fad4d7ceb98a67c9a75f0b8d1016fd031b499485005670f8f133a0cecc4d5ef87e4ad9f37bcf24cabe9628c433befb518b7a18d3f8763027 SHA512 ae87ffe73ac5bc531de66948f07daee0854af70ef381720d771b6e239f156968868e82b36d55f89b455606e17f42e332484694b3a5f93c5a43a67544587eca80
 DIST boogie.executionengine.3.2.3.nupkg 88881 BLAKE2B f94d2403a9f62601b865c77a008e0cc6f1284b2666de51b5c977d480a65e39c4bd4895f1181b66fc04297d4081c12eca34e978b1a53fb03ec991a12ee95c58b7 SHA512 d80544fe9952b1000c89844c57244e14181e407cc9325778afdf9c95eff18fbe166eb14d24a1ca1376ecc1428c8d88a69bf6881132c6649a9e4cf69f2c137b20
 DIST boogie.executionengine.3.2.5.nupkg 89582 BLAKE2B fb07d43f27f564c43206bc5681f7a24b5e0d92a813a80c973afcd4245289c2172827148d9d09e168aaa4bce21de78ad7be6460017eb9ae5d8da107cff41b0364 SHA512 0709c423e18b00ecc5ec283a1463f35cac4950482ab93407344ada434c5217b720fbc977b480afa7cba8cfb7280af065d7b88c95d0829bb269a2e0e41c0201c3
+DIST boogie.executionengine.3.3.3.nupkg 89701 BLAKE2B 1bbeaf4901e04c6dbaab3802d4f9af9eb64552241fb86b77f1d67af92b7c0020fc00bbe20d5fd1f813b6be4420ec75e208b662c4ffb9c7476884a914b611f6f0 SHA512 7db9aa9448572aff856f60193c25cfbf0dd913e0f8d22b05506ac9566d6f13bd1ebb5f235a3e030db18b7d2ced358ab8252b3a327fc975795e61d6cf77eb196d
 DIST boogie.graph.3.2.3.nupkg 29420 BLAKE2B c686a976ca8761d6ba311d9a7c285a393fc7966d991dac4e6c6890432fd29e102b1badab61249275dddb57caa4319069a5d466e7ed7219aabbf8a35343d62714 SHA512 39ff97c48ce7dfaebcc601d866d040f5a5d4d1de44121cdde03c1557c90f8a00a11c9c2670f66b12fc210af2bc58fa5804657c8978cd1130d7b67a8c56024742
 DIST boogie.graph.3.2.5.nupkg 29379 BLAKE2B 3e13d4e08b247ebcb3220e2e2363bb9d7f6608ae27a652341554549bfc4fbe57ba46254e160e5783b64fb185c028911479678e96d23bda4ad21d1dbfa16a681b SHA512 3a7b3e980cf0b7a7251833f33e4100e5c942ae3818860b11266415cdf247b4f0603c6f0dd845526f791f0ff5f3eccfa2b81be97edf6987a7f359ce5b3e021f0d
+DIST boogie.graph.3.3.3.nupkg 29388 BLAKE2B 80174bf6bd91973b7574998990dae55bf1da66343a0946dcdbc5d10d2537de2b90980eef7340b73263e7d6460c676431160f6807740119e592ffb535e203d73e SHA512 9be27eda4161875a307c397c06a819472290ca7bc6980ee32b9982a8ab636a60910af29fb58575369f14921846d392e3d2df38986931402121d6f41b6e7313cb
 DIST boogie.houdini.3.2.3.nupkg 54152 BLAKE2B 7af01af66224141598d60a847bb2bf2e6e68d049992fc838d75397e216f504e4b140d5a94b459332b6f35628070a9960708ba324c645c8b425fa4bde661cfb44 SHA512 dcdb9a53be6587b03e134a56d931f4b1fed974bdb3d32a0d6dde12a4398ee430dde49d6cbbe1e206e9d4452f6c168aea5805bc8fcf2e0883046350e9b3d8b3f7
 DIST boogie.houdini.3.2.5.nupkg 54145 BLAKE2B a89c11efd001ee4a052bb2174f1aa0cd11c0c681f191a4d6e4780ea098f02a3394939e1f7e55b6caed1f62098046450ed88d8357aa432c68f584f0c863edfee3 SHA512 c179a606ce3f49b2ca491e4ebffb6ed8a001eb551a5e393929f9d235cbe2dc01409daf16b544c412fcf93b31b7e1fd3e90df512f3a9bd7e290649becb3aa25c8
+DIST boogie.houdini.3.3.3.nupkg 54194 BLAKE2B 2b5439c130a38d30882bc93e07d5b15c0397cd62576ecea73820feab2ab28aeac8f0e55f8d9a4c89508d29b3cbf8f451143a917e0fb9958d230e5f9051252724 SHA512 108b188cf04084940101472831b3226ddf4a8b406035b2111876c0531ed9ffd81f237d79b1a09ffb8e2a95cc75f1d7991730014882476d157daf6b80000e93a3
 DIST boogie.model.3.2.3.nupkg 28314 BLAKE2B bd5c01968ec6f021646c5ea987d238d76d0303ca59045436614e9564586a698b489997f9d36722763d47b12413bffe60674bd45d539a48f80c381ac191b14dd6 SHA512 0df754580b51b5bdc4a26b8b55f17cdabf224e8db37427e212a896c3f4f05478627428224302ad222fecbcd1b75a7875ce32359649ad571996e78519829fee13
 DIST boogie.model.3.2.5.nupkg 28312 BLAKE2B deafc900a7a084123816addd81ea4a42aa9e9ae775ddacbfec3b0791e892c3d82680d187b51fb07aa4f6d82d4806db9ea7d6f22e5c3d5f9363d7c9742784b183 SHA512 eba4d84bdd7cf6238f047af2e18a562b6191e4a827853a9ed0da66773c49cbf1bc4f6aacc8b339f8cf6509afc4863e1977f4b338c778ebdd6d4efb6a2968ce52
+DIST boogie.model.3.3.3.nupkg 28299 BLAKE2B a3ba53316cf4b931822458d23a514bf1cee00ed1b486472741e1b0750558e9c974f63d3da777491a3f7dbc724976d370dfed9153482976908008c0f286d02098 SHA512 e9763bcaa321d5ca87058e904b253855be4f856e34ef4940a19db056d9f4679e05494d53fd93255baebc807305d75e17539c90bdb28bef64a7ab9b8705d688be
 DIST boogie.provers.leanauto.3.2.3.nupkg 30083 BLAKE2B 13cdcfc94a6576eb0bf184f669c0a166e75893a626284872ed029c37a687ac6a585d62db2e239a63fd957738d9cbbab6d9d71baacabc8b9c4c6ead60c97bd9c9 SHA512 39b7edbc94d374dee9ba3aadbe09bc7cb7671271668abdaf8821a6299b58fae8cf4bc07c33b917a7f650abdbcf313d98af43dc6a432f0edeb354cdeacd27fa35
 DIST boogie.provers.leanauto.3.2.5.nupkg 30316 BLAKE2B d38b21cc6d6f41f35cce0b6991a78ec263cfbdac94a50943ed9251c344c64830a0e70ee51f7d96807facd360c9486a74c9f1edb6c78506d0bad1fc8755d5e15c SHA512 50f5da6efae9c585cd93a5b2b9d09709860e2700951adbf88ebd268000e30c7337cc59a5178731f56ff946f7b9b4a8b445becb52169cdc010a414aca29e1a017
+DIST boogie.provers.leanauto.3.3.3.nupkg 30300 BLAKE2B 5e5b047330806d524c3fb29bdbefd1fefcc29b4213bb120cd5364a435addcde7477750993b914db832509f3e379c7e55e0da7e661a5b9e808d902337f11a35ae SHA512 ac1388e0ecbaadbc7409c8146efa6256b53489b09100037f49876382a6920187a9a952416b8e1f9fc77c097049e19454c3c34fda248c857e6aaee28cc1a21adb
 DIST boogie.provers.smtlib.3.2.3.nupkg 71925 BLAKE2B cedaa456e389c50543a18377243217ecb75a92c6800bad359cbd83d5da1ab216c4becee5bc4b55219fe6798ee8bd57057fc340c84b97ef4b99938f86574e88f6 SHA512 1c23cdeee2b4a4a47ce2b4e80bc1fefd1d42f3798582bf8179778b461d63614474cbca9f46e2ddc82990a4d25f134dcc25b738075f76d03f08bf048e217ce030
 DIST boogie.provers.smtlib.3.2.5.nupkg 71922 BLAKE2B 5098107dd62e4cef2a346d56a84fa8710116e103d392d39775fa03dc512ea6154d7c52f9e85adfe5c85c0042e28ddfc1727ac64844d5aa72d722f0e97b7a484f SHA512 a51087f2f40f40d36b25dce717a18f8841d8d669f947274f6b78bab3d03315a578dcad0da17733e872797876b04c446372e259e16c034f98cf5ab25daa04e0c3
+DIST boogie.provers.smtlib.3.3.3.nupkg 72072 BLAKE2B 9fa7b59423f20810bd0db84a7f756066ce89a820ac44b46a050a0b24c48db302a7ed7fc5e50a60d2d122d1fd52efd25f8b96de38cefc9785dd2174a4e31225a6 SHA512 381b8e7560afdb33cfea2f6fcc14d4be87420d4c879d9bf9aba763aba3f1e9756872ff35699b68178dd79597d0bb88dc8090aed2497c89cb4919736196a46427
 DIST boogie.vcexpr.3.2.3.nupkg 75389 BLAKE2B 01f0cb6081152993a2da928045524b2092a509109caf3ba3b3e76a9dca391a402e962c227aa4c93c8a368fe4502311874be3f545a5cbec08e522091c8a408393 SHA512 89cb65dc0459e9017923febf2c09bc8a93f7fd6480cb2010f4db84bbe3c745134a50df6f1b4f486619d3b336a59c76bd2455f61774176a484f41ed6a7731342d
 DIST boogie.vcexpr.3.2.5.nupkg 75407 BLAKE2B 07634d52cf007ae1343365875c5a95a397bf6fd7e5af5e6d3b23662ed619a3ef565720049a77b72aefb8ba2ed5015d7d2266db899ccff2bb687bc323d77d474b SHA512 8c3f9e4126ad3c5099f53ffa23feb1ec1f4a8fea718be320414a86c6423d792e56d4dd623645715423660f2c61f2274e3490854fc6299483f99f669ecddf6592
+DIST boogie.vcexpr.3.3.3.nupkg 75396 BLAKE2B f2a13f3231dbb981fe96093dc31a7b278a3e453ade2daad5752daa0597d0469e57b89570f486ddd63b809c0b3f5b74569ad0713f2a2f5edac692afc665f8f516 SHA512 543002f8fa76734b0ab207a22c1ac0d5a0d1eab3532e9213de331526ed39b8dacf18c22756eeb546bc2756b877df94426ac3d9216b011468c0718823f6e379d2
 DIST boogie.vcgeneration.3.2.3.nupkg 95225 BLAKE2B a2325e9f05240140c4ae8a369281b5482b9f16d80b499d8a2c7552c5f87a27c3e0cb5afd012d0499205bdb9e2dc916a513c38a872d17198bd12a36c8e40bd253 SHA512 a4eccf1dc4bf173a441858747f6b6ee0accfc6bd8c46efd97f8e6bc896fa648db6eda896b17031436cf37e3abbd22930839f0ff48d540e43eeddc46a0c496f49
 DIST boogie.vcgeneration.3.2.5.nupkg 96524 BLAKE2B 6f1017d1ed7b87a36ad1e48d2ac4c1f950689e0d32d3ebea05fd58d0b3f41154289f85d70c9a8f4e713a9883924a420a6f760ceffc2fb7fb9a5be80146263fbe SHA512 800e4d2724abb01683fcb6866c68c02036c52e6af168faa1e3d30416c841bc5e2e5536843d0c6429fcb31eb4fc0b6c0c02ddf6adf67e8ca22438a20de597d868
+DIST boogie.vcgeneration.3.3.3.nupkg 96878 BLAKE2B 188e158667e931b0c6e861e675385edc3dc4b1e73f10a2b89001cbcc4f2b79857dbdc788f4090e70f24246d9341a7a95826e2512cab21d60a2f69d178b0de784 SHA512 52ed2dc265f9ad7e06106cc10bacb13bfe39f89b63d21c51c6955cb657f0431a84de18a0538dfb5f2cb4353ba8371cf7c2e5956ede74f2d29c800706c5c17544
 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.8.0.tar.gz 6615281 BLAKE2B d891a1955554b194e7af231eff9368549bd2686b43dc1aca8034df4502b7b57297a8384db990ca3268bf992ce2ea562d02d936617b0788a58705d2b0cd91aa98 SHA512 8194f2544b411e00874b174ae4036d6ff21e516e342b3ddd9bc00e70a8140037e5a35f10ef797336b1d4f471ea1596829f0d5446d6a93e436690753dc9b19a31
 DIST dafny-4.8.1.tar.gz 6693520 BLAKE2B 4cceaba7aec5809c6f714bc5f79fd92656ec0c30e9188aecb5d153575ab06a244fbc248f91ae64e2e1e9ea15914ebc408ebf2ce197edeac8e021770499d3779f SHA512 cfbeb9d36ee9f63c703048fb8497a54df040d96a3e9d5ee208bb2f6a0795416e49b34ec08052f568b7c50d0a892dc6139c01a2310adbd63d347ddec61c79b56b
+DIST dafny-4.9.0.tar.gz 6733045 BLAKE2B a13eb0716eb6449c8145b25261d97539b04a6310ba24f3dba30938adc46da99b52016e44683bd7521a66cb11e03b92972dee3da6377bc13c6f519f44a91d6c81 SHA512 3d7493467db5006df02fb912d562a7109b225e7eb33e36b02fcb4ddca8cb4353464f668d578017226a22ffed7dac10424dc8fbd73ee13c8108e3bde219562884
 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
@@ -101,7 +115,9 @@ DIST microsoft.netcore.platforms.3.1.0.nupkg 29544 BLAKE2B 2739d62e92e61677964f9
 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.1.0.3.nupkg 20961 BLAKE2B 8632244fc71708fbb2a56331c8642a12782baeebda676b1b8d3ada50788e0725a7572cf0ed1c296c4cad3fb8bdd669871c90f963b9c8da6eff796fd30ba768e2 SHA512 e3b8317b290696a380a32abdd9e75e71ddae68049769beb895024c34089f41262aeddf53e30984330b1293f013e34d854a83223ae1e2afe417186795da8dc148
 DIST microsoft.netframework.referenceassemblies.net452.1.0.2.nupkg 19845441 BLAKE2B c2be1acfd4207984ba33a5ed468fea39299d61d6af99ef9cfc7df16096c0ecfb6133a3c970ffc150f79566710a589c5a387a5d2da8d5ce25f23173cfcfcc7661 SHA512 f4b099aa012c3d117c58dafcaa3edfc273ad7d5acf30c84d213eb15ae101559e7da3f1810285909153e85d73ac58dfedc34e6730c264cb0ae013e19a1213d691
+DIST microsoft.netframework.referenceassemblies.net452.1.0.3.nupkg 19845441 BLAKE2B a43644d3cba19eadb7e4dce9daa0e84b4c646e9399f5ee3680f44f23487f18fdb8d4748300f0837aee7d023aaa4779b5086c4cde6073ca5f489af63146473e3d SHA512 125b35cb0b1b2c3fd7a44810595d3232900e1e4d0b79ccf88d698e78bc33192149dca15707ee7bc0a8d7e2b109c6a25ff7b08816752670efa9bc8cfc2df4d7bf
 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

diff --git a/dev-lang/dafny/dafny-4.9.0.ebuild b/dev-lang/dafny/dafny-4.9.0.ebuild
new file mode 100644
index 000000000000..968c455920bb
--- /dev/null
+++ b/dev-lang/dafny/dafny-4.9.0.ebuild
@@ -0,0 +1,643 @@
+# Copyright 1999-2024 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+PYTHON_COMPAT=( python3_{11..13} )
+
+DOTNET_PKG_COMPAT="6.0"
+NUGETS="
+boogie.abstractinterpretation@3.3.3
+boogie.basetypes@3.3.3
+boogie.codecontractsextender@3.3.3
+boogie.concurrency@3.3.3
+boogie.core@3.3.3
+boogie.executionengine@3.3.3
+boogie.graph@3.3.3
+boogie.houdini@3.3.3
+boogie.model@3.3.3
+boogie.provers.leanauto@3.3.3
+boogie.provers.smtlib@3.3.3
+boogie.vcexpr@3.3.3
+boogie.vcgeneration@3.3.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.net452@1.0.3
+microsoft.netframework.referenceassemblies@1.0.2
+microsoft.netframework.referenceassemblies@1.0.3
+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-lang/boogie-3.3.3
+		dev-go/go-tools
+		dev-lang/go
+		dev-python/OutputCheck
+		dev-python/lit
+		dev-python/psutil
+		net-libs/nodejs[npm]
+	)
+"
+
+CHECKREQS_DISK_BUILD="2G"
+DOTNET_PKG_PROJECTS=( Source/Dafny/Dafny.csproj )
+
+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() {
+	# Unpack manually to skip additional archives, eg "bignumber.js".
+
+	nuget_link-system-nugets
+	nuget_link-nuget-archives
+
+	if [[ -n "${EGIT_REPO_URI}" ]] ; then
+		git-r3_src_unpack
+	else
+		unpack "${P}.tar.gz"
+	fi
+}
+
+src_prepare() {
+	# Using "for-each-compiler" will fail because of Cargo requiring network access.
+	while read -r test_file ; do
+		if grep "// RUN: %testDafnyForEachCompiler" "${test_file}" >/dev/null ; then
+			rm "${test_file}" || die "failed to remove test ${bad_test}"
+		fi
+	done < <(find "${TEST_S}" -type f -name "*.dfy")
+
+	# Remove bad tests (recursive).
+	local -a bad_tests=(
+		# Unsupported test build (and those that need network access):
+		comp/rust
+
+		# Following tests fail:
+		VSComp2010/Problem2-Invert.dfy
+		ast/function.dfy
+		auditor/TestAuditor.dfy
+		benchmarks/sequence-race/SequenceRace.dfy
+		blogposts/TestGenerationNoInliningEnumerativeDefinitions.dfy
+		blogposts/TestGenerationWithInliningQuantifiedDefinitions.dfy
+		c++/extern.dfy
+		c++/functions.dfy
+		c++/tuple.dfy
+		cli/measure-complexity.dfy
+		cli/projectFile/projectFile.dfy
+		cli/runArgument.dfy
+		comp/CoverageReport.dfy
+		comp/Libraries/consumer.dfy
+		concurrency/06-ThreadOwnership.dfy
+		concurrency/09-CounterNoStateMachine.dfy
+		dafny0/CoinductiveProofs.dfy
+		dafny0/Fuel.legacy.dfy
+		dafny0/Stdin.dfy
+		dafny0/SubsetTypes.dfy
+		dafny0/TypeConversions.dfy
+		dafny1/MoreInduction.dfy
+		dafny1/SchorrWaite.dfy
+		dafny4/Lucas-up.legacy.dfy
+		dafny4/Primes.dfy
+		doofiles/allowWarningsDoo.dfy
+		doofiles/semanticOptions.dfy
+		doofiles/standardLibraryOptionMismatch.dfy
+		examples/Simple_compiler/Compiler.dfy
+		exports/ExportRefinement.dfy
+		exports/IncludeSkipTranslate.dfy
+		git-issues/git-issue-2026.dfy
+		git-issues/git-issue-2299.dfy
+		git-issues/git-issue-2301.dfy
+		git-issues/git-issue-3855.dfy
+		git-issues/git-issue-505.dfy
+		git-issues/git-issue-MainE.dfy
+		gomodule/multimodule/DerivedModule.dfy
+		gomodule/publishedruntime/helloworld.dfy
+		gomodule/singlemodule/dafnysource/helloworld.dfy
+		lambdas/MatrixAssoc.dfy
+		metatests/InconsistentCompilerBehavior.dfy
+		metatests/TestBeyondVerifierExpect.dfy
+		printing/ModulePrint.dfy
+		pythonmodule/multimodule/DerivedModule.dfy
+		pythonmodule/nestedmodule/SomeTestModule.dfy
+		pythonmodule/singlemodule/dafnysource/helloworld.dfy
+		separate-verification/assumptions.dfy
+		server/counterexample_none.transcript
+		triggers/emptyTrigger.dfy
+		unicodecharsFalse/DafnyTests/RunAllTestsOption.dfy
+		unicodecharsFalse/comp/Print.dfy
+		verification/isolate-assertions.dfy
+		verification/outOfResourceAndIsolateAssertions.dfy
+		verification/progress.dfy
+		vstte2012/Combinators.dfy
+		wishlist/exists-b-exists-not-b.dfy
+		wishlist/sequences-s0-in-s.dfy
+	)
+	local bad_test=""
+	for bad_test in "${bad_tests[@]}" ; do
+		if [[ -e "${TEST_S}/${bad_test}" ]] ; then
+			rm -r "${TEST_S}/${bad_test}" || eerror "failed to remove test ${bad_test}"
+		else
+			ewarn "Test file ${bad_test} does not exist"
+		fi
+	done
+
+	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")
+	edob jar cvf "DafnyRuntime-${PV}.jar" dafny/*
+
+	cp "DafnyRuntime-${PV}.jar" "${dafny_runtime_java}/build/libs/" || die
+	popd || die
+
+	# Build main dotnet package.
+	dotnet-pkg_src_compile
+
+	# Build "TestDafny" without saving artifacts.
+	if use test ; then
+		local -a build_test_opts=(
+			--configuration Debug
+			--no-self-contained
+			-maxCpuCount:$(makeopts_jobs)
+		)
+		edotnet build "${build_test_opts[@]}" "${S}/Source/TestDafny/TestDafny.csproj"
+	fi
+}
+
+src_test() {
+	# Dafny GOLang transpiler tests need "goimports" from "/usr/lib/go/bin".
+	local -x PATH="${EPREFIX}/usr/lib/go/bin:${PATH}"
+
+	einfo "Installing bignumber.js package required for tests using NodeJS."
+	local -a npm_opts=(
+		--audit false
+		--color false
+		--foreground-scripts
+		--offline
+		--progress false
+		--verbose
+	)
+	edob npm "${npm_opts[@]}" install "${DISTDIR}/bignumber.js-9.1.2.tgz"
+
+	einfo "Starting tests using the lit test tool."
+	local -a lit_opts=(
+		--order=lexical
+		--time-tests
+		--timeout 1800          # Let one test take no mere than half a hour.
+		--verbose
+		--workers="$(makeopts_jobs)"
+	)
+	edo lit "${lit_opts[@]}" "${TEST_S}"
+}
+
+src_install() {
+	dotnet-pkg-base_install
+
+	local -a dafny_exes=(
+		Dafny
+		DafnyDriver
+		DafnyLanguageServer
+		DafnyServer
+		TestDafny
+	)
+	local dafny_exe
+	for dafny_exe in "${dafny_exes[@]}" ; do
+		dotnet-pkg-base_dolauncher "/usr/share/${P}/${dafny_exe}" "${dafny_exe}"
+	done
+
+	dosym -r /usr/bin/Dafny /usr/bin/dafny
+	dosym -r /usr/bin/DafnyServer /usr/bin/dafny-server
+
+	einstalldocs
+}
+
+pkg_postinst() {
+	optfeature "Dafny GO language backend" dev-go/go-tools
+	optfeature "Dafny Rust language backend" virtual/rust
+}