summaryrefslogtreecommitdiff
path: root/sci-mathematics
diff options
context:
space:
mode:
Diffstat (limited to 'sci-mathematics')
-rw-r--r--sci-mathematics/Manifest.gzbin15842 -> 15850 bytes
-rw-r--r--sci-mathematics/giac/Manifest2
-rw-r--r--sci-mathematics/giac/giac-1.7.0.45.ebuild165
-rw-r--r--sci-mathematics/gimps/Manifest3
-rw-r--r--sci-mathematics/gimps/gimps-30.7.9.ebuild5
-rw-r--r--sci-mathematics/lean/Manifest2
-rw-r--r--sci-mathematics/lean/lean-3.37.0.ebuild75
-rw-r--r--sci-mathematics/spin/Manifest3
-rw-r--r--sci-mathematics/spin/files/spin-6.5.2-nesting_limit.patch55
-rw-r--r--sci-mathematics/spin/spin-6.5.2-r1.ebuild (renamed from sci-mathematics/spin/spin-6.5.2.ebuild)3
-rw-r--r--sci-mathematics/why3/Manifest2
-rw-r--r--sci-mathematics/why3/why3-1.4.0-r2.ebuild (renamed from sci-mathematics/why3/why3-1.4.0-r1.ebuild)5
-rw-r--r--sci-mathematics/z3/Manifest4
-rw-r--r--sci-mathematics/z3/z3-4.8.11b.ebuild103
-rw-r--r--sci-mathematics/z3/z3-4.8.13.ebuild4
15 files changed, 316 insertions, 115 deletions
diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index 6a9d8d754519..349fd019ec7f 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
Binary files differ
diff --git a/sci-mathematics/giac/Manifest b/sci-mathematics/giac/Manifest
index b3bd352c3ce9..3aa90b149f78 100644
--- a/sci-mathematics/giac/Manifest
+++ b/sci-mathematics/giac/Manifest
@@ -2,5 +2,7 @@ AUX giac-1.6.0-pari-2.11.patch 783 BLAKE2B f173015006fef4a9f8176965f923664f11b0b
AUX giac-1.7.0.1-gsl_lapack.patch 2912 BLAKE2B b0f9f05126316b9b76d5f1a5ad737cc88ecbc71dc450ef714f6da323128d9c945ada9d658c73647987f84638498aa4d3bbef49062424ab63b53c76defc127902 SHA512 14bfcb04e5a23933cfa4635789bf02f6d6e6a528c167504678b3d2ecb38f135d0c05583712005fe53afd7696cc9ebee5dc3ab90cac056d75bd43be786075b011
AUX giac-1.7.0.13-xcas-desktop.patch 890 BLAKE2B 31e33a52fdcb70c610edf21f046d112df3702e1d4f635cd4956bbe17d928839c9a0a87cb5ba5d6aeff94213b482ce22bd497d1d258aaa8abd6d8fc0116031f15 SHA512 269c733edc899051fc3de23021c322a3099499dfeb559ab1cada0964258a91a9735e620b480560226e5a3b492f2f5654062ee9c2c5479ae9789b012e7a5055ca
DIST giac_1.7.0-13.tar.gz 86447065 BLAKE2B 4d91e83608f7ec376d133c2784ffce99447a9dd78b5c8582b81a0aae0b8ac59eec4db3ee4a8bcb39202c777c300178a181f2dc2ac74ab445ddba2f3efa0ecb1b SHA512 99fff7ce5117fd8c106601ead03679805d529fe12d5372cdd4ae54824aa6fdcbdaaa1a62ea1153391a1a65af8970e38fca7d95ca9983755ff06053f1d8b6d65a
+DIST giac_1.7.0-45.tar.gz 96780194 BLAKE2B c43b0f89ad664b419db5d98541f23d3259a32b462d71f3a4fe06ea2ac3de0dd71d903308cd8e241758d809d0755a2f070bae03434a75abc94f17b1d8cbda03a2 SHA512 47fa019fee526d584f5dbc67adb4326e2680649ad942a2140d033ecd66957ba7a21441f02a3ba55d009bbd6756da239fcee99cab2a361993aae4df6e9f79a1a7
EBUILD giac-1.7.0.13-r1.ebuild 4257 BLAKE2B af1277a69e3a27cf215e870fe6dab127d4ac7edc0fd1e8905498e5b745bc92133d7f4f725fc096c4a83bd649fd5ba3731d16c86688f3bee1a9f8e4b7b1bd2aaf SHA512 351d891b219e15c24cae84e5ef1e1063a702c36d0fc6a6f9955f0eb3b1d16cb179e0fdbfd39bd6f820929fbe9d259a3ab91e71976cdb1a270cedbb66ec6fff83
+EBUILD giac-1.7.0.45.ebuild 4209 BLAKE2B a5229d4b3c5e1bf9c04b99e555c70ee57eef601d2ccca939a148435c4780be251c0e8e7dd5abf83127f5371e20efbd14e10ace4b3e0e47d9dec38d317f51d28b SHA512 be2c595f3ca7ffb7904d20029848a1654179f5a1da4662e51be848f151871c71c9e7e153f9d7e9e19bff037697e7d6c522f4eae6b8bc5fa34d8616e000672890
MISC metadata.xml 1315 BLAKE2B a461d359b33617422f5863466bdbec9ddf56db03467b992c887bce9967d434913489602fd684edc893303078f89cf94d01b44cfdc0ccff33db9b42c5e686cfa8 SHA512 eaeb480010c9dbdfd75516e45e97e3226d2b2812c44e217b318c5a1d86dc40820bac0de69686d7b502775b14a6f1ed3bc11d2372b891c46a37080b4e84da9a1c
diff --git a/sci-mathematics/giac/giac-1.7.0.45.ebuild b/sci-mathematics/giac/giac-1.7.0.45.ebuild
new file mode 100644
index 000000000000..70e638c38502
--- /dev/null
+++ b/sci-mathematics/giac/giac-1.7.0.45.ebuild
@@ -0,0 +1,165 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+inherit autotools flag-o-matic xdg-utils
+
+FETCH_P="${PN}_"$(ver_rs 3 '-')
+MY_PV=$(ver_cut 1-3)
+DESCRIPTION="A free C++ Computer Algebra System library and its interfaces"
+HOMEPAGE="https://www-fourier.ujf-grenoble.fr/~parisse/giac.html"
+SRC_URI="https://www-fourier.ujf-grenoble.fr/~parisse/debian/dists/stable/main/source/${FETCH_P}.tar.gz"
+LICENSE="GPL-2"
+
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+LANGS="el en es pt"
+IUSE="ao doc +ecm examples gc +glpk gui static-libs test"
+for X in ${LANGS} ; do
+ IUSE="${IUSE} l10n_${X}"
+done
+
+# nauty and cliquer are automagical dependencies
+RDEPEND="dev-libs/gmp:=[cxx(+)]
+ sys-libs/readline:=
+ gui? ( x11-libs/fltk
+ media-libs/libpng:= )
+ ao? ( media-libs/libao )
+ dev-libs/mpfr:=
+ sci-libs/mpfi
+ sci-libs/gsl:=
+ sci-mathematics/pari:=[threads]
+ dev-libs/ntl:=
+ virtual/lapack
+ virtual/blas
+ net-misc/curl
+ sci-mathematics/cliquer
+ sci-mathematics/nauty
+ ecm? ( sci-mathematics/gmp-ecm )
+ glpk? ( sci-mathematics/glpk )
+ gc? ( dev-libs/boehm-gc )"
+
+DEPEND="${RDEPEND}"
+
+BDEPEND="dev-tex/hevea
+ virtual/pkgconfig
+ virtual/yacc"
+
+PATCHES=(
+ "${FILESDIR}/${PN}-1.7.0.1-gsl_lapack.patch"
+ "${FILESDIR}/${PN}-1.6.0-pari-2.11.patch"
+)
+
+REQUIRED_USE="test? ( gui )"
+
+# The mirror restriction is due to the French documentation for which
+# "Other kind of redistributions require the consent of the copyright
+# holder."
+RESTRICT="!test? ( test ) mirror"
+
+S="${WORKDIR}/${PN}-${MY_PV}"
+
+src_prepare() {
+ default
+ eautoreconf
+}
+
+src_configure() {
+ append-cxxflags -std=c++14 # bug 788283
+
+ if use gui; then
+ append-cppflags -I$(fltk-config --includedir)
+ append-lfs-flags
+
+ # Get the big-L flags from fltk's LDFLAGS.
+ append-ldflags $(fltk-config --ldflags | sed -e 's/\(-L\S*\)\s.*/\1/')
+ fi
+
+ # Using libsamplerate is currently broken
+ #
+ # The giac build system supports --docdir, but the path /usr/share/giac/doc
+ # is hard-coded throughout the source code, so passing anything else to
+ # ./configure --docdir just causes problems. Later, we'll put things right.
+ #
+ # micropython is for specific use in an upstream project
+ econf \
+ --enable-gmpxx \
+ --disable-samplerate \
+ --disable-micropy \
+ --docdir="${EPREFIX}"/usr/share/giac/doc \
+ $(use_enable static-libs static) \
+ $(use_enable gui) \
+ $(use_enable gui png) \
+ $(use_enable ao) \
+ $(use_enable ecm) \
+ $(use_enable glpk) \
+ $(use_enable gc)
+
+}
+
+src_install() {
+ docompress -x "/usr/share/doc/${PF}/"{aide_cas,doc,examples}
+ emake install DESTDIR="${D}"
+
+ # Move all of /usr/share/giac (which contains only documentation) to
+ # its /usr/share/doc/${PF} counterpart.
+ dodir /usr/share/doc
+ mv "${ED}"/usr/share/giac "${ED}/usr/share/doc/${PF}" || die
+
+ # and create a symlink from the original location to the new one
+ dosym "./doc/${PF}" /usr/share/giac
+
+ # This is duplicated in ${ED}/usr/share/doc/${PF}/examples
+ rm -r "${ED}/usr/share/doc/${PF}/doc/Exemples" || die
+
+ # These aren't supposed to be installed at all.
+ find "${ED}/usr/share/doc/${PF}" -type f -name 'Makefile*' -delete || die
+
+ # The French docs are not freely licensed according to the README.
+ rm -r "${ED}/usr/share/doc/${PF}/doc/fr" || die
+
+ dodoc AUTHORS ChangeLog INSTALL NEWS README TROUBLES
+ if ! use gui; then
+ rm -rf \
+ "${ED}"/usr/bin/x* \
+ "${ED}"/usr/share/application-registry \
+ "${ED}"/usr/share/applications \
+ "${ED}"/usr/share/icons \
+ || die "failed to clean up fltk files"
+ fi
+
+ if ! use doc; then
+ rm -r "${ED}/usr/share/doc/${PF}/doc" || die "failed to remove doc directory"
+ else
+ for lang in ${LANGS}; do
+ if use l10n_$lang; then
+ dosym ../aide_cas "/usr/share/doc/${PF}/doc/${lang}/aide_cas"
+ else
+ rm -r "${ED}/usr/share/giac/doc/${lang}" \
+ || die "failed to remove ${lang} documentation"
+ fi
+ done
+ fi
+
+ if ! use examples; then
+ rm -r "${ED}/usr/share/doc/${PF}/examples" \
+ || die "failed to remove examples"
+ fi
+
+ find "${ED}" -type f -name '*.la' -delete || die
+}
+
+pkg_postinst() {
+ if use gui; then
+ xdg_desktop_database_update
+ xdg_icon_cache_update
+ fi
+}
+
+pkg_postrm() {
+ if use gui; then
+ xdg_desktop_database_update
+ xdg_icon_cache_update
+ fi
+}
diff --git a/sci-mathematics/gimps/Manifest b/sci-mathematics/gimps/Manifest
index e8e8bb61147b..a3c626827c16 100644
--- a/sci-mathematics/gimps/Manifest
+++ b/sci-mathematics/gimps/Manifest
@@ -3,6 +3,7 @@ AUX gimps-25.6-conf.d 254 BLAKE2B 44cbf88e3bba505846396c87a68c879d03f76f7f0d0334
AUX gimps-28.9-init.d 722 BLAKE2B 8d55dfbb4166da76e2621097c85165ef49ade916d4ac76576b2abb249d79e0dcd7e37e060a0996576993e6510c051099d6bb7bed6da4ec8800f51b964803c3a8 SHA512 8a7501d8347aa0974268c910890550a2ce5a3d11606670dd69d5e5ccb1046e2994bc5b1f04f9e9dae89174a5a69f9158757079b835fbff50fd25f983190521e9
AUX gimps.service 283 BLAKE2B db6c0c777d514aa0216c1af087418ead25561ffa950752e237e1633a6b6414b56732b84aabd11533ea3dab34f8657358370d21c4730f551d0ff5cf03006b7ad3 SHA512 710c7d075d5542364746b837f2b62257011abb8f45862bf0a1fabd53adb182b5fd969256c7f3221506fef38e81ab1b0f4698efafc1ca7908d9e2d42dee386d8b
AUX gimps.tmpfiles 38 BLAKE2B c306d739ed0a0cc8bb4c80c7051ad93326cf0054d3f7fd61c4ed8a7d518356d521f7d3c3202d0b8b69723b8e7178457a34c65e92732eb15e8e64c3dff468ae2a SHA512 61c5eda13289175cdf55704442ceab4d5391d24cfa49f04155799fc2798e5ad5f1e624802e1c04b99685b1560f9898d1b0fc0c15c82251d1a765dd5de93024d8
+DIST gimps-30.7.9.linux32.tar.gz 5966449 BLAKE2B b31b93417857d338e5e7454e1466bd881422fef51ce0cecb9f7991f7dd19526fcfc01283e0ed871859e32aa4672492fe222bdacd2e06b55ef8401a2169c1846a SHA512 0491f7ec80953b8a86c75b6cc58532130dd51c6abd28617c87208da22a1fb4a1d2f4bea15bf6bd5de3a6706f5b8dcaa5a4cf7bcd39a47f5db0ee4ec74c41cfbd
DIST gimps-30.7.9.linux64.tar.gz 7100830 BLAKE2B 8ebae083d26309f7c624e38c943e3bb0c7fe40a538840970dc222ed33ba5eaa9a5c0767b822682921eaae27f839c1eca5c0204b2c135748002e5d072744afe25 SHA512 5e6f3fbcc50b9b91fda7b286392bb17e58fd8d55a8386f27e206c63c560993da9713513d5eb4355e8e934f2e8703b39fc96f3c6f01058b729330f3526d37479b
DIST p95v303b6.linux32.tar.gz 5702312 BLAKE2B 728c8b8e7e2b5187dc8126bccc5e2c165fbfbc0900d6c35517cd21b78e5292df143641e3766cc0146918062039b1eecab568f9b278f64b1b9197ee2f775603b9 SHA512 3e06fb77be07334949ece3ae152bdf5491f0b7f8e33e0e8ed2af3c34332841975a9514d1993ed2355abfa4e09f93e42093d02f96dc30c3471ae9f974cc2de11a
DIST p95v303b6.linux64.tar.gz 7046127 BLAKE2B 9cde9c2670203071cfc463434a47c8123064cb232bfeb25d8767cad2c25ea75b395e2ec135b7b4a6dc9616e9d6b05ead371e1083274a82468f62a0e1de93c98f SHA512 6d6ded9a1724993d42adee28d400b0337835c52a4ce42271e62efb37134adfc6f017f55475860fbc1224e377a227ef8547b8852a35c082c37e996f4a1c1b570c
@@ -10,5 +11,5 @@ DIST p95v305b2.linux32.tar.gz 5695951 BLAKE2B d97f5b553e0a0563d51a08049c08fe3123
DIST p95v305b2.linux64.tar.gz 7165963 BLAKE2B 3ae20e8e29273650e94ff8774f973240c6b57d7a54e1674e7f741a9d366d3fdad98bb91b8e2abfcf7e1df6319476aa116e921171f2b585a568ee7d5038635531 SHA512 5fe250f7dcc35767fd5f4529219351095d1076f631528d80fa09498e27fa211abc621ef070548c398402143bec5e1d6e6e974155f50eb9f42af0ca179e4e03a8
EBUILD gimps-30.3.6.ebuild 1808 BLAKE2B 3483a73734d0b0008c992a946d36558f1e8ac93872a46bf80d79bb21ae65720c5614df1e1380fb15c2db2537559bc1969fc90dba0614afef1c2f8a6419ea996d SHA512 0dd32cf22373ec922a2716afc7f60ed5af2b0f76ba8f91b94eef891b1137b1dc597f0aca3609f76cb56b3f90b973953decd946d37e02cb6a1db1df1fd81c55a4
EBUILD gimps-30.5.2.ebuild 1884 BLAKE2B ab8a5f9fec9a8cef6bdd4284364201fd29bb7a25070170f4de072e18be7749a7e0406a37f8a5321cbeb5709f1cfb2f1d4d655914d0032d9ee2ec67c59d720b62 SHA512 d2f7e56482733997dc72872e83e0b64a47d15ff1985b61bde6be2aec8c3543a97638d625125e4b30ec4a057e748f3fb422fc06c0c8d25c22a74a221bb675fcc9
-EBUILD gimps-30.7.9.ebuild 1821 BLAKE2B 748341f70cbe142cfe193c48c32a1254d881a3a518621499572e7b72442c4b2e466929018789f03454068c90cd483c8848a2545d82b4ccc05a6b3b510bd7720a SHA512 5f59cfdb4b50d55ce5268f7115bdad851b78e079ad6fdc499e72e211130f25612c6c3cf6c0f5db7cf18579aac0a1dfbef12da9ad43a169f1e51d86025bcd51e6
+EBUILD gimps-30.7.9.ebuild 1930 BLAKE2B ce358754fafc0ff4b7b327424d9ea54d0b7e9ddbf9a3eb63d94d6e823a63850e1ef40284724d2de3b5fd079a51a851a0488212892f63231b2b08eb72c00461fa SHA512 c69e5bbba032b53e2a9c239ebf38021d9f12c7509fa0fb9378f5637b45ebe79f5b526dd8a694893742d87e9ad00049bf178616ea8652d63581923d961b0eaa72
MISC metadata.xml 560 BLAKE2B 01b265f54acd4ad1c9e1d23043d4ce2020fd41843a0efb09003046ea835989393df9935edcc3320eff43d552e47c2bb5afc688ddb96e9e6088c1e1c3a38fca64 SHA512 ba744b0b86d81acf54ed31c70e19be7ee315b6976b29cf0a40e79a7a227b8f68f4262ac2eecd696ddf051dd13de2019dae5df43706ca629bceca738e0e501175
diff --git a/sci-mathematics/gimps/gimps-30.7.9.ebuild b/sci-mathematics/gimps/gimps-30.7.9.ebuild
index f1cf70e083a8..33b432fb3b2f 100644
--- a/sci-mathematics/gimps/gimps-30.7.9.ebuild
+++ b/sci-mathematics/gimps/gimps-30.7.9.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=7
@@ -16,12 +16,13 @@ MY_PV=$(ver_rs 2 'b' )
SRC_URI="
amd64? ( https://www.mersenne.org/ftp_root/gimps/p95v${MY_PV/./}.linux64.tar.gz -> ${P}.linux64.tar.gz )
+ x86? ( https://www.mersenne.org/ftp_root/gimps/p95v${MY_PV/./}.linux32.tar.gz -> ${P}.linux32.tar.gz )
"
SLOT="0"
LICENSE="GIMPS"
RESTRICT="mirror bindist"
-KEYWORDS="-* ~amd64"
+KEYWORDS="-* ~amd64 ~x86"
# Since there are no statically linked binaries for this version of mprime,
# and no static binaries for amd64 in general, we use the dynamically linked
diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index a54e94d036a1..356a56321b13 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,5 +1,7 @@
AUX lean-CMakeLists-fix_flags.patch 1285 BLAKE2B 0507e553c1acf2a53c5267932127117d5ae5ba9015a08c88748b3d82c041f8d904d15cd033dd7934ac55c474fa75a5d4a46f680cc887fee37c05c3f5f3832839 SHA512 11a5918847e45aac7bf79e48d8f881ef5cd3e6b09dbb0979f3f0b88fd36458be21ebeb530158da801399a0cdc8fe382444ff338cd793cd9f1bfced90c5d5a71b
DIST lean-3.35.1.tar.gz 1872461 BLAKE2B 44635b05a7e8ea89522dfb44b8f097ec530419ab79a5413648292ca34019ca744ae3e327cf3a7c627cb7a7a682cfcb2ffc5e6802f2c5ad67e0a7abc303624a3c SHA512 24238cd9e920042f5bf7ba0a121da860e7e9c804d169c888bfabbc5e79e55f556a8920fab0c1a7e72b13501798c5f3fcb068f1705a0cf230f2b89abe1b3045ab
+DIST lean-3.37.0.tar.gz 1875569 BLAKE2B 26d2513da35f0fa7efa6a9bb7706884b95666079e1c0d4349f2745a5908417c0b3d01027901425bf6bc4affdb314a79235c52bac9395bd9e54d53930e6b0dbe0 SHA512 c28139cfff7b40785ab51a9591964adc473f28d7a9877d891a132737c165ce6649924e6c75905442632452b9447c095aae830df347492bae058215d3392a7c09
EBUILD lean-3.35.1-r2.ebuild 1773 BLAKE2B 15392079ec1e4d9eec5dfd9ee13fee05eca98fb2d7fe204a05b793b06588848c339dbb3b01c8c84f30fc45acc2ce8bb74be5841b9aa216a3d5f2d42d3158b7a6 SHA512 89f983bdb770e0fdbbcbd4db2a1bc8de25df33050ed936748788695e4926588471e8963289ef5bd397748abc41aae656f5614f3317b05b70f54dcd43189464d1
+EBUILD lean-3.37.0.ebuild 1773 BLAKE2B 6a332c70ff4fe6731391d180909c732976385466dc28add08014be98e84dd0c7a36a56349516099f6b16966bf70e03d3bf1b19633d9e54c054d2adbb4b9d12e8 SHA512 7601871b46ee585037c8c7600ebf3f4166004314cae3062b3a70838920f0199f5ba4570daa8f1b051a1aa7390e9a9986a0e553088e0a39b1ac45e884bc1ed18a
EBUILD lean-3.9999.ebuild 1773 BLAKE2B 15392079ec1e4d9eec5dfd9ee13fee05eca98fb2d7fe204a05b793b06588848c339dbb3b01c8c84f30fc45acc2ce8bb74be5841b9aa216a3d5f2d42d3158b7a6 SHA512 89f983bdb770e0fdbbcbd4db2a1bc8de25df33050ed936748788695e4926588471e8963289ef5bd397748abc41aae656f5614f3317b05b70f54dcd43189464d1
MISC metadata.xml 672 BLAKE2B 60612895864a164fce242ff1daa5390444c74fbb56fbc062c5448a2770ecab1048d67ce672ff543bab7b410eae118fa9fb087319e724a60437b4da2d8638e40d SHA512 2496062c9db3c2d1c9467b00fe20c0618df8cbdce2799dfdabd6c4fda4b5393bd49392c438fa81f07330fbf1aec3556b369f0fa88acff44e65b0c2cee8e94ea7
diff --git a/sci-mathematics/lean/lean-3.37.0.ebuild b/sci-mathematics/lean/lean-3.37.0.ebuild
new file mode 100644
index 000000000000..e47a48054580
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.37.0.ebuild
@@ -0,0 +1,75 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+MAJOR=$(ver_cut 1)
+CMAKE_IN_SOURCE_BUILD="ON"
+
+inherit cmake optfeature readme.gentoo-r1
+
+DESCRIPTION="The Lean Theorem Prover"
+HOMEPAGE="https://leanprover-community.github.io/"
+
+if [[ "${PV}" == *9999* ]]; then
+ inherit git-r3
+ EGIT_REPO_URI="https://github.com/leanprover-community/lean.git"
+else
+ SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz"
+ KEYWORDS="~amd64 ~x86"
+fi
+S="${WORKDIR}/lean-${PV}/src"
+
+LICENSE="Apache-2.0"
+SLOT="0/${MAJOR}"
+IUSE="debug +json +threads"
+
+RDEPEND="dev-libs/gmp:="
+DEPEND="${RDEPEND}"
+
+PATCHES=( "${FILESDIR}/${PN}-CMakeLists-fix_flags.patch" )
+
+src_configure() {
+ local CMAKE_BUILD_TYPE
+ if use debug; then
+ CMAKE_BUILD_TYPE="Debug"
+ else
+ CMAKE_BUILD_TYPE="Release"
+ fi
+
+ local mycmakeargs=(
+ -DALPHA=ON
+ -DAUTO_THREAD_FINALIZATION=ON
+ -DJSON=$(usex json)
+ -DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
+ -DMULTI_THREAD=$(usex threads)
+ -DUSE_GITHASH=OFF
+ )
+ cmake_src_configure
+}
+
+src_test() {
+ local myctestargs=(
+ # Disable problematic "style_check" cpplint test,
+ # this also removes the python test dependency
+ --exclude-regex style_check
+ )
+ cmake_src_test
+}
+
+src_install() {
+ cmake_src_install
+
+ local DISABLE_AUTOFORMATTING="yes"
+ local DOC_CONTENTS="You probably want to use lean with mathlib, you can either:
+ - Do not install mathlib globally and use local versions
+ - Use leanproject from sci-mathematics/mathlib-tools
+ $ leanproject global-install
+ - Use leanpkg and compile mathlib (which will take some time)
+ $ leanpkg install https://github.com/leanprover-community/mathlib"
+ readme.gentoo_create_doc
+}
+
+pkg_postinst() {
+ readme.gentoo_print_elog
+}
diff --git a/sci-mathematics/spin/Manifest b/sci-mathematics/spin/Manifest
index f55709e26d98..0aa27ce2cfe8 100644
--- a/sci-mathematics/spin/Manifest
+++ b/sci-mathematics/spin/Manifest
@@ -1,4 +1,5 @@
AUX spin-6.5.2-makefile.patch 320 BLAKE2B d88604300a9a1c7f16339e9c9c0ba96f79e3a0d08f041eba6c623d8e1d62d4a247f0ad6e06e83816a011ba072bfb7bd6afe39df796cfb1b80ad514e6cab33e76 SHA512 89166f068ab54c99c55029c7d936db663335e99c6e884b9885fe0478bb211bc186d32302ce933bd8e597bb78c72f2a0d016c8e661095a58761d437b89914c573
+AUX spin-6.5.2-nesting_limit.patch 1755 BLAKE2B 8c7b54262492dfc399bfbd90383a801375f4a6c6d7604f2f17841285b3ffb2ef32db67a02bdf4bee3b71633b436e057d4e0d6594c1a545ee7278c578546fb563 SHA512 dd92d130c61698d44c88e13ff8b744f3412dd5940e37c0c5e971889644e5482fcac1b0483e8dae0b6197749828a8dbdf74a5402fc2e8fb7dd88876199e02832a
DIST spin-6.5.2.tar.gz 6084903 BLAKE2B a075043c55609de5860c3a428d356a9618a4062667e06d92797e1fb87cb4c805ac90ac580c7d9dfac1d5be1dda4c7f9c9f72927826b921c23710a858adb3eb4d SHA512 ff1d378076995fa5a8b66dd31d19d8bad6296b968183180251d267c926c20775edda927a31f466199e01231f6233c3a5166fd51ec44b02d570070e857d8ba7f9
-EBUILD spin-6.5.2.ebuild 1055 BLAKE2B 577a87309cad0970b307d592f69a83c187e81ec74e409aa007321a88c57a0740641739a0bc3676241766697d723aa227000ddb86b5cd3a8e7699dd0e43cf0f95 SHA512 0e55d1c692d58e9f9a35ee529d550fab597438215921c0252146541e18f8cfa186943ce656be5a46d043466408746a3ebdd921ecb6f88ebf8ad77272b28ec919
+EBUILD spin-6.5.2-r1.ebuild 1102 BLAKE2B b71ca487a6d3c75d9522d2f3c9cfee41b5de4fa721cd8466bd408b36332e445b8aa23b6038c8751d90a3a681a2697d7c3467d023b30e193eeb2a85c5f9051f86 SHA512 462f90050a0fda2451e8e4f1bd1486270a8082b8491dc221921ca7b3d7f37ba7c165992cc2ad30663aadca4838b8546e1003646d57bfbb66d33e5cb59d434f1e
MISC metadata.xml 327 BLAKE2B 1b6a2bbece4fff801301d1bc5b86ebea4fe32096f1fb76d24831bd299608d73116261733e1318cf76532a336c467b394655157145ba565e256626ca66bf191be SHA512 5baaef50807b13c5a3e63d394a0df2b75ecb7973d1467d918329b55536ff6280da086311ee56bcff9fc156f377f077916d572f3cf8a1756d959b4bdb70b55ae8
diff --git a/sci-mathematics/spin/files/spin-6.5.2-nesting_limit.patch b/sci-mathematics/spin/files/spin-6.5.2-nesting_limit.patch
new file mode 100644
index 000000000000..c73152e8485c
--- /dev/null
+++ b/sci-mathematics/spin/files/spin-6.5.2-nesting_limit.patch
@@ -0,0 +1,55 @@
+Backported upstream changes to address CVE-2021-46168.
+
+From 62cf91c944ea457c218528e9021443a0cbe05758 Mon Sep 17 00:00:00 2001
+From: nimble-code <gerard.holzmann@gmail.com>
+Date: Sun, 2 Jan 2022 11:26:40 -0800
+Subject: [PATCH] fix
+
+--- a/sched.c
++++ b/sched.c
+@@ -18,7 +18,7 @@ extern int lineno, nr_errs, dumptab, xspin, jumpsteps, columns;
+ extern int u_sync, Elcnt, interactive, TstOnly, cutoff;
+ extern short has_enabled, has_priority, has_code, replay;
+ extern int limited_vis, product, nclaims, old_priority_rules;
+-extern int old_scope_rules, scope_seq[128], scope_level, has_stdin;
++extern int old_scope_rules, scope_seq[256], scope_level, has_stdin;
+
+ extern int pc_highest(Lextok *n);
+ extern void putpostlude(void);
+--- a/spinlex.c
++++ b/spinlex.c
+@@ -51,7 +51,7 @@ extern int implied_semis, ltl_mode, in_seq, par_cnt;
+
+ short has_stack = 0;
+ int lineno = 1;
+-int scope_seq[128], scope_level = 0;
++int scope_seq[256], scope_level = 0;
+ char CurScope[MAXSCOPESZ];
+ char yytext[2048];
+ FILE *yyin, *yyout;
+From 9ecb1af6d174532f3a77acae3a1d424fe7345a3e Mon Sep 17 00:00:00 2001
+From: nimble-code <gerard.holzmann@gmail.com>
+Date: Sat, 15 Jan 2022 10:39:38 -0800
+Subject: [PATCH] nesting limit
+
+--- a/spinlex.c
++++ b/spinlex.c
+@@ -1704,8 +1704,16 @@ lex(void)
+ case '|': c = follow('|', OR, '|'); break;
+ case ';': c = SEMI; break;
+ case '.': c = follow('.', DOTDOT, '.'); break;
+- case '{': scope_seq[scope_level++]++; set_cur_scope(); break;
+- case '}': scope_level--; set_cur_scope(); break;
++ case '{':
++ assert(scope_level < sizeof(scope_seq)-1);
++ scope_seq[scope_level++]++;
++ set_cur_scope();
++ break;
++ case '}':
++ assert(scope_level > 0);
++ scope_level--;
++ set_cur_scope();
++ break;
+ default : break;
+ }
+ ValToken(0, c)
diff --git a/sci-mathematics/spin/spin-6.5.2.ebuild b/sci-mathematics/spin/spin-6.5.2-r1.ebuild
index 5e4110e9abeb..0e1f17681a7c 100644
--- a/sci-mathematics/spin/spin-6.5.2.ebuild
+++ b/sci-mathematics/spin/spin-6.5.2-r1.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
@@ -27,6 +27,7 @@ BDEPEND="virtual/yacc"
PATCHES=(
"${FILESDIR}"/${PN}-6.5.2-makefile.patch
+ "${FILESDIR}"/${PN}-6.5.2-nesting_limit.patch
)
S="${WORKDIR}"/${MY_P}/Src
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index 56bc0cb38a09..fa40a5a4e727 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1,3 +1,3 @@
DIST why3-1.4.0.tar.gz 6306524 BLAKE2B ade7803a608d090ea06d974ae47e920993de92a5849d60bd63dba68252919a8f4fd1f0f6a3c975fdb727c4ae3afe13921b5d31a14c005e0d08f518e64bcf05e5 SHA512 b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a
-EBUILD why3-1.4.0-r1.ebuild 2089 BLAKE2B 5d3ccd3ab09f320640dc30b20d4dd0e4caad312bcbad1685507839f5803221ae8ac5da9e184aece2f77afa439e4e8cae5541f1ba02f71b0713ea9989f4758581 SHA512 6dc7c9572d02fccfec6445268f1f880f540c9cc53d618328865baf958dd6cc310904fe991341f2e7156c961ae38e6c73a3572a73cebb55937fa2055384a6a62a
+EBUILD why3-1.4.0-r2.ebuild 2170 BLAKE2B 4a69d3d119d8ac3dd1d33a820717b1f59d88eb888f168ab5c019e23457de62d81ee07bf7d64ad48a63ab90fe864084588a54d4e7b8163e86cff5f2dbd8185a4e SHA512 99073cf81b27903bd21c0c7d7ce898a449191aeb6e23e3ac81e58cebf6704a2a829d03c847c810093f8ee835f677bae1f64c8b20ffc9f37f74e04ee11e771a5e
MISC metadata.xml 1680 BLAKE2B 4443de2368a7003db59e341bc671c8aa4c664be935b65df1fd1af161900a977194e012ef3b486f877a77f6b32405d700ee814d7cdeb10703b2462f7337965fb5 SHA512 7cc8dbe476d891d1311cec6ea15b1c6e6391c32bdbe715fe1fb7d2549763384c148e0509fb2b7c68b98b70eec1feeb4d94271378a343d50ef58cb5bb8a07a109
diff --git a/sci-mathematics/why3/why3-1.4.0-r1.ebuild b/sci-mathematics/why3/why3-1.4.0-r2.ebuild
index badf49628e94..85da04d96b8a 100644
--- a/sci-mathematics/why3/why3-1.4.0-r1.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0-r2.ebuild
@@ -37,7 +37,9 @@ BDEPEND="
dev-python/sphinx
dev-python/sphinxcontrib-bibtex
media-gfx/graphviz
- || ( dev-texlive/texlive-latex dev-tex/latexmk dev-tex/rubber )
+ dev-texlive/texlive-latex
+ dev-texlive/texlive-fontsrecommended
+ dev-texlive/texlive-latexextra
)
"
@@ -48,6 +50,7 @@ src_prepare() {
sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
-e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
+ -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
-i Makefile.in || die
eautoreconf
diff --git a/sci-mathematics/z3/Manifest b/sci-mathematics/z3/Manifest
index a8bfa9189478..8d1c5c24bc08 100644
--- a/sci-mathematics/z3/Manifest
+++ b/sci-mathematics/z3/Manifest
@@ -1,7 +1,5 @@
-DIST z3-4.8.11b.tar.gz 4801435 BLAKE2B 903a04246fe4dedc96fda653fa9e3a57a80b951d20b992306bd07bc778cf0a94cf36fe4ed3f178bb26196a1ca294834c784a117fe906d52b82f874a43869d110 SHA512 dfcfc85209dd00aa5f07de0a7e7186a33442b72b94b05c01f53350b9281551be2a2c21ad5e7814bc2c52a3329be8df578e6be8c387cbfdc3a9d3bef0611d6613
DIST z3-4.8.13.tar.gz 5103999 BLAKE2B 5500bbc71e7a863092a36bdd2bc04f5a4435e9d8fdc62c7956aa2546ffa9e39344c9528bf802f6e4c211c799e873f2673dbf8b113599dcbb694ac040ada2e9a0 SHA512 c5e8f34525ed3b6b2935d7f01ce2f90f5dd99b4cdd035664b36c967fb1c7f3b05abed45c7288e2261723e73d68728ee91a0f67d92012d86b04598d7b54369c30
DIST z3-4.8.14.tar.gz 5113598 BLAKE2B c6a82cec33e879123c33506897ac02be682d08a6432da0b11c6918f2664fd7249d8874ccb6f543907f789cc3b40b126465548abeabf4ac16d2ee791ce179742a SHA512 10170516ca472258d2f9df28cd036e43023a76a25f1e1670290c62f3890d935bf82770970054a5fd3a0f02559409e7ed4b18fb08347c040ff2f9e0918e152aab
-EBUILD z3-4.8.11b.ebuild 2610 BLAKE2B 62e0920d9e4ba69c65fff37bdc74c70f7177853f3b8ff61b2f4a50dd09d72d0f42ffcf71da152e2c5b80d1ff4e26b96d683f10a439c8a8270cc8f6dc50fb3faf SHA512 457a93cfee6bb224e5d1987a7ecaeba18f3f478ac26a222ed4c93e249225c46834d07800e9049931833e01d8ce1e5fadca09ab24df261fbc4b1165e1290845f9
-EBUILD z3-4.8.13.ebuild 2599 BLAKE2B 7d4b057cf1b8a9853db7d5f482a7457cd55fe1e4c3bdaa727db86fa69d0d144ccb2de9e25e51f34c7edb7c3487e6b0f4a51a76890dc309820e8096e39d7d9f01 SHA512 3c40f3b590e1d46defc757c6133136693e5ee5129949dfd1f7dbf49bc7e0634c591c2ba6e0758b0a0e9b979425c9501864020e4e12cc685ce963d74d5b2b6889
+EBUILD z3-4.8.13.ebuild 2594 BLAKE2B 672fa6fcbf0d98a092bbdd264d57dd8ca52a84fe9ae220eeb429697ec4eedd786764d412a4995d6bbc295c83bf0244934533f60b1d355c6ca600dabf0b0b455d SHA512 a5e24ea461889c39524412961cb77bcd40f5771ecec5a15a05293768435ef8261de0929c9387d6d79ef582f853dc66df6f73e4c57d70d30e19119167da89b17f
EBUILD z3-4.8.14.ebuild 2599 BLAKE2B 7d4b057cf1b8a9853db7d5f482a7457cd55fe1e4c3bdaa727db86fa69d0d144ccb2de9e25e51f34c7edb7c3487e6b0f4a51a76890dc309820e8096e39d7d9f01 SHA512 3c40f3b590e1d46defc757c6133136693e5ee5129949dfd1f7dbf49bc7e0634c591c2ba6e0758b0a0e9b979425c9501864020e4e12cc685ce963d74d5b2b6889
MISC metadata.xml 617 BLAKE2B f940ac3d7c159dadf4398164b749eaded84c12af5553a154d97fd9bfb939c72e3122e08e11c1c9764514f59a87695534daff6628bd15be4de834c7cfdb65d7f9 SHA512 758df481a60606de12c5a450162ee89fd2f68f842675b3bf280f024fcd61232228476ac889e60c09e42ebae01ad855b32ad77793ba7fa5714861ccc5ca52bfc7
diff --git a/sci-mathematics/z3/z3-4.8.11b.ebuild b/sci-mathematics/z3/z3-4.8.11b.ebuild
deleted file mode 100644
index aec3b57fd997..000000000000
--- a/sci-mathematics/z3/z3-4.8.11b.ebuild
+++ /dev/null
@@ -1,103 +0,0 @@
-# Copyright 1999-2021 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-CMAKE_ECLASS=cmake
-PYTHON_COMPAT=( python3_{8..10} )
-
-inherit cmake-multilib java-pkg-opt-2 python-single-r1 toolchain-funcs
-
-DESCRIPTION="An efficient theorem prover"
-HOMEPAGE="https://github.com/Z3Prover/z3/"
-SRC_URI="https://github.com/Z3Prover/z3/archive/${P}.tar.gz"
-S=${WORKDIR}/z3-${P}
-
-SLOT="0/4.8"
-LICENSE="MIT"
-KEYWORDS="amd64 arm arm64 ~ppc ppc64 ~riscv x86"
-IUSE="doc examples gmp isabelle java python"
-REQUIRED_USE="${PYTHON_REQUIRED_USE}"
-
-RDEPEND="${PYTHON_DEPS}
- gmp? ( dev-libs/gmp:0=[cxx(+),${MULTILIB_USEDEP}] )"
-DEPEND="${RDEPEND}
- java? ( >=virtual/jdk-1.8 )"
-BDEPEND="
- doc? ( app-doc/doxygen )"
-
-CMAKE_BUILD_TYPE=RelWithDebInfo
-
-src_prepare() {
- cmake_src_prepare
- java-pkg-opt-2_src_prepare
-}
-
-multilib_src_configure() {
- local mycmakeargs=(
- -DCMAKE_INSTALL_DOCDIR="${EPREFIX}/usr/share/doc/${P}"
- -DZ3_USE_LIB_GMP=$(usex gmp)
- -DZ3_ENABLE_EXAMPLE_TARGETS=OFF
- -DZ3_BUILD_DOCUMENTATION=$(multilib_native_usex doc)
- -DZ3_BUILD_PYTHON_BINDINGS=$(multilib_native_usex python)
- -DZ3_BUILD_JAVA_BINDINGS=$(multilib_native_usex java)
- -DZ3_INCLUDE_GIT_DESCRIBE=OFF
- -DZ3_INCLUDE_GIT_HASH=OFF
- )
-
- multilib_is_native_abi && use java && mycmakeargs+=( -DJAVA_HOME="$(java-config -g JAVA_HOME )" )
-
- cmake_src_configure
-}
-
-multilib_src_test() {
- cmake_build test-z3
- set -- "${BUILD_DIR}"/test-z3 /a
- echo "${@}" >&2
- "${@}" || die
-}
-
-multilib_src_install_all() {
- dodoc README.md RELEASE_NOTES
- use examples && dodoc -r examples
- use python && python_optimize
-
- if use isabelle; then
- insinto /usr/share/Isabelle/contrib/${P}/etc
- newins - settings <<-EOF
- Z3_COMPONENT="\$COMPONENT"
- Z3_HOME="${EPREFIX}/usr/bin"
- Z3_SOLVER="${EPREFIX}/usr/bin/z3"
- Z3_REMOTE_SOLVER="z3"
- Z3_VERSION="${PV}"
- Z3_INSTALLED="yes"
- Z3_NON_COMMERCIAL="yes"
- EOF
- fi
-}
-
-pkg_postinst() {
- if use isabelle; then
- if [[ -f ${ROOT}/etc/isabelle/components ]]; then
- sed -e "/contrib\/${PN}-[0-9.]*/d" \
- -i "${ROOT}/etc/isabelle/components" || die
- cat <<-EOF >> "${ROOT}/etc/isabelle/components" || die
- contrib/${P}
- EOF
- fi
- fi
-}
-
-pkg_postrm() {
- if use isabelle; then
- if [[ ! ${REPLACING_VERSIONS} ]]; then
- if [[ -f "${ROOT}/etc/isabelle/components" ]]; then
- # Note: this sed should only match the version of this ebuild
- # Which is what we want as we do not want to remove the line
- # of a new Isabelle component being installed during an upgrade.
- sed -e "/contrib\/${P}/d" \
- -i "${ROOT}/etc/isabelle/components" || die
- fi
- fi
- fi
-}
diff --git a/sci-mathematics/z3/z3-4.8.13.ebuild b/sci-mathematics/z3/z3-4.8.13.ebuild
index 488e59de75e0..66a173a9a933 100644
--- a/sci-mathematics/z3/z3-4.8.13.ebuild
+++ b/sci-mathematics/z3/z3-4.8.13.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=7
@@ -15,7 +15,7 @@ S=${WORKDIR}/z3-${P}
SLOT="0/4.8"
LICENSE="MIT"
-KEYWORDS="~amd64 ~arm ~arm64 ~ppc ~ppc64 ~riscv ~x86"
+KEYWORDS="amd64 arm arm64 ~ppc ppc64 ~riscv x86"
IUSE="doc examples gmp isabelle java python"
REQUIRED_USE="${PYTHON_REQUIRED_USE}"
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-27 21:58:30 +0000