commit:     2784f1947a3c1cfa6b2f3e4f7c12f3c7086b9d28
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Thu Jun 27 21:10:46 2024 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Jun 27 22:42:19 2024 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=2784f194

dev-lang/dafny: bump to 4.7.0

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

 dev-lang/dafny/Manifest           |  14 +
 dev-lang/dafny/dafny-4.7.0.ebuild | 665 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 679 insertions(+)

diff --git a/dev-lang/dafny/Manifest b/dev-lang/dafny/Manifest
index 133f085036b5..d1aec9b0a014 100644
--- a/dev-lang/dafny/Manifest
+++ b/dev-lang/dafny/Manifest
@@ -1,21 +1,35 @@
 DIST bignumber.js-9.1.2.tgz 79226 BLAKE2B 
3d2ff19d73a6fcfbcc0d03d1e9808796baae639e19973cbe0c26af4b514abc299129b8a7bc3e4e803c61af44b76f4381b1965d8fa331ea43e8a4c8fc7f98d8e7
 SHA512 
dbf98ac991fd2bce5bcce11f8570c11594c6775093b3ee481e9785428f65ba2046ee1821742f39d4f8f658085be84dd1e9bf6d663fd72a16e0e1fba6f8a7a9ba
 DIST boogie.abstractinterpretation.3.1.3.nupkg 29640 BLAKE2B 
6ebadfc92014018649ba1998f878ca8d8cda2df25d8b7f5243becd27bcafbcc166c071769adabdc99098b4fbf4aee8a6de8be9f8da43b3a3e1511dba96bbf2d1
 SHA512 
b950ceab224aca2a6d9a0202d2f79dc59f5e8f18f710933d843e8eb6dae9badadf6f78e79297f74bbe35a9d9170f2c928174c93a6edfd70e79aa282348b4be58
+DIST boogie.abstractinterpretation.3.1.6.nupkg 31060 BLAKE2B 
232350ede99fdfe5eafccfe1975d69dec478e353041cfdf85f66b9ef6080b9530c3ce3e1caf9cdadb72dc7238dc0730fe689cd97014f0ca6e7a0721ef5906e51
 SHA512 
8d1d2d9fa70e3428ae5be04f13498492e3075eef4c51162b265a30361496acf173c1d6ee8d875fc29e1b5bab58d899a351b3fa07c9321c2f30641efaa61391f5
 DIST boogie.basetypes.3.1.3.nupkg 25710 BLAKE2B 
e45663df336757dcc448f2ebe4f150948504047a1d5e4814fba81b0c08d7480aa717a42ebaa1ef9714276093a0d2755780669d0af410dda4806181c513874bf0
 SHA512 
ce3bbdf67d1332a51dbfffc21f12cde720b6583638dd7b6bc1fb68e5e6a7d1d6f0a191e795728b79adc1f113102996475c0290afb7062bd1122a17c1d6d1605f
+DIST boogie.basetypes.3.1.6.nupkg 27130 BLAKE2B 
34a2c49a31c3582011934b6fccede103858e6c117d3ad07c0bf07bf95b6899b8274184e615369ea16b5d309273402a3876147ad54cdc3076cbbf6f65603ccc67
 SHA512 
41365c6b02cf0cc333f2bba5a282f17c061cb9ffeccfaad50888f4ae40571226fbccab5ad4b4ce77d5abea6dfc20d33490006a8694f66a82d6f8fd1cc79f3f4b
 DIST boogie.codecontractsextender.3.1.3.nupkg 17458 BLAKE2B 
2005168450015740d0afd9415c47674bb55f99b2a717ad03f56e0571be1f5532a9abb0a662b3b3f785dab32914684dc0046854c4286ea9be338aa0dcad0e4618
 SHA512 
1508e11342e88ef0fe3a6f7dc758924987b6edcc30f62d0a7e43aaba09cc14b26b999eb0d59faa13e26f246e91b9c176f4c983fdeb653892cff655f40b5bd24f
+DIST boogie.codecontractsextender.3.1.6.nupkg 18878 BLAKE2B 
8b1b92b1bf916ccd5dabe99102ee1d5feea10fe4cb9aca7926bc1ab7f17e5c626e72f71f9aba33b4a8076760323f8fecc115d7f5d111437c8af0ce51ae97c413
 SHA512 
7675cf3e961ac3e323fc39fe39e1ed1a955aa2ce651302729c8d1a6a4f015315f3e5fd3cfe79888bc4b2e7b6be4a9fab5febacf7f12b814e3f980f42d99fdea4
 DIST boogie.concurrency.3.1.3.nupkg 92168 BLAKE2B 
81ff170058924043a10c83aed60ea38951bca7ff35de3d8be29fcf68fea9da2d658ba0abf36f0fa93e4c9f96b0a81f96b550396ca55e3ac204b4e21e49d112bd
 SHA512 
069c34b152ccfa9ab8903b6beda6090fcbfbad243d79dc473c01e30d19a6a5ed15528120180ad271d28b43eb520dae6e221a9256680b7e241a6bb83415988d93
+DIST boogie.concurrency.3.1.6.nupkg 92317 BLAKE2B 
174a2ed0ae2e4141e9f4a4dba6d2498bb7b56babcc25a103a4a77d8fce9b5d7d41e26df16dca3b9f1f64e503d377b9b3b41484be01d80bb820c468bf87f7601e
 SHA512 
c4a62941db25677f45dde8657d3c917a1845e51d3fde13dee40a9446ee30f5a533392b333989864439b29c8278b256b71f0d8eb7d118f1152c7ab514d29103c8
 DIST boogie.core.3.1.3.nupkg 208304 BLAKE2B 
c3affd650c0c81c61e39e5bba0e3f88684fe43169c59b60aa15ef532747ed624d3b4d2a1ebf1fef6d216bb380b535c62a48cce072bf4a3ff57feea907c48ca8c
 SHA512 
ae611fe91b8189ba55315db75be7fd927d08ae096305d099aa5b51ef692b4c5f4633c7cdcc95f9344791f7e11414e4078a8640127e2442f667594b335338eb1e
+DIST boogie.core.3.1.6.nupkg 209262 BLAKE2B 
42160fee38ba905ef76ee63e6384b6be8e248302cca8f6fc9784ae822e2d55200a1e54b38c399d616aff2adc47bf7cb34713cff0b11da36c453b47b9b901b8fd
 SHA512 
14f2680defcc7db41698b9e959fb554ea15ab1752dfc238124c535e406029dd29305f26173d7084d98cac235385bc0d8552e16bb2455e6d7ebe687e164b06c1d
 DIST boogie.executionengine.3.1.3.nupkg 85951 BLAKE2B 
4dc3e7c442d2fc8f79b8f17c5139bf28453205f7fbb22caf35cdff40ff5294e940820e44029669e4f2103ae4dda56ad34b5d3d76dc73327d8925e6c5384859af
 SHA512 
d06372aa80356ee5b07dd6cd30495246a5d900727fd7c6bba52faef25aabc191b5d89f479ba3c936a2a31a0045c8c195e9099d4c87231c14705ff00ac37b8c84
+DIST boogie.executionengine.3.1.6.nupkg 88418 BLAKE2B 
98e49c3c54af899e5e70d39c083fa62fba395aaa5a8abc04362e98bb9ab109cdc854072d0609d30da319373ac66de54e0640d29c8579ac38da91a5104ac926d5
 SHA512 
7628e192df3914da874ff774419d88a9d684ef500bb74ae0c5cb484438b02c9bf1dd73d814848aac781ca9c236518f71cad07ddb87486ad373d5caccd2bcd6c1
 DIST boogie.graph.3.1.3.nupkg 27927 BLAKE2B 
66694f02030c943892514881969c05be58d2a9cc4e4ca44a7b6115908a2e04e104350b706b19346e5ea7d659101532ffba2cf0ac919157102c7832185f4cf112
 SHA512 
f50c932d6ca907f359f698c02cdf857cf21b47ec6671ec917f4ae5a03db5b02cfdf3bc075b4ad840ab31c44db343aac2fe0d623d555f17e3ce2d9cf0f5efe9e3
+DIST boogie.graph.3.1.6.nupkg 29347 BLAKE2B 
f96ff7e145cd7b5897a984b5d0109783e7e18e74e0a8185816cd80bb4fc53537a16b14f9e0ec98ce90db9f26eed32c8b23420cbf8343b21837e0aa369f6d2354
 SHA512 
4f385c6941637d456d921ea4247cbdf4eb8e5d470fbf1f1f35972358851fe45f7f925c3fd2f436468e133531174d71aefeb178de30c527fd56388ae89b212056
 DIST boogie.houdini.3.1.3.nupkg 52727 BLAKE2B 
4a37e98bc0ab9bc8956e81df2541bf1bcfb50c32258b94818a5c8cafbcc74c76d4cfc5432a2e1ee94db5fc503dddd020123cc4f5f4a47c6b3bc8743b47784a04
 SHA512 
0f83ea50aa6f453d741cc7ff28a00ab9e9205a90caecaf7ccbd49d5b9217ec3bf9f5e1a7e9cce83314f48f25ee32c682c9509d00ed7bdcee602827f78712ce31
+DIST boogie.houdini.3.1.6.nupkg 54144 BLAKE2B 
4b1571a49818ef03d30a87eb6326c33ec7d693fe31eed4ab4f636dd50ba6015b5594cdb89024943f9beb1322edb4a3813629421609417d6308513e5a0c7a71ff
 SHA512 
608a293d03927b7fc5d3a0cdd364bcbffa7b11bd8443f13afff58aa8dfb4cf0c0c8615786c50e16560df5ee968b41477bf27033d0f48bb518d19a2cecc0c0a19
 DIST boogie.model.3.1.3.nupkg 26902 BLAKE2B 
f384227782a32efa4083412a0820343e301337df11bcf4dc4611ce9022a63387b66a350d921dab484230d29f6a33006e1e56ebbd1818e8d5a4b0b34e61912211
 SHA512 
f6e52696ded95d9be9ec4046917c171cddda7429f63d2a0f188b960950bd9684285ce6eb21d1181b4f582b2d400117bf810a8b5a11a654f43a40c22fef4abbf4
+DIST boogie.model.3.1.6.nupkg 28325 BLAKE2B 
11a0a9cf0931e246fc5ac7b2f7598033dff11e92cc7f505616e3af95260c08b65e9ab9bdcf794231240da4a341ce5c88cdfd9ed84b54641c83e0344fd454de0e
 SHA512 
d638cf7c495d26e1edb6ac82d83a6dfa756121098a538ece663095c08ec9f623c57bcf7b34c492889a85e28e928d0f77cc55fc49aa04c9da21ab32220bc15b39
+DIST boogie.provers.leanauto.3.1.6.nupkg 30068 BLAKE2B 
a8a751bc5df775c0ae5b6254734120b2a094c6713618f8854ef785fc02f0774fe6727b930df945b63282e45dbdc2e472fd5508281b9ed5304ad1ac4c1b1bd13a
 SHA512 
37da67c1e202f4b9aac420171d83fd96add2ecce51f69f83901a57151420fc32bdb98e18f31b98e140d881bc1f10cfa19ffcb2ca3c57c0db79a38af42febb7b7
 DIST boogie.provers.smtlib.3.1.3.nupkg 70581 BLAKE2B 
ade8aaf77a42dc7aa8ab7a7dcf2eacd00db612b032a7e62d2ddb5f96431e43ac16df282e55fe2cc46b104b721bb1183421b98a22e8823746c6f655c7f7789fc6
 SHA512 
50368434be8277c5dd84edce72fcb1ba107737cedcac0f6ff7cbad32b44bc749912b576e4c1076a840239cf5f84d93354fc8a5fe649121f5ff339316cd53c1c4
+DIST boogie.provers.smtlib.3.1.6.nupkg 71966 BLAKE2B 
7879b4893bf8f24486648f73aa21f9a5046e04a1ab765ecccc5ae66a5000170eb733949567a52f3c3a46246739976290d6180936a30d6fa4a83966957115d556
 SHA512 
2edcb1ed93c6d6a4f457785a1cced9d655b8afcfec04558fc189ae9a08ea64036bfdea646366c06ed9eeb5ed34d1ba542d4f88ae716a5fc766f10d6578e51d7c
 DIST boogie.vcexpr.3.1.3.nupkg 74142 BLAKE2B 
d523aecb82111a712fe619a69c159213ee4bef8182b1dd5708ff2b84ecd7690bceed5eaa825f8735c373ae7d3cf5ba4385e552f4a332d68fa5740cf862992bce
 SHA512 
540e15a2830b739921e72165a39633bbc5b0a820463d79d7a2a915d2d902d242d9221e12026b6c8f6796d2309f5bff672dae50ff9d27834f2660fb433ce5809b
+DIST boogie.vcexpr.3.1.6.nupkg 75557 BLAKE2B 
8fce1d8b05a18bc55c80259e9a856df7c4b0631eca4f19b050bc13405773e4b9f7072e32dba67378eb63e137d1dcd4988b868b57ae2f41c9735ee6dbd9bba274
 SHA512 
b9bc0d6148bca1010161442ec800a798bd5a5c6748e9b3e41cd8608ecf7020d97c2d111317764dc404f547ce5ed974a7945f8d2e9d948259b0a0f6fb1bf2e327
 DIST boogie.vcgeneration.3.1.3.nupkg 90517 BLAKE2B 
d5f0271491a37f7ba806c2a46894c474b0c65d5bc66a659241e9ebffbf63c77a75a3533a615957ced4af1ee0363a34fd2c6803beca59e1fe656a1ba29c5fb309
 SHA512 
e402de9912b9d788520ef615fd80b8dba2eca9938f8321fb9e3f53bf158baedfd4c69f3aa4eaa3fe8f685d3ed9556982001117014279f9440605bac368b521c5
+DIST boogie.vcgeneration.3.1.6.nupkg 91911 BLAKE2B 
405a1995a6438953ab44d912dc633024fb564eb95d258e0d360a13b6b29075eb283da95f02f157fca740b86d499e25c43f98af96664b837cdf13ea496e53b813
 SHA512 
be76b5c721c42a301bd553b205868328b855e23463e2c728d6780919b2bc09481e3fa5c5abdcd7673b3a9ce48f1675da9fbc120b8bfc978dbccb5b048ea7c55a
 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.6.0.tar.gz 6373177 BLAKE2B 
9348a9b170dd694885efe4682f05abe60240e6f7df7bde7bb53e8955c1c75a332ca6e7d6d6f38eb1aa9a83a9a5dfccea13b7683e99873c1fce12181d47679548
 SHA512 
abac500a27a811b434d32036ff7d877dd337a0a5917a07a7ac1fceffb1dd5d493bd07b7d518875243674b7919862a25f628fe62052983a8ff8f1450669c49b69
+DIST dafny-4.7.0.tar.gz 6538682 BLAKE2B 
92597a70055ab599bdc8495de9e00a441112098b990372d40515cafc191fff0b63e835aad0a94fdef363436ea06e012dfdfca76ade5b7271386a0293a9471729
 SHA512 
4fca7fab490df1a075c70f4c2b3f62d77c7194224b34de954e5195477b08f30d4ec9562defa9dc3756039b217bf758f86d212f4c71a644ac43069d829d5b2eb2
 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

diff --git a/dev-lang/dafny/dafny-4.7.0.ebuild 
b/dev-lang/dafny/dafny-4.7.0.ebuild
new file mode 100644
index 000000000000..edd00aee8e1e
--- /dev/null
+++ b/dev-lang/dafny/dafny-4.7.0.ebuild
@@ -0,0 +1,665 @@
+# Copyright 1999-2024 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+PYTHON_COMPAT=( python3_{10..13} )
+
+DOTNET_PKG_COMPAT=6.0
+NUGETS="
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
+runtime.debian.8-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.fedora.23-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.fedora.24-x64.runtime.native.system.security.cryptography.openssl@4.3.0
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
+runtime.opensuse.13.2-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.opensuse.42.1-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.osx.10.10-x64.runtime.native.system.security.cryptography.apple@4.3.0
+runtime.osx.10.10-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.rhel.7-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.ubuntu.14.04-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.ubuntu.16.04-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.ubuntu.16.10-x64.runtime.native.system.security.cryptography.openssl@4.3.0
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]
+"
+
+inherit check-reqs dotnet-pkg edo java-pkg-2 multiprocessing python-any-r1 
optfeature
+
+DESCRIPTION="Dafny is a verification-aware programming language"
+HOMEPAGE="https://dafny.org/
+       https://github.com/dafny-lang/dafny/";
+
+if [[ "${PV}" == *9999* ]] ; then
+       inherit git-r3
+
+       EGIT_REPO_URI="https://github.com/dafny-lang/${PN}.git";
+else
+       SRC_URI="https://github.com/dafny-lang/${PN}/archive/v${PV}.tar.gz
+               -> ${P}.tar.gz"
+
+       KEYWORDS="~amd64"
+fi
+
+SRC_URI+="
+       ${NUGET_URIS}
+       test? ( 
https://registry.npmjs.org/bignumber.js/-/bignumber.js-9.1.2.tgz )
+"
+
+LICENSE="MIT"
+SLOT="0"
+IUSE="test"
+RESTRICT="!test? ( test )"
+
+RDEPEND="
+       !dev-lang/dafny-bin
+       >=virtual/jre-1.8:*
+       sci-mathematics/z3
+"
+DEPEND="
+       >=virtual/jdk-1.8:*
+"
+BDEPEND="
+       ${RDEPEND}
+       dev-dotnet/coco
+       test? (
+               ${PYTHON_DEPS}
+               >=dev-lang/boogie-3.1.6
+               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=( "${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() {
+       # 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
+               c++/extern.dfy
+               c++/functions.dfy
+               c++/tuple.dfy
+               cli/projectFile/projectFile.dfy
+               cli/runArgument.dfy
+               comp/CoverageReport.dfy
+               comp/Libraries/consumer.dfy
+               concurrency/06-ThreadOwnership.dfy
+               dafny0/Fuel.legacy.dfy
+               dafny0/Stdin.dfy
+               dafny1/MoreInduction.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
+               gomodule/multimodule/DerivedModule.dfy
+               gomodule/singlemodule/dafnysource/helloworld.dfy
+               lambdas/MatrixAssoc.dfy
+               metatests/InconsistentCompilerBehavior.dfy
+               metatests/TestBeyondVerifierExpect.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
+
+               # 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/ExternCtors.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
+               comp/rust/strings.dfy
+               concurrency/07-CounterThreadOwnership.dfy
+               concurrency/08-CounterNoTermination.dfy
+               concurrency/09-CounterNoStateMachine.dfy
+               concurrency/10-SequenceInvariant.dfy
+               concurrency/12-MutexLifetime-short.dfy
+               dafny0/ModuleInsertion.dfy
+               dafny0/NoTypeArgs.dfy
+               dafny0/RlimitMultiplier.dfy
+               dafny1/ExtensibleArray.dfy
+               dafny1/ExtensibleArrayAuto.dfy
+               dafny1/SchorrWaite.dfy
+               dafny2/SnapshotableTrees.dfy
+               dafny4/git-issue250.dfy
+               git-issues/git-issue-Main4.dfy
+               git-issues/git-issue-MainE.dfy
+               separate-verification/app.dfy
+               unicodecharsFalse/comp/CompileWithArguments.dfy
+               unicodecharsFalse/expectations/Expect.dfy
+               unicodecharsFalse/expectations/ExpectAndExceptions.dfy
+               unicodecharsFalse/expectations/ExpectWithNonStringMessage.dfy
+               verification/filter.dfy
+       )
+       local bad_test
+       for bad_test in "${bad_tests[@]}" ; do
+               if [[ -e "${TEST_S}/${bad_test}" ]] ; then
+                       rm -r "${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-4.6.0.jar" dafny/*
+
+       cp "DafnyRuntime-4.6.0.jar" "${dafny_runtime_java}/build/libs/" || die
+       popd || die
+
+       # Build main dotnet package.
+       dotnet-pkg_src_compile
+
+       if use test ; then
+               # Build "TestDafny" without saving artifacts.
+               edotnet build                                                   
                        \
+                               --configuration Debug                           
                \
+                               --no-self-contained                             
                        \
+                               -maxCpuCount:$(makeopts_jobs)                   
        \
+                               "${S}/Source/TestDafny/TestDafny.csproj"
+       fi
+}
+
+src_test() {
+       # Dafny GOLang transpiler tests need "goimports" from "/usr/lib/go/bin".
+       local -x PATH="${EPREFIX}/usr/lib/go/bin:${PATH}"
+
+       einfo "Installing bignumber.js package required for tests using NodeJS."
+       local -a npm_opts=(
+               --audit false
+               --color false
+               --foreground-scripts
+               --offline
+               --progress false
+               --verbose
+       )
+       edob npm "${npm_opts[@]}" install "${DISTDIR}/bignumber.js-9.1.2.tgz"
+
+       einfo "Starting tests using the lit test tool."
+       local -a lit_opts=(
+               --order=lexical
+               --time-tests
+               --timeout 1800          # Let one test take no mere than half a 
hour.
+               --verbose
+               --workers="$(makeopts_jobs)"
+       )
+       edo lit "${lit_opts[@]}" "${TEST_S}"
+}
+
+src_install() {
+       dotnet-pkg-base_install
+
+       local -a dafny_exes=(
+               Dafny
+               DafnyDriver
+               DafnyLanguageServer
+               DafnyServer
+               TestDafny
+       )
+       local dafny_exe
+       for dafny_exe in "${dafny_exes[@]}" ; do
+               dotnet-pkg-base_dolauncher "/usr/share/${P}/${dafny_exe}" 
"${dafny_exe}"
+       done
+
+       dosym -r /usr/bin/Dafny /usr/bin/dafny
+       dosym -r /usr/bin/DafnyServer /usr/bin/dafny-server
+
+       einstalldocs
+}
+
+pkg_postinst() {
+       optfeature "Dafny GO language backend" dev-go/go-tools
+       optfeature "Dafny Rust language backend" virtual/rust
+}

Reply via email to