From 2c4057102db258a197f73df9e1286833f2db8eef Mon Sep 17 00:00:00 2001 From: Stefan Huber Date: Mon, 17 Aug 2026 22:38:03 +0200 Subject: [PATCH] sci-mathematics: remove boolector and lingeling --- sci-mathematics/boolector/Manifest | 4 -- .../boolector/boolector-1.5.116.ebuild | 34 ---------- .../boolector/files/pathfixes.patch | 68 ------------------- sci-mathematics/boolector/metadata.xml | 8 --- sci-mathematics/lingeling/Manifest | 3 - .../lingeling/lingeling-1212013.ebuild | 29 -------- sci-mathematics/lingeling/metadata.xml | 8 --- 7 files changed, 154 deletions(-) delete mode 100644 sci-mathematics/boolector/Manifest delete mode 100644 sci-mathematics/boolector/boolector-1.5.116.ebuild delete mode 100644 sci-mathematics/boolector/files/pathfixes.patch delete mode 100644 sci-mathematics/boolector/metadata.xml delete mode 100644 sci-mathematics/lingeling/Manifest delete mode 100644 sci-mathematics/lingeling/lingeling-1212013.ebuild delete mode 100644 sci-mathematics/lingeling/metadata.xml diff --git a/sci-mathematics/boolector/Manifest b/sci-mathematics/boolector/Manifest deleted file mode 100644 index 1b33888..0000000 --- a/sci-mathematics/boolector/Manifest +++ /dev/null @@ -1,4 +0,0 @@ -AUX pathfixes.patch 1613 BLAKE2B 54d1c9723e33f58d77f0534918397b5257384b804242571099e94ce3e18b29460c2f8f15d841ca6b236064b3556166d29453185630f7ba6d0dc9aeed625cfcd0 SHA512 7efd68a0ab531a165727626c506f289b4181adca399c7f8dcf05ddbd1e41947df19eb48ef26bd7d9b0b6a0865a49711119caac53da9d4d0870572fdb4b0878fb -DIST boolector-1.5.116-eeaf10b-121004.tar.gz 187600 BLAKE2B 613c23f63f07575900da3bd9522c12b9b55ffdb4b36ca9146d34ae0b06bf9b1a1f539682e6d362abd8b78a7800ae5d0e2a382252756a351c5f17c93f0261d993 SHA512 e38399280d2fa799b17f956adb21f53187e2a6e25ae09cc52403929e7cdc1ef7dce28b19eb27f5f3faaaba7e99c67c0ce0727979b467c04617da80d73a44c217 -EBUILD boolector-1.5.116.ebuild 728 BLAKE2B 9cde12f7f7ec0ddc1e0f02d362c4210fc3712665cd8635ffb2ed6d22639ac02329c38f401c574cfde230ad65e5eb5b36cd31526e23759721b62087f370323ab6 SHA512 d8df094d7de1bb3a75494a13bc18b7d59bde5e182883c28bb0a33bb10a68a80f25c1d0a940500ee7d8a64ce3dcdd4c1c8fc5ace5d3e12b880babb2781b0ea44a -MISC metadata.xml 243 BLAKE2B 889d08efb220a9fb8457500f5f3c33c8c737616995e19fa8b621ced4bc9d380d016413d098d4d09925c679cd23f7fbd75e495424fe6ed809a9e873014caae682 SHA512 f9051a65d7e11d7abd1b9568dbbf8be84a6ae68eb994b0c22d57dff5620047d5ad5a324057a5cf4cec10837d16024e5f21a8cf5f1a6247807f62931839eb73bc diff --git a/sci-mathematics/boolector/boolector-1.5.116.ebuild b/sci-mathematics/boolector/boolector-1.5.116.ebuild deleted file mode 100644 index e361367..0000000 --- a/sci-mathematics/boolector/boolector-1.5.116.ebuild +++ /dev/null @@ -1,34 +0,0 @@ -# Copyright 1999-2013 Gentoo Foundation -# Distributed under the terms of the GNU General Public License v2 -# $Header: $ - -EAPI=8 - -DESCRIPTION="Boolector is an SMT solver for bit-vectors and arrays" -HOMEPAGE="http://fmv.jku.at/boolector/" -SRC_URI="http://fmv.jku.at/boolector/boolector-1.5.116-eeaf10b-121004.tar.gz" -S=${WORKDIR}/boolector-1.5.116-eeaf10b-121004 - -LICENSE="boolector" -SLOT="0" -KEYWORDS="~x86 ~amd64" -IUSE="" - -DEPEND=" - sci-mathematics/lingeling" -RDEPEND="${DEPEND}" - -src_prepare() { - epatch ${FILESDIR}/pathfixes.patch -} - -src_configure() { - ./configure --lingeling --no-picosat --no-minisat -} - -src_install() { - dodoc NEWS VERSION - dobin boolector synthebtor deltabtor - dolib libboolector.a - doheader boolector.h -} diff --git a/sci-mathematics/boolector/files/pathfixes.patch b/sci-mathematics/boolector/files/pathfixes.patch deleted file mode 100644 index a378fd4..0000000 --- a/sci-mathematics/boolector/files/pathfixes.patch +++ /dev/null @@ -1,68 +0,0 @@ -diff --git a/btorexp.c b/btorexp.c -index fe2bddf..0d9edd6 100644 ---- a/btorexp.c -+++ b/btorexp.c -@@ -8267,7 +8267,7 @@ BTOR_SPLIT_SLICES_RESTART: - #ifndef BTOR_DO_NOT_PROCESS_SKELETON - /*------------------------------------------------------------------------*/ - --#include "../lingeling/lglib.h" -+#include - - static int - btor_fixed_exp (Btor * btor, BtorNode * exp) -diff --git a/btorsat.c b/btorsat.c -index 611c616..b54e4a6 100644 ---- a/btorsat.c -+++ b/btorsat.c -@@ -14,7 +14,7 @@ - #endif - - #ifdef BTOR_USE_LINGELING --#include "../lingeling/lglib.h" -+#include - #endif - - #ifdef BTOR_USE_MINISAT -diff --git a/configure b/configure -index 13b1ffe..a6a1305 100755 ---- a/configure -+++ b/configure -@@ -179,36 +179,13 @@ then - msg "not using Lingeling as requested by command line option" - else - -- if [ -d ../lingeling ] -- then -- for path in ../lingeling/lglib.h ../lingeling/liblgl.a allfound -- do -- [ -f $path ] || break -- done -- else -- path=../lingeling -- fi -- -- if [ $path = allfound ] -- then -- msg "using Lingeling in '../lingeling'" -- lingeling=yes -- elif [ $lingeling = yes ] -- then -- die "impossible to use Lingeling: '$path' missing" -- else -- msg "disabling Lingeling: '$path' missing" -- lingeling=no -- fi -- - if [ $lingeling = yes ] - then - [ X"$CFLAGS" = X ] || CFLAGS="$CFLAGS " - [ X"$LDEPS" = X ] || LDEPS="$LDEPS " - [ X"$LIBS" = X ] || LIBS="$LIBS " - CFLAGS="${CFLAGS}-DBTOR_USE_LINGELING" -- LIBS="${LIBS}-L../lingeling -llgl" -- LDEPS="${LDEPS}../lingeling/liblgl.a" -+ LIBS="${LIBS} -llgl" - LIBM=yes - fi - diff --git a/sci-mathematics/boolector/metadata.xml b/sci-mathematics/boolector/metadata.xml deleted file mode 100644 index 9434230..0000000 --- a/sci-mathematics/boolector/metadata.xml +++ /dev/null @@ -1,8 +0,0 @@ - - - - - shuber@sthu.org - Stefan Huber - - diff --git a/sci-mathematics/lingeling/Manifest b/sci-mathematics/lingeling/Manifest deleted file mode 100644 index 1c1077c..0000000 --- a/sci-mathematics/lingeling/Manifest +++ /dev/null @@ -1,3 +0,0 @@ -DIST lingeling-ala-b02aa1a-121013.tar.gz 166291 BLAKE2B e9b824832559b16c50cea3d7857bced6d07432da9f16ac9e1128c6c40d69e2c0989d22aeb0cb27fad44ab815c6869094715fcbfb2dfbcb55e39cb23ea63532ef SHA512 b7ad6cedef5ebcd03d798ae6b379a10077c657172932a6124a6972d70e87be428148d0a47ba91a67a78a0d413a0de0a13fd3cd1687a04d98434160f27ae9089e -EBUILD lingeling-1212013.ebuild 576 BLAKE2B ee3d8f4ff294e3ca006b7f1e9461dba200b74a1462d5fcb4d04df1c50070a23afc54e57849189a3646800bbce47c4626f8c9388fb03ad83f43285f16b2d6095c SHA512 74c187b7f253a78aa074c2b412605620f2774e2378cc3cd1af60784a09f15de1b76278270f8c8a3a28ae7d1c91d97a8dcc60ff6263230d2ff75535d6639b050d -MISC metadata.xml 243 BLAKE2B 889d08efb220a9fb8457500f5f3c33c8c737616995e19fa8b621ced4bc9d380d016413d098d4d09925c679cd23f7fbd75e495424fe6ed809a9e873014caae682 SHA512 f9051a65d7e11d7abd1b9568dbbf8be84a6ae68eb994b0c22d57dff5620047d5ad5a324057a5cf4cec10837d16024e5f21a8cf5f1a6247807f62931839eb73bc diff --git a/sci-mathematics/lingeling/lingeling-1212013.ebuild b/sci-mathematics/lingeling/lingeling-1212013.ebuild deleted file mode 100644 index a46d955..0000000 --- a/sci-mathematics/lingeling/lingeling-1212013.ebuild +++ /dev/null @@ -1,29 +0,0 @@ -# Copyright 1999-2013 Gentoo Foundation -# Distributed under the terms of the GNU General Public License v2 -# $Header: $ - -EAPI=8 - -DESCRIPTION="A SAT (boolean satisfiability) solver" -HOMEPAGE="http://fmv.jku.at/lingeling/" -SRC_URI="http://fmv.jku.at/lingeling/lingeling-ala-b02aa1a-121013.tar.gz" -S=${WORKDIR}/lingeling-ala-b02aa1a-121013 - -LICENSE="GPL" -SLOT="0" -KEYWORDS="~x86 ~amd64" -IUSE="" - -DEPEND="" -RDEPEND="${DEPEND}" - -src_configure() { - ./configure || die -} - -src_install() { - dodoc NEWS VERSION - dobin lingeling ilingeling plingeling - dolib liblgl.a - doheader lglib.h -} diff --git a/sci-mathematics/lingeling/metadata.xml b/sci-mathematics/lingeling/metadata.xml deleted file mode 100644 index 9434230..0000000 --- a/sci-mathematics/lingeling/metadata.xml +++ /dev/null @@ -1,8 +0,0 @@ - - - - - shuber@sthu.org - Stefan Huber - - -- 2.39.5