From ad391b961414c99124b93cb86695c04bd8d57937 Mon Sep 17 00:00:00 2001 From: V3n3RiX Date: Wed, 11 Jan 2023 05:43:34 +0000 Subject: gentoo auto-resync : 11:01:2023 - 05:43:34 --- sci-mathematics/Manifest.gz | Bin 17875 -> 18371 bytes sci-mathematics/boolector/Manifest | 3 + .../boolector/boolector-3.2.2_p20220110.ebuild | 77 +++++++++++++++ sci-mathematics/boolector/metadata.xml | 32 +++++++ sci-mathematics/btor2tools/Manifest | 5 + .../btor2tools/btor2tools-1.0.0_pre20220518.ebuild | 39 ++++++++ ...tools-1.0.0_pre20220518-cmake-also-static.patch | 28 ++++++ ...btor2tools-1.0.0_pre20220518-cmake-clfags.patch | 19 ++++ sci-mathematics/btor2tools/metadata.xml | 13 +++ sci-mathematics/cadical/Manifest | 2 +- sci-mathematics/cadical/cadical-1.5.3-r1.ebuild | 37 ++++++++ sci-mathematics/cadical/cadical-1.5.3.ebuild | 35 ------- sci-mathematics/cubicle/Manifest | 4 + sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild | 71 ++++++++++++++ sci-mathematics/cubicle/files/50cubicle-gentoo.el | 4 + sci-mathematics/cubicle/metadata.xml | 31 +++++++ sci-mathematics/picosat/Manifest | 2 +- sci-mathematics/picosat/picosat-965-r1.ebuild | 39 ++++++++ sci-mathematics/picosat/picosat-965.ebuild | 38 -------- sci-mathematics/singular/Manifest | 4 +- sci-mathematics/singular/singular-4.3.1_p2.ebuild | 103 --------------------- sci-mathematics/singular/singular-4.3.1_p3.ebuild | 103 +++++++++++++++++++++ 22 files changed, 509 insertions(+), 180 deletions(-) create mode 100644 sci-mathematics/boolector/Manifest create mode 100644 sci-mathematics/boolector/boolector-3.2.2_p20220110.ebuild create mode 100644 sci-mathematics/boolector/metadata.xml create mode 100644 sci-mathematics/btor2tools/Manifest create mode 100644 sci-mathematics/btor2tools/btor2tools-1.0.0_pre20220518.ebuild create mode 100644 sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-also-static.patch create mode 100644 sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-clfags.patch create mode 100644 sci-mathematics/btor2tools/metadata.xml create mode 100644 sci-mathematics/cadical/cadical-1.5.3-r1.ebuild delete mode 100644 sci-mathematics/cadical/cadical-1.5.3.ebuild create mode 100644 sci-mathematics/cubicle/Manifest create mode 100644 sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild create mode 100644 sci-mathematics/cubicle/files/50cubicle-gentoo.el create mode 100644 sci-mathematics/cubicle/metadata.xml create mode 100644 sci-mathematics/picosat/picosat-965-r1.ebuild delete mode 100644 sci-mathematics/picosat/picosat-965.ebuild delete mode 100644 sci-mathematics/singular/singular-4.3.1_p2.ebuild create mode 100644 sci-mathematics/singular/singular-4.3.1_p3.ebuild (limited to 'sci-mathematics') diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz index 3f0ad1f98c27..8406de39f580 100644 Binary files a/sci-mathematics/Manifest.gz and b/sci-mathematics/Manifest.gz differ diff --git a/sci-mathematics/boolector/Manifest b/sci-mathematics/boolector/Manifest new file mode 100644 index 000000000000..01c7a42e9bbe --- /dev/null +++ b/sci-mathematics/boolector/Manifest @@ -0,0 +1,3 @@ +DIST boolector-3.2.2_p20220110.tar.gz 1567668 BLAKE2B 6816f0434d88c790a27b9afe4c3b63c18a55b14f9f13b092f2940309e34842fe4868bf8d378bad130c4561d25e7d79b356fc27d9422bd42ba1b74ff98be36f72 SHA512 b1b964c155c8227e631025cf6bff69cf54728b1d875c2bd44a5a1ddb2857de2ab8fefc96d194faa5f98015e730b417d46a415ea601740e890df07ad5e50ad656 +EBUILD boolector-3.2.2_p20220110.ebuild 1791 BLAKE2B cf124ec570c488760e50384cb59131557fb5860729e7204ee84b3f123fe9a4a4ce79df946f4038bc018d25c635abe57ec8d29528e108e4ecb80705ad8beeb8fc SHA512 a8c0c27f80e29f5177bc1026f1598d86f12fd0142d983e8f65a064312d55234ab59213f658dcee9bb9345502201c64c3b813e48dea315471c6d23a0fec68868a +MISC metadata.xml 1245 BLAKE2B a04e1e5a6af857100b8b569f57f4d2610593e9eb741513e4e6405a8fa9828471b92aaa1ad57a3163dc2f251b5664493692f92477b7191621ff8fd76eed9f57e7 SHA512 81257f7be3b21bf10caad654d5747ef2d978c0df5a05049b890420e2d170b7a4fa06151da0604a8b1b6e7daf2fb01344003c9243205a94b4040c580beb414836 diff --git a/sci-mathematics/boolector/boolector-3.2.2_p20220110.ebuild b/sci-mathematics/boolector/boolector-3.2.2_p20220110.ebuild new file mode 100644 index 000000000000..289c5358a5b9 --- /dev/null +++ b/sci-mathematics/boolector/boolector-3.2.2_p20220110.ebuild @@ -0,0 +1,77 @@ +# Copyright 1999-2023 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +H=13a8a06d561041cafcaf5458e404c1ec354b2841 +PYTHON_COMPAT=( python3_{8..11} ) + +inherit python-single-r1 cmake + +DESCRIPTION="Fast SMT solver for bit-vectors, arrays and uninterpreted functions" +HOMEPAGE="https://boolector.github.io/ + https://github.com/Boolector/boolector/" + +if [[ "${PV}" == *9999* ]] ; then + inherit git-r3 + EGIT_REPO_URI="https://github.com/Boolector/${PN}.git" +else + SRC_URI="https://github.com/Boolector/${PN}/archive/${H}.tar.gz + -> ${P}.tar.gz" + S="${WORKDIR}"/${PN}-${H} + KEYWORDS="~amd64 ~x86" +fi + +LICENSE="MIT" +SLOT="0" +IUSE="cryptominisat examples +gmp minisat +picosat python test" +REQUIRED_USE=" + python? ( ${PYTHON_REQUIRED_USE} ) + || ( cryptominisat minisat picosat ) +" +RESTRICT="!test? ( test )" + +RDEPEND=" + sci-mathematics/btor2tools:= + cryptominisat? ( sci-mathematics/cryptominisat:= ) + gmp? ( dev-libs/gmp:= ) + minisat? ( sci-mathematics/minisat:= ) + picosat? ( sci-mathematics/picosat:= ) + python? ( ${PYTHON_DEPS} ) +" +DEPEND="${RDEPEND}" +BDEPEND="test? ( dev-cpp/gtest )" + +pkg_setup() { + use python && python-single-r1_pkg_setup +} + +src_configure() { + local mycmakeargs=( + -DBUILD_SHARED_LIBS=ON + -DUSE_PYTHON2=OFF + -DPYTHON=$(usex python) + -DTESTING=$(usex test) + -DUSE_GMP=$(usex gmp) + -DUSE_PYTHON3=$(usex python) + + # Integration with other SMT solvers + -DUSE_LINGELING=OFF # Not packaged yet. + -DUSE_CADICAL=OFF # Fails to link. + -DUSE_CMS=$(usex cryptominisat) + -DUSE_MINISAT=$(usex minisat) + -DUSE_PICOSAT=$(usex picosat) + ) + cmake_src_configure +} + +src_install() { + cmake_src_install + + dodir /usr/$(get_libdir) + mv "${ED}"/usr/lib/*.so "${ED}"/usr/$(get_libdir)/ || die + + if use examples ; then + dodoc -r examples + fi +} diff --git a/sci-mathematics/boolector/metadata.xml b/sci-mathematics/boolector/metadata.xml new file mode 100644 index 000000000000..b61474ce8353 --- /dev/null +++ b/sci-mathematics/boolector/metadata.xml @@ -0,0 +1,32 @@ + + + + + + sci-mathematics@gentoo.org + Gentoo Mathematics Project + + + Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories + of fixed-size bit-vectors, arrays and uninterpreted functions. It supports + the SMT-LIB logics BV, QF_ABV, QF_AUFBV, QF_BV and QF_UFBV. Boolector + provides a rich C and Python API and supports incremental solving, both + with the SMT-LIB commands push and pop, and as solving under assumptions. + + + + Enable support for sci-mathematics/cryptominisat + + + Enable support for sci-mathematics/minisat + + + Enable support for sci-mathematics/picosat + + + + https://github.com/Boolector/boolector/issues/ + https://boolector.github.io/docs/index.html + Boolector/boolector + + diff --git a/sci-mathematics/btor2tools/Manifest b/sci-mathematics/btor2tools/Manifest new file mode 100644 index 000000000000..a6f98fe33e62 --- /dev/null +++ b/sci-mathematics/btor2tools/Manifest @@ -0,0 +1,5 @@ +AUX btor2tools-1.0.0_pre20220518-cmake-also-static.patch 804 BLAKE2B bdfb9e99a98f9cd9989ba0eb10490877b24553c5db478281c8771bb922060c20412521dbab513e5742daa4878189313cae075d044b4ba4ee8f265bde15aef520 SHA512 ac03a333bd0563559b940d4b4b0f2e5da4440503e5ec84b0a28ddb4c4b5a17cf96910c025abe088f93dc82147023cfaa598eb18a6aa409e690baffe0166d10d6 +AUX btor2tools-1.0.0_pre20220518-cmake-clfags.patch 551 BLAKE2B 8cc8c427a2ec7defc4bd7f251b2a2a6484bc321b0f0d88a7099e8a69963cfbf6b69d13dbce4f54874d8138ec01ae870752a947a01c93c3cf996456c546ce012e SHA512 a6c446440405ab44b9bffb8316d170782241d77334c5837820ee0ea1e6da5ff97121b966a49af9c15e8e0e2a184ae3781166eb9c0ba07c4319dd92fed105ae2d +DIST btor2tools-1.0.0_pre20220518.tar.gz 87420 BLAKE2B df8ddc8f286c32c580a8feaf0c7e90dff113d2b0303e3da0a378f2906cd34134ea91707cd40c95c38782990bf4d815416b3a566680f4d6668ddca46321ae530a SHA512 96e17327de311b3d16e086031038a8248431d0dda75b83ce137d6526a096b69fc062290f92ec5b58fffb56aa25437835f97a96bd15f0044d4d52263bf386d928 +EBUILD btor2tools-1.0.0_pre20220518.ebuild 783 BLAKE2B a911486c6340478d3c00421c77f8f4eca47e442cae1fd0df8c048e5ea27065c219ec58af95618eba7b837b4ee20b250746a92d0d915a66a1f01b1287feabed62 SHA512 2bb3a28dd080ffd68f8e37c92a58a12ac1f19a2864e116d4c66d46e2e793d733fe1d9fdfc2539c1c3c108f6590cb4bb0564c009d8b0b854c7f43bb1e0f644f7e +MISC metadata.xml 437 BLAKE2B 93f1e3a98b8dd3edd95de3bd8f830427a9e05dcfc73690899ed16ec49be25bfd524d86fcaa9735d15c22515b98d13ded8a95c7a39e4970e3035c72e4cbe7d544 SHA512 39b7bd39e597f6d3086358738cb2d668f0317af3a8674eb4c032f59c64de0ceada799900bd193f244f049f51e1a91dcd9bb4474db39ac88967086206f3090a62 diff --git a/sci-mathematics/btor2tools/btor2tools-1.0.0_pre20220518.ebuild b/sci-mathematics/btor2tools/btor2tools-1.0.0_pre20220518.ebuild new file mode 100644 index 000000000000..efade1283737 --- /dev/null +++ b/sci-mathematics/btor2tools/btor2tools-1.0.0_pre20220518.ebuild @@ -0,0 +1,39 @@ +# Copyright 1999-2023 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +H=b8456dda4780789e882f5791eb486f295ade4da4 + +inherit cmake + +DESCRIPTION="Generic parser and tools for the BTOR2 format" +HOMEPAGE="https://github.com/Boolector/btor2tools/" + +if [[ "${PV}" == *9999* ]] ; then + inherit git-r3 + EGIT_REPO_URI="https://github.com/Boolector/${PN}.git" +else + SRC_URI="https://github.com/Boolector/${PN}/archive/${H}.tar.gz + -> ${P}.tar.gz" + S="${WORKDIR}"/${PN}-${H} + KEYWORDS="~amd64 ~x86" +fi + +LICENSE="MIT" +SLOT="0" +IUSE="examples" + +PATCHES=( + "${FILESDIR}"/${P}-cmake-also-static.patch + "${FILESDIR}"/${P}-cmake-clfags.patch +) + +src_install() { + cmake_src_install + + if use examples ; then + insinto /usr/share/${PN} + dodoc -r examples + fi +} diff --git a/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-also-static.patch b/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-also-static.patch new file mode 100644 index 000000000000..061ddac84194 --- /dev/null +++ b/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-also-static.patch @@ -0,0 +1,28 @@ +--- a/src/CMakeLists.txt ++++ b/src/CMakeLists.txt +@@ -1,4 +1,5 @@ + add_library(btor2parser ++ SHARED + btor2parser/btor2parser.c + ) + target_include_directories(btor2parser PRIVATE .) +@@ -10,6 +11,19 @@ install( + PUBLIC_HEADER DESTINATION ${CMAKE_INSTALL_INCLUDEDIR} + ) + ++add_library(btor2parser_static ++ STATIC ++ btor2parser/btor2parser.c ++) ++target_include_directories(btor2parser_static PRIVATE .) ++set_target_properties(btor2parser_static PROPERTIES OUTPUT_NAME btor2parser) ++set_target_properties(btor2parser_static PROPERTIES PUBLIC_HEADER btor2parser/btor2parser.h) ++install( ++ TARGETS btor2parser_static ++ ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR} ++ PUBLIC_HEADER DESTINATION ${CMAKE_INSTALL_INCLUDEDIR} ++) ++ + add_executable(btorsim + btorsim/btorsimam.cpp + btorsim/btorsimstate.cpp diff --git a/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-clfags.patch b/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-clfags.patch new file mode 100644 index 000000000000..84c6631c9219 --- /dev/null +++ b/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-cmake-clfags.patch @@ -0,0 +1,19 @@ +--- a/CMakeLists.txt ++++ b/CMakeLists.txt +@@ -91,16 +91,6 @@ add_check_c_cxx_flag("-Wredundant-decls") + add_check_c_flag("-std=gnu99") + add_required_cxx_flag("-std=gnu++11") + +-if(CMAKE_BUILD_TYPE STREQUAL "Debug") +- add_check_c_cxx_flag("-g3") +- add_check_c_cxx_flag("-ggdb") +-else() +- add_check_c_cxx_flag("-O3") +- if(NOT CHECK) +- add_check_c_cxx_flag("-DNDEBUG") +- endif() +-endif() +- + if(ASAN) + # -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set, + # otherwise the -fsanitize=address check will fail while linking. diff --git a/sci-mathematics/btor2tools/metadata.xml b/sci-mathematics/btor2tools/metadata.xml new file mode 100644 index 000000000000..237d97fb7791 --- /dev/null +++ b/sci-mathematics/btor2tools/metadata.xml @@ -0,0 +1,13 @@ + + + + + + sci-mathematics@gentoo.org + Gentoo Mathematics Project + + + https://github.com/Boolector/btor2tools/issues/ + Boolector/btor2tools + + diff --git a/sci-mathematics/cadical/Manifest b/sci-mathematics/cadical/Manifest index 1fbc26daa231..67a34a024cd4 100644 --- a/sci-mathematics/cadical/Manifest +++ b/sci-mathematics/cadical/Manifest @@ -3,5 +3,5 @@ AUX cadical-makefile.in-ar.patch 323 BLAKE2B 226618745824824d8d7ccea53a3435abed9 DIST cadical-1.5.2.tar.gz 596334 BLAKE2B 2e6c0f0602b807cf9ee5993aa627e074291b0128d19474d5431e01992d66b111773e593c14712338e9702f64e23eae6fdd937b5b86b2b9b3e08022dbbb199fd7 SHA512 1aab87bdaec938eb219f75f13bf2fcb031f47ac1f49b586f769aeececd1c33b166341bef3bc8713e62b4612a91c405db33e6d1b48e1074a3433d80e9ecb33fe2 DIST cadical-1.5.3.tar.gz 596378 BLAKE2B 1ac27412745b0f24668ccf2ea1ff89e02c1e68137110bf9522a63ad82b14621d898d0bf873a651a24ccef9f502982f5e2d5b9c558ed0b1c5b7432c1a1459cb58 SHA512 bec811ab6a4c392506bdc391227d108476b5b5fae280b2d7d484429fe6d84e86206a054a1044cf68046ce183ecd7af3ec58f8be3ac27224fe37930cf43f08f3b EBUILD cadical-1.5.2-r1.ebuild 732 BLAKE2B f97142135bf5be3f3912d572235aa0de953ac4137e715b0b3732014c19527cb2a6a4fca456bdd5e48b9384038b1028fcaef8b47695ead65bff5ebdd17fc1d3ce SHA512 aed6e5bd0cda217c6b2a1c9a32dc27f0b0c5f051dcbf43a3e06e806e5a6099340a8d224027b77e6949b3ca3f053f1cd1676cf968d95c9a63636bbe18703e7f79 -EBUILD cadical-1.5.3.ebuild 787 BLAKE2B b4303e9b1636eabd5697e1dcf2111182ca297c7b7d76a64eddf03acef1dd9e3ce569cf1907282cb8511d74a54d4372f5fd67d1d8f1f2f9430fbb9ecb13d9cb70 SHA512 bb7d45d98a46b0a61ce0174a9d287c2fdd425dad7da90fd0f8c963aaf53cdd0aa8b617a9a7ae1ff817a44b39ea2e4ff951d17539dcc5958ad20cd5e24f60d929 +EBUILD cadical-1.5.3-r1.ebuild 813 BLAKE2B 028ee0555334e9f2a4e3a4c90cac3d85644592c69f5d44392212c941889ad24bb7e9b1f7bbe5a67e6efd370d1f9832300da57b16543c30d17e32786925c774b8 SHA512 1dc7b61c695804ae6348ff35b4047b9ad2bb26f3a63906d661dcf87b4e0a4ff5127228c9694d46377517ec2c27d04f2173a5f9e3f8582349e1b8662ff2f1cab6 MISC metadata.xml 613 BLAKE2B 6d7e0c1b5eae3803aa0981b195457cdcc6d2ffa2af655837e615da6ed6914ac5bec7a831ced6703ff67476561cf67139ea5519d98cdc2bd8d5781108496046e2 SHA512 b04ad6ae6e2626cea18049e3e20eb227b5580853b8ad77179ea693ed61f12d042b7ea505eb8cfafaa0121564ab0a4b6c7dcdf84f78fa2f47c465e6f61fb1a3f0 diff --git a/sci-mathematics/cadical/cadical-1.5.3-r1.ebuild b/sci-mathematics/cadical/cadical-1.5.3-r1.ebuild new file mode 100644 index 000000000000..63bd3bf453f3 --- /dev/null +++ b/sci-mathematics/cadical/cadical-1.5.3-r1.ebuild @@ -0,0 +1,37 @@ +# Copyright 1999-2023 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +inherit toolchain-funcs + +DESCRIPTION="Simplified Satisfiability Solver" +HOMEPAGE="http://fmv.jku.at/cadical/" +SRC_URI="https://github.com/arminbiere/${PN}/archive/rel-${PV}.tar.gz + -> ${P}.tar.gz" +S="${WORKDIR}"/${PN}-rel-${PV} + +LICENSE="MIT" +SLOT="0/${PV}" +KEYWORDS="~amd64 ~x86" + +PATCHES=( + "${FILESDIR}"/${PN}-configure.patch + "${FILESDIR}"/${PN}-makefile.in-ar.patch +) + +DOCS=( BUILD.md CONTRIBUTING NEWS.md README.md VERSION ) + +src_configure() { + tc-export AR + CXX="$(tc-getCXX)" CXXFLAGS="${CXXFLAGS} ${LDFLAGS}" ./configure || die +} + +src_install() { + exeinto /usr/bin + doexe build/{cadical,mobical} + dolib.a build/libcadical.a + doheader src/cadical.hpp + doheader src/ccadical.h + einstalldocs +} diff --git a/sci-mathematics/cadical/cadical-1.5.3.ebuild b/sci-mathematics/cadical/cadical-1.5.3.ebuild deleted file mode 100644 index dac39982db2e..000000000000 --- a/sci-mathematics/cadical/cadical-1.5.3.ebuild +++ /dev/null @@ -1,35 +0,0 @@ -# Copyright 1999-2022 Gentoo Authors -# Distributed under the terms of the GNU General Public License v2 - -EAPI=8 - -inherit toolchain-funcs - -DESCRIPTION="Simplified Satisfiability Solver" -HOMEPAGE="http://fmv.jku.at/cadical/" -SRC_URI="https://github.com/arminbiere/${PN}/archive/rel-${PV}.tar.gz -> ${P}.tar.gz" -S="${WORKDIR}"/${PN}-rel-${PV} - -LICENSE="MIT" -SLOT="0/${PV}" -KEYWORDS="~amd64 ~x86" - -PATCHES=( - "${FILESDIR}"/${PN}-configure.patch - "${FILESDIR}"/${PN}-makefile.in-ar.patch -) - -DOCS=( BUILD.md CONTRIBUTING NEWS.md README.md VERSION ) - -src_configure() { - tc-export AR - CXX="$(tc-getCXX)" CXXFLAGS="${CXXFLAGS} ${LDFLAGS}" ./configure || die -} - -src_install() { - exeinto /usr/bin - doexe build/{cadical,mobical} - dolib.a build/libcadical.a - doheader src/cadical.hpp - einstalldocs -} diff --git a/sci-mathematics/cubicle/Manifest b/sci-mathematics/cubicle/Manifest new file mode 100644 index 000000000000..aa9a2c6b901b --- /dev/null +++ b/sci-mathematics/cubicle/Manifest @@ -0,0 +1,4 @@ +AUX 50cubicle-gentoo.el 185 BLAKE2B 76ef002c52bd0d6ef8ce5474e5cf9032cffe861d273a88176c3a8eae17f6176896bc1a4cb099d1f793b63f1ad3e0b7fb6d4b066317f160a0a4fd586e0a61ec64 SHA512 c9a93fec3f1f12cbe326940a79dfe950b56c82e7bdd24a6bf5923d1c4fe6245b8fec4c399f3e60c16cc4757f290f9cbeab606a20b5844f4228a4f29b0ed669f4 +DIST cubicle-1.2.0.tar.gz 866004 BLAKE2B 4fd944acb394165396344b7a9d4b29ffcb7b61571e1ac9cb90aacf1a5ddb0521d399f301a51af6b37461e5a47244fb095ad69ab0041440c240257522ba4de4a7 SHA512 e2815b4b7b4feda30df91eabebae741d14a2c822f5efea972676bc7a941454ea368e9dc003f754c2edb1c6b1db5a5c86a354b3612c2d47a9095f8fc348dfb692 +EBUILD cubicle-1.2.0-r1.ebuild 1332 BLAKE2B 7dbbb9ed042dd4ecabb00ee3ccc050e39174b01e7131f90b6bbd5dde249299071e30eee3f2cfd5576f8504b7a3f27ab1430428935b4012e0da69c8cbc67409b7 SHA512 a9018679ffa0b2481fd3629518317e8ceab2494d66d1688e1a95ff41b73964a62f17b4d2c6e2ad17e130c09e93b84bb1d23f360e5eebdb8f6f87f154a4069f9d +MISC metadata.xml 1503 BLAKE2B d67f3f6524234cf3be4b0118aced6f4e3424a25754d91b13eb5c8250aedb6a57a6f7faabe6539875953874f48b2d8349fe3adfe431b72675fdd6723cb9ff3c52 SHA512 96540a56c6ef839924fa93f49e4ffdeb8a5eb3b83ef43bd62ccbed72dfa522f1b0acad4132650f67387915af5be8fe432fd6d01f8c9a76271c53f7f3a33f476d diff --git a/sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild b/sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild new file mode 100644 index 000000000000..8159f9f60a4a --- /dev/null +++ b/sci-mathematics/cubicle/cubicle-1.2.0-r1.ebuild @@ -0,0 +1,71 @@ +# Copyright 1999-2023 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +inherit autotools elisp-common + +DESCRIPTION="Model checker for verifying properties of array-based systems" +HOMEPAGE="https://cubicle.lri.fr/ + https://github.com/cubicle-model-checker/cubicle/" +SRC_URI="https://github.com/cubicle-model-checker/${PN}/archive/${PV}.tar.gz + -> ${P}.tar.gz" + +LICENSE="Apache-2.0" +SLOT="0/${PV}" +KEYWORDS="~amd64 ~x86" +IUSE="emacs examples ocamlopt" + +RDEPEND=" + >=dev-lang/ocaml-4.09.0:=[ocamlopt=] + dev-ml/num:= + emacs? ( >=app-editors/emacs-23.1:* ) +" +DEPEND="${RDEPEND}" +BDEPEND=" + dev-ml/findlib + sys-apps/gawk +" + +SITEFILE="50${PN}-gentoo.el" + +src_prepare() { + default + eautoreconf + + # Makefile checks if "configure.in" exists, + # it is needed by the ".depend" target. + ln -s configure.ac configure.in || die +} + +src_configure() { + econf --without-z3 # Needs Z3 Ocaml bindings, not yet packaged. +} + +src_compile() { + default + + if use emacs ; then + elisp-compile emacs/*.el + fi +} + +src_install() { + default + + doman doc/${PN}.1 + + if use emacs ; then + elisp-install ${PN} emacs/*.el{,c} + elisp-site-file-install "${FILESDIR}/${SITEFILE}" + fi + use examples && dodoc -r examples +} + +pkg_postinst() { + use emacs && elisp-site-regen +} + +pkg_postrm() { + use emacs && elisp-site-regen +} diff --git a/sci-mathematics/cubicle/files/50cubicle-gentoo.el b/sci-mathematics/cubicle/files/50cubicle-gentoo.el new file mode 100644 index 000000000000..bab0f0d76325 --- /dev/null +++ b/sci-mathematics/cubicle/files/50cubicle-gentoo.el @@ -0,0 +1,4 @@ +(add-to-list 'load-path "@SITELISP@") +(autoload 'cubicle-mode "cubicle-mode" + "A major mode for editing Cubicle files." t) +(add-to-list 'auto-mode-alist '("\\.cub\\'" . cubicle-mode)) diff --git a/sci-mathematics/cubicle/metadata.xml b/sci-mathematics/cubicle/metadata.xml new file mode 100644 index 000000000000..d3a0058bc0c9 --- /dev/null +++ b/sci-mathematics/cubicle/metadata.xml @@ -0,0 +1,31 @@ + + + + + + ml@gentoo.org + ML + + + sci-mathematics@gentoo.org + Gentoo Mathematics Project + + + Cubicle is an open source model checker for verifying safety properties of + array-based systems. This is a syntactically restricted class of + parametrized transition systems with states represented as arrays indexed + by an arbitrary number of processes. Cache coherence protocols and mutual + exclusion algorithms are typical examples of such systems. Cubicle + model-checks by a symbolic backward reachability analysis on infinite sets + of states represented by specific simple formulas, called cubes. Cubicle is + based on ideas introduced by MCMT from which, in addition to revealing the + implementation details, it differs in a more friendly input language and a + concurrent architecture. Cubicle is written in OCaml. Its SMT solver is a + tightly integrated, lightweight and enhanced version of Alt-Ergo; and its + parallel implementation relies on the Functory library. + + + https://github.com/cubicle-model-checker/cubicle/issues/ + cubicle-model-checker/cubicle + + diff --git a/sci-mathematics/picosat/Manifest b/sci-mathematics/picosat/Manifest index d2426840a5b1..cbf04723294e 100644 --- a/sci-mathematics/picosat/Manifest +++ b/sci-mathematics/picosat/Manifest @@ -1,4 +1,4 @@ AUX picosat-965-makefile.in.patch 364 BLAKE2B fd6d9ade8e918dd8c9a16ced81a8f47a6ba2b64c7b262a385b0637092beaac4adcc0886506b49c5b21131a550f332b170bc4cc456696d99b7404aa8c11d37018 SHA512 950bddde2363c5b0e36c2333201fbfee54229674f9051f3c4f45023f4364a3bdca3cdaf6b083eed7c9a59c4de0ab92c0eb748092c6cba4c9dba5da6146d6b90f DIST picosat-965.tar.gz 64386 BLAKE2B 913b08a72c0b15065353c2ee1ff8fe5a9c0f7a2a8653d80f4cdcee8fdcf69eed7621e28f4259a9d0fb506fefb8eccfd293f06aa7c1b3ea3f6cc31eb319a30532 SHA512 b5372962a0079d70641fd76c431b4ab5042c2f3015179762e447634f220cf0744eea786ee40b00035a342f3ead482061ebe1a9e3726bd06e7adf8e0ac0c5eabf -EBUILD picosat-965.ebuild 756 BLAKE2B e9f78bc57ecb6098b4adf42604c953d7ceff70d50c5cb6c2050efc6c7bed971f831c48a037b79411d501b9d6c63b6f12020b63ae0968b7cc219261b128bf9d47 SHA512 a567120a954bd949c3550bf765187624b6403befef00f5d1b4fa98a45b1f51f7159d2c8d1e366d38898651cec0600e5759e43988a5365eb70b4363bb87336199 +EBUILD picosat-965-r1.ebuild 778 BLAKE2B 1bbc097e9d473e4f7924ecf9a867481c6d3b845e8386e6d5bebbf2c761b7d985f077ac12e6b5b0b50e761daa6be9be1c1d8ede80e9d16ecf795e333e1988cd49 SHA512 9d446c871c701798b8b5cff7261bd817103775968fe885293112d782e135b94f2cbaa4e41307bc0379916d52a1618ad6303daadd47c6a7c6c6e2ab16657bdba1 MISC metadata.xml 277 BLAKE2B 3d5dbdb3275e5d5623299c686ddb7ce896215621e87d688814bc03d383eeec180594639627ed7b8ac903fba49120507407c9e53813401c797c67a2da8330ef02 SHA512 f7b11642db7488b1cc11d3a5602fc18985a0e050502a332ed6850e123c51d3cad21790c09e032454c7590b61d4718cd91bde453c1ec00baaedea90ee9f57882c diff --git a/sci-mathematics/picosat/picosat-965-r1.ebuild b/sci-mathematics/picosat/picosat-965-r1.ebuild new file mode 100644 index 000000000000..30e893f62288 --- /dev/null +++ b/sci-mathematics/picosat/picosat-965-r1.ebuild @@ -0,0 +1,39 @@ +# Copyright 1999-2023 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +inherit toolchain-funcs + +DESCRIPTION="SAT solver with proof and core support" +HOMEPAGE="http://fmv.jku.at/picosat/" +SRC_URI="http://fmv.jku.at/${PN}/${P}.tar.gz" + +SLOT="0" +KEYWORDS="~amd64 ~x86" +LICENSE="MIT" + +PATCHES=( "${FILESDIR}"/${P}-makefile.in.patch ) + +src_configure() { + CC="$(tc-getCC)" sh ./configure.sh --shared --trace || die +} + +src_compile() { + emake AR="$(tc-getAR)" RANLIB="$(tc-getRANLIB)" \ + CFLAGS="${CFLAGS} ${LDFLAGS} -fPIC" +} + +src_install() { + exeinto /usr/bin + doexe picomus picomcs picosat picogcnf + + insinto /usr/share + newins VERSION picosat.version + + dolib.a libpicosat.a + dolib.so libpicosat.so + doheader picosat.h + + dodoc NEWS README +} diff --git a/sci-mathematics/picosat/picosat-965.ebuild b/sci-mathematics/picosat/picosat-965.ebuild deleted file mode 100644 index 9803703a619b..000000000000 --- a/sci-mathematics/picosat/picosat-965.ebuild +++ /dev/null @@ -1,38 +0,0 @@ -# Copyright 1999-2022 Gentoo Authors -# Distributed under the terms of the GNU General Public License v2 - -EAPI=8 - -inherit toolchain-funcs - -DESCRIPTION="SAT solver with proof and core support" -HOMEPAGE="http://fmv.jku.at/picosat/" -SRC_URI="http://fmv.jku.at/${PN}/${P}.tar.gz" - -SLOT="0" -KEYWORDS="~amd64 ~x86" -LICENSE="MIT" - -PATCHES=( "${FILESDIR}"/${P}-makefile.in.patch ) - -src_configure() { - CC="$(tc-getCC)" sh ./configure.sh --shared --trace || die -} - -src_compile() { - emake AR="$(tc-getAR)" RANLIB="$(tc-getRANLIB)" \ - CFLAGS="${CFLAGS} ${LDFLAGS} -fPIC" -} - -src_install() { - exeinto /usr/bin - doexe picomus picomcs picosat picogcnf - - insinto /usr/share - newins VERSION picosat.version - - dolib.so libpicosat.so - doheader picosat.h - - dodoc NEWS README -} diff --git a/sci-mathematics/singular/Manifest b/sci-mathematics/singular/Manifest index e08a451c39ba..29648303b20d 100644 --- a/sci-mathematics/singular/Manifest +++ b/sci-mathematics/singular/Manifest @@ -1,6 +1,6 @@ AUX 60singular-gentoo.el 298 BLAKE2B 5b42e2083037e2ff2ace5597ddebfb079920e09ed91d1a359e058fc654c6778456174d6cee9242f7fcaf81bf1464f47f43604b9e4eb298f051c6a4daba4630ca SHA512 4c17a25d91c085e12f26441fcde858e61bf191bd7d9dcf63ff5b5a1dce1d63e3f7c4f78ce8afa4f2359ad4ba6eb51f3e224ae6c502b18f5f7a76738534337431 DIST singular-4.3.1p1.tar.gz 15090370 BLAKE2B d4e40378b3892b98b1f78c3928c8a40484336ea25ea4dcd4b3a1e5f651281d2cdb06d92c9cc64427ce76e91c5bf4eaa1c3b643df174a24c188823ae808817ad9 SHA512 d27d8e042ea085e49aed6a0697056c36e78e62ea0b9d17751cdf4c556cf4f6efce3b34b411c77aef97c6d90675bea11c97651eb7009634cb8a9b630ec820a06e -DIST singular-4.3.1p2.tar.gz 15088650 BLAKE2B 17d73518653f6348297c955214aa8d30b3ce7cdf342f1bbb6fb49b746ddc563b1f46906df92f45abd601c834c77139f7aaccadf14bf706010017564d56948ca2 SHA512 ff2282b2fcd1a5b8809297036d524838403a2b66ae87ceb566ed6ff0571843d3c4aa0f7a4abbaab8541630f4e0130b6171ea0a7b8a5296b3b10f6c5cd5088828 +DIST singular-4.3.1p3.tar.gz 14991986 BLAKE2B 0ae2585a362839914d3a134bfe637f6faa34d95f58937f2adcca0c5a35e3218eb36554bae8187f5bb3a423dcac445c836e9bfff2d0d1a19d4e14a4452b84d839 SHA512 f092683f4a92158d82a2e694f284662c6285bac5faaa7d5e5695a84a220012fb8a733b4bbc52820def3037e1596ea4c2ab3846f58a3a3fb19e01bf7595790462 EBUILD singular-4.3.1_p1.ebuild 2294 BLAKE2B 1147387c35f31d8bef97c67ec8d4596952494c85d8dd0c427981c7d491200fb3eb02658f3f63fde4e8323e1cc0f9ccbb467ae73ba17bbba12a05831b12f35348 SHA512 2d0c8047da3d2940f7ada1f68f314b7499a497dce09d7166f866f62bd67ab315df7bca5e90af07f897839ceb288651dd6be347a1ecceaa8ce6177f9a30df72d9 -EBUILD singular-4.3.1_p2.ebuild 2300 BLAKE2B d55b7cf13d0fbdd2d61f52237b709ffa470b955e256563b525a30929eeed12fe321b9f7935616d300d3e313e07bdebe62995c34b9586391cff70304f42915297 SHA512 dd7be599866c801ed2303319061f325f8052a8041b280d0815902cdc9f75fc88be5d1187ff4c4785716bd62eff8e480adf4c5a1bacfdab2711f05471e47a50b9 +EBUILD singular-4.3.1_p3.ebuild 2300 BLAKE2B 8335c3d556cb98834fa9f8f9a5287954b62444a30f3d6e4c5602b425f03d2646fe8fafe922bf41a0e978104e6cf424e4c5afbaf9263758a38b2e7931398a4362 SHA512 2beceeec3f73e1ef4fe470642d170eb4a0dce7d737dfb9453ca7cb1ab0283ab9199cb01a490487580ebb9a4f57f74ccc7c3742ddae6fe776396dee92ab648d3f MISC metadata.xml 782 BLAKE2B 7f10704c78b5a55cff9d07ffc3456a57aba4001ffd337dfbbb712e32608446ab9ae8039d14143939ad41710dcc6d4725992db2c80bcd1678397e563fefa929b4 SHA512 3c4904a4a8f63ff073745409caf9a9a68aa5d46861b8e8d77a538716a7a6a099d87137d604e52a3b8ce4ab81b7333f95389cd888ccbabe52017b6e8b1e4a77d0 diff --git a/sci-mathematics/singular/singular-4.3.1_p2.ebuild b/sci-mathematics/singular/singular-4.3.1_p2.ebuild deleted file mode 100644 index 810f2e71b223..000000000000 --- a/sci-mathematics/singular/singular-4.3.1_p2.ebuild +++ /dev/null @@ -1,103 +0,0 @@ -# Copyright 1999-2022 Gentoo Authors -# Distributed under the terms of the GNU General Public License v2 - -EAPI=8 - -inherit elisp-common - -MY_PN=Singular -MY_PV=$(ver_rs 3 '') -# Consistency is different... -MY_DIR2=$(ver_cut 1-3 ${PV}) -MY_DIR=$(ver_rs 1- '-' ${MY_DIR2}) - -DESCRIPTION="Computer algebra system for polynomial computations" -HOMEPAGE="https://www.singular.uni-kl.de/ https://github.com/Singular/Singular" -SRC_URI="https://www.singular.uni-kl.de/ftp/pub/Math/${MY_PN}/SOURCES/${MY_DIR}/${PN}-${MY_PV}.tar.gz" -S="${WORKDIR}/${PN}-${MY_DIR2}" - -LICENSE="BSD GPL-2 GPL-3" -SLOT="0" -KEYWORDS="~amd64 ~ppc ~riscv ~x86 ~x86-linux" -IUSE="emacs examples polymake +readline static-libs" - -RDEPEND=" - dev-lang/perl - dev-libs/gmp:0 - dev-libs/ntl:= - sci-libs/cddlib - sci-mathematics/flint - emacs? ( >=app-editors/emacs-23.1:* ) - polymake? ( sci-mathematics/polymake ) - readline? ( sys-libs/readline ) -" -DEPEND="${RDEPEND}" - -SITEFILE=60${PN}-gentoo.el - -src_configure() { - local myconf=( - --disable-debug - --disable-doc - --disable-optimizationflags - --disable-pyobject-module - --disable-python - --disable-python-module - --disable-python_module - --enable-factory - --enable-gfanlib - --enable-libfac - --with-flint - --with-gmp - --with-libparse - --with-ntl - --without-python - --without-pythonmodule - $(use_enable emacs) - $(use_enable polymake polymake-module) - $(use_enable static-libs static) - $(use_with readline) - ) - econf "${myconf[@]}" -} - -src_compile() { - default - - if use emacs; then - pushd "${S}"/emacs - elisp-compile *.el || die "elisp-compile failed" - popd - fi -} - -src_install() { - # Do not compress singular's info file (singular.hlp) - # some consumer of that file do not know how to deal with compression - docompress -x /usr/share/info - - default - - dosym Singular /usr/bin/"${PN}" - - # purge .la file - find "${ED}" -name '*.la' -delete || die -} - -src_test() { - # SINGULAR_PROCS_DIR need to be set to "" otherwise plugins from - # an already installed version of singular may be used and cause segfault - # See https://github.com/Singular/Sources/issues/980 - SINGULAR_PROCS_DIR="" emake check -} - -pkg_postinst() { - einfo "Additional functionality can be enabled by installing" - einfo "sci-mathematics/4ti2" - - use emacs && elisp-site-regen -} - -pkg_postrm() { - use emacs && elisp-site-regen -} diff --git a/sci-mathematics/singular/singular-4.3.1_p3.ebuild b/sci-mathematics/singular/singular-4.3.1_p3.ebuild new file mode 100644 index 000000000000..b51070f29cc5 --- /dev/null +++ b/sci-mathematics/singular/singular-4.3.1_p3.ebuild @@ -0,0 +1,103 @@ +# Copyright 1999-2023 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +inherit elisp-common + +MY_PN=Singular +MY_PV=$(ver_rs 3 '') +# Consistency is different... +MY_DIR2=$(ver_cut 1-3 ${PV}) +MY_DIR=$(ver_rs 1- '-' ${MY_DIR2}) + +DESCRIPTION="Computer algebra system for polynomial computations" +HOMEPAGE="https://www.singular.uni-kl.de/ https://github.com/Singular/Singular" +SRC_URI="https://www.singular.uni-kl.de/ftp/pub/Math/${MY_PN}/SOURCES/${MY_DIR}/${PN}-${MY_PV}.tar.gz" +S="${WORKDIR}/${PN}-${MY_DIR2}" + +LICENSE="BSD GPL-2 GPL-3" +SLOT="0" +KEYWORDS="~amd64 ~ppc ~riscv ~x86 ~x86-linux" +IUSE="emacs examples polymake +readline static-libs" + +RDEPEND=" + dev-lang/perl + dev-libs/gmp:0 + dev-libs/ntl:= + sci-libs/cddlib + sci-mathematics/flint + emacs? ( >=app-editors/emacs-23.1:* ) + polymake? ( sci-mathematics/polymake ) + readline? ( sys-libs/readline ) +" +DEPEND="${RDEPEND}" + +SITEFILE=60${PN}-gentoo.el + +src_configure() { + local myconf=( + --disable-debug + --disable-doc + --disable-optimizationflags + --disable-pyobject-module + --disable-python + --disable-python-module + --disable-python_module + --enable-factory + --enable-gfanlib + --enable-libfac + --with-flint + --with-gmp + --with-libparse + --with-ntl + --without-python + --without-pythonmodule + $(use_enable emacs) + $(use_enable polymake polymake-module) + $(use_enable static-libs static) + $(use_with readline) + ) + econf "${myconf[@]}" +} + +src_compile() { + default + + if use emacs; then + pushd "${S}"/emacs + elisp-compile *.el || die "elisp-compile failed" + popd + fi +} + +src_install() { + # Do not compress singular's info file (singular.hlp) + # some consumer of that file do not know how to deal with compression + docompress -x /usr/share/info + + default + + dosym Singular /usr/bin/"${PN}" + + # purge .la file + find "${ED}" -name '*.la' -delete || die +} + +src_test() { + # SINGULAR_PROCS_DIR need to be set to "" otherwise plugins from + # an already installed version of singular may be used and cause segfault + # See https://github.com/Singular/Sources/issues/980 + SINGULAR_PROCS_DIR="" emake check +} + +pkg_postinst() { + einfo "Additional functionality can be enabled by installing" + einfo "sci-mathematics/4ti2" + + use emacs && elisp-site-regen +} + +pkg_postrm() { + use emacs && elisp-site-regen +} -- cgit v1.2.3