9 files changed, 133 insertions, 221 deletions
diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index a65fc5431f6b..468d0be07d9b 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
diff --git a/sci-mathematics/acl2/Manifest b/sci-mathematics/acl2/Manifest
new file mode 100644
index 000000000000..14113f3e630d
--- /dev/null
+++ b/sci-mathematics/acl2/Manifest
@@ -0,0 +1,4 @@
+AUX 50acl2-gentoo.el 230 BLAKE2B 42394e3aa3c8925a09ae331c0e133ebe0eb917991301172a50630b53c80dfda75629e8bc1ae4e9f844b5ab606ffbe0ffd70778c8066f4da386f8dad10ccee7ab SHA512 8b367c76497e50284f11606e7660148b78f069fa474bfaae49de4ac9649e524da1902b61a28ea50223d53582fe76485a8c2b26ca8b698005b2dd47cadcf99828
+DIST acl2-8.5.tar.gz 222696244 BLAKE2B e5aa8360d9f94ed398d11c4e0873818f8f49ed0e072192c7d62dde99b4a7f98b4240b352818e7691ebc98f85ab3c10981c36bb1e35317e50a111c9c7f3f57b33 SHA512 5a2e004713350ae41ced830aa8620c27963eb108baa499f7e52a1c60961b220ef7a026efdfef6cea1063f731b50f3cccbe1583a9957c9cf269b0a958ec83fe48
+EBUILD acl2-8.5.ebuild 2144 BLAKE2B 5952da8e09626d4e087783cdc2311b0485d50052c4f43e8b1046ed8ad2770c38404c0246c69b397df124d0f77385882b6b819dcf6aabaea669c462dbec46af21 SHA512 fa27d6da48e6dfaa9122cc7c9429a95af08511e00dae889f45beeb7ffd071ba251d372e2f07cfe2b6984388f0a503f828d54e8e502ed880ecbf53493a6f9e6ee
+MISC metadata.xml 816 BLAKE2B 791aff8f16b043469eb568aa6d50c2dabb2ffc3686ee846e98fd8f6e48533f5e4f86d500d8065a3a91cfce767c4990aabaf437eb97e57f8deabe19a6b9248116 SHA512 42a005fb8d3831cc422fed00a18419b959d40c3ee25a437efbfb836d9cb008fe22390a1986b090261c735fc0ff18688331ef884ee892703b166807616b947e64
diff --git a/sci-mathematics/acl2/acl2-8.5.ebuild b/sci-mathematics/acl2/acl2-8.5.ebuild
new file mode 100644
index 000000000000..bea58cd4e997
--- /dev/null
+++ b/sci-mathematics/acl2/acl2-8.5.ebuild
@@ -0,0 +1,92 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+# NOTICE: Only SBCL (dev-lisp/sbcl) is tested for now, but probably
+#   more CL implementations can be added as alternative dependencies.
+#   With ClozureCL (dev-lisp/clozurecl) ACL2 fails to build,
+#   this might need in-depth investigation...
+
+EAPI=8
+
+inherit elisp-common
+
+DESCRIPTION="Industrial strength theorem prover, logic and programming language"
+HOMEPAGE="https://www.cs.utexas.edu/users/moore/acl2/
+	https://github.com/acl2/acl2/"
+SRC_URI="https://github.com/acl2/acl2/archive/${PV}/${P}.tar.gz"
+
+SLOT="0"
+LICENSE="BSD"
+KEYWORDS="~amd64 ~x86"
+IUSE="doc emacs"
+REQUIRED_USE="emacs? ( doc )"
+
+RDEPEND="
+	dev-lisp/sbcl
+	emacs? ( >=app-editors/emacs-25:* )
+"
+BDEPEND="
+	${RDEPEND}
+	doc? ( dev-lang/perl )
+"
+
+DOCS=( books/README.md )
+SITEFILE="50${PN}-gentoo.el"
+
+src_prepare() {
+	find . -type f -name "*.bak" -delete || die
+	find . -type f -name "*.orig" -delete || die
+	rm books/workshops/2003/schmaltz-al-sammane-et-al/support/acl2link || die
+
+	default
+}
+
+src_compile() {
+	emake LISP="sbcl --no-sysinit --no-userinit --disable-debugger"
+
+	use doc && emake ACL2="${S}"/saved_acl2 basic DOC
+
+	if use emacs ; then
+		local elisp_dir
+		for elisp_dir in books/emacs books/interface/emacs ; do
+			BYTECOMPFLAGS="-L ${S}/${elisp_dir}"        \
+				elisp-compile "${S}"/${elisp_dir}/*.el
+		done
+	fi
+}
+
+src_install() {
+	local saved_name=saved_acl2
+
+	sed "s|${S}|/usr/share/acl2|g" -i ${saved_name} || die
+	sed "5iexport ACL2_SYSTEM_BOOKS=/usr/share/acl2/books/"    \
+		-i ${saved_name} || die
+
+	exeinto /usr/share/acl2
+	doexe ${saved_name}
+	insinto /usr/share/acl2
+	doins ${saved_name}.core
+	doins TAGS
+	dosym -r /usr/share/acl2/${saved_name} /usr/bin/acl2
+
+	if use doc ; then
+		doins -r books
+
+		HTML_DOCS=( doc/HTML/. )
+		einstalldocs
+	fi
+	if use emacs ; then
+		elisp-install ${PN}                     \
+			books/emacs/*.el{,c}                \
+			books/interface/emacs/*.el{,c}
+		elisp-site-file-install "${FILESDIR}/${SITEFILE}"
+	fi
+}
+
+pkg_postinst() {
+	use emacs && elisp-site-regen
+}
+
+pkg_postrm() {
+	use emacs && elisp-site-regen
+}
diff --git a/sci-mathematics/acl2/files/50acl2-gentoo.el b/sci-mathematics/acl2/files/50acl2-gentoo.el
new file mode 100644
index 000000000000..d61224e84506
--- /dev/null
+++ b/sci-mathematics/acl2/files/50acl2-gentoo.el
@@ -0,0 +1,6 @@
+(add-to-list 'load-path "@SITELISP@")
+(defvar *acl2-sources-dir* "/usr/share/acl2/")
+(autoload 'inferior-acl2 "inf-acl2.el"
+  "Run an inferior Acl2 process" t)
+(autoload 'run-acl2 "inf-acl2.el"
+  "Run an inferior Acl2 process" t)
diff --git a/sci-mathematics/acl2/metadata.xml b/sci-mathematics/acl2/metadata.xml
new file mode 100644
index 000000000000..df9ae811037d
--- /dev/null
+++ b/sci-mathematics/acl2/metadata.xml
@@ -0,0 +1,20 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</email>
+    <name>Gentoo Mathematics Project</name>
+  </maintainer>
+  <longdescription>
+    ACL2 is a logic and programming language in which you can model computer
+    systems, together with a tool to help you prove properties of those models.
+    "ACL2" denotes "A Computational Logic for Applicative Common Lisp". ACL2 is
+    part of the Boyer-Moore family of provers, for which its authors have
+    received the 2005 ACM Software System Award.
+  </longdescription>
+  <upstream>
+    <bugs-to>https://github.com/acl2/acl2/issues/</bugs-to>
+    <remote-id type="github">acl2/acl2</remote-id>
+  </upstream>
+</pkgmetadata>
diff --git a/sci-mathematics/octave/Manifest b/sci-mathematics/octave/Manifest
index 4e34be42c13e..a0a0b0805954 100644
--- a/sci-mathematics/octave/Manifest
+++ b/sci-mathematics/octave/Manifest
@@ -5,7 +5,6 @@ AUX octave-6.4.0-slibtool.patch 1416 BLAKE2B e4b487481490b41a4da499bb5eceff0f6a2
 AUX octave-7.3.0-docs-texinfo-7.0.patch 1623 BLAKE2B 36a6ceda753083171ece9e4045af8551121f7073901d9f32facfd6c2bb88a10226f5aa719a79e8677c7a0cb7f26a226f2da190d9b4281b3fd666f570af3ac761 SHA512 0ac71393c59681a2188316356235ddb876e5c7cbf4a2ff1752bd3dddde7babeb456e0619ed65e32d5048d754416fb33c949aa0979748f7282e3e9d2589931612
 DIST octave-6.4.0.tar.gz 32873157 BLAKE2B afa729c3c9917f724e7d97fe3af42986f323d3ff849e0a33ac9f183237e68d989d4f3dacd644405b648ec050ad07d8973abddbd8657b810de6f65d5b5ae37c02 SHA512 91ff031f6dfff8506fa738fd4f1f07276501fdfe003f8ed992cccf91da14d9d33da6d08923322b0dae5f5b696b49856b0f5c5065e26b0701b0d1630173807435
 DIST octave-7.3.0.tar.xz 26215288 BLAKE2B 53fff89e798f8b8795f83e46f66793f2cf37f98933fa62a47d5ec389f89a3447eb96128c1d6b68a4184630d071ecf1a4323299c251b43c3211a8f781486b32e5 SHA512 1399d7010cbd4e83d6dc60ab8cc2abb20e64a762e905a00066e6331c5350df93b4ff8f2670fd52fc183918cea21bc176cb263ca71080de6e4041f5e0ea21558e
-EBUILD octave-6.4.0-r3.ebuild 6043 BLAKE2B a99d2325249cbd29bcc3b00e734b28f7de4b61025f8f2133d5b7c53ad7bbb14bdbbd068ac204e3f7af80143c3797ec97688487b70361f8966dffd06569b3612d SHA512 559c07c35ecc7011e0f44a23fb2ad392a1562221f7218c0b5d89a2a9a2dd60e9f68e9cf3345b226d572d5da85d63cbe051643363bc9e1896ce4820817317f605
-EBUILD octave-6.4.0-r4.ebuild 6029 BLAKE2B 0bc2a9b11d237a51ea875b916e3dde0db429d3d577a20746d68d7dff43cf3755776a2c19c3bcc5987897e308850f9f570973d8c0abb0506a68d581b42ad3a50c SHA512 d6fef61f24420cbbc7a520ac42d9308f6e1824a68ed6bc928f9225fd5b5fa070ca091375445675d2e0654753b2d87d738e4c920d26bff2d245448a94c3a8b0c3
-EBUILD octave-7.3.0-r1.ebuild 6638 BLAKE2B 4eaa8ca9ce1a7a0ce3bc91efa819aa8025d4d3ad32b7139b572d793f4b66c137adbaa952bb9a576adcfce3d9c48813522c36c7cd2e17e19dd33bda8092ef4a4e SHA512 80d0f6e43c6f45cdfb1e26d9a4c9e321fb254e1abf81f5f2cd40c64b56a9d33fe8cb6ce2062949c42742e0465d71bc56f589d374d0c3c8cfe2c884b315a09df1
+EBUILD octave-6.4.0-r5.ebuild 6099 BLAKE2B 2f2d206f60d84675928d97cc67b14abc3cf6f4749d1b9519b3a03e2811eebc29d33ed87d02a1c23808f9f8bb10db7f299b2a0f8dfca85d0cc1e8e32368f8106d SHA512 615987c1b4f4e7f264ca6c5cf62d27800558accf8fc4c0a54b9a0d250acdeff7200243280dcd35644c0cd324f1f0b8b42ca5cee735faba1aa9b8e09be9b3dbf1
+EBUILD octave-7.3.0-r2.ebuild 6721 BLAKE2B bcd93f4df6d08e24cc934b9157091725ea2aafca293a1d50a6137d9b8c05f8ad11bbcb7fc69c7d76c0fd542c06ccad316a90294334d99718d880d783630ab81c SHA512 17c3e0c3a6603ef5e16277a02daf65fcf1fc83ef0b73aa6190ca1437389f29dd1e14d0ef5956332ab9bc44743d2e011972267c1105c28aa13829ad134becb92d
 MISC metadata.xml 1703 BLAKE2B 0471bc1eeaa2ce86b8eeca5c3e831eb0d9207b5fd1d3c03aba017a257b7b98b313c42a1054471c79dab1b5d2d84df8a8d3b0ee68e772cbe6970ac92f07dc3269 SHA512 3c051ff80c958af4315faa1670cc5e1d6a53397b4182304b760cf4f2e14f716e187dd76879d094e35713ac115c47ea623530c2f4b114f7bf2eae1cdf28bc46b8
diff --git a/sci-mathematics/octave/octave-6.4.0-r3.ebuild b/sci-mathematics/octave/octave-6.4.0-r3.ebuild
deleted file mode 100644
index e99fbea2fc93..000000000000
--- a/sci-mathematics/octave/octave-6.4.0-r3.ebuild
+++ /dev/null
@@ -1,215 +0,0 @@
-# Copyright 1999-2022 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-inherit autotools flag-o-matic fortran-2 java-pkg-opt-2 pax-utils qmake-utils toolchain-funcs xdg-utils
-
-DESCRIPTION="High-level interactive language for numerical computations"
-LICENSE="GPL-3"
-HOMEPAGE="https://www.gnu.org/software/octave/"
-SRC_URI="mirror://gnu/${PN}/${P}.tar.gz"
-
-SLOT="0/${PV}"
-IUSE="curl doc fftw +glpk gnuplot gui hdf5 java opengl
-	portaudio postscript +qhull +qrupdate readline sndfile +sparse
-	ssl static-libs sundials X zlib"
-KEYWORDS="amd64 arm arm64 ~hppa ~ppc ~ppc64 ~riscv x86 ~amd64-linux ~x86-linux"
-
-# Although it is listed in INSTALL.OCTAVE as a build tool, Octave runs
-# "makeinfo" from sys-apps/texinfo at runtime to convert its texinfo
-# documentation to text (see scripts/help/help.m).
-#
-# (un)zip isn't mentioned, but there's a test that uses it (bug 775254).
-#
-RDEPEND="
-	app-arch/bzip2
-	app-arch/unzip
-	app-arch/zip
-	app-text/ghostscript-gpl
-	sys-apps/texinfo
-	dev-libs/libpcre:3=
-	sys-libs/ncurses:0=
-	sys-libs/zlib
-	virtual/blas
-	virtual/lapack
-	curl? ( net-misc/curl:0= )
-	fftw? ( sci-libs/fftw:3.0= )
-	glpk? ( sci-mathematics/glpk:0= )
-	gnuplot? ( sci-visualization/gnuplot )
-	gui? (
-		dev-qt/qtcore:5
-		dev-qt/qtgui:5
-		dev-qt/qthelp:5
-		dev-qt/qtnetwork:5
-		dev-qt/qtopengl:5
-		dev-qt/qtprintsupport:5
-		dev-qt/qtwidgets:5
-		x11-libs/qscintilla:=
-	)
-	hdf5? ( sci-libs/hdf5:0= )
-	java? ( >=virtual/jre-1.6.0:* )
-	opengl? (
-		media-libs/freetype:2=
-		media-libs/fontconfig:1.0=
-		virtual/glu
-		>=x11-libs/fltk-1.3:1=[opengl,xft]
-		x11-libs/gl2ps:0=
-	)
-	portaudio? ( media-libs/portaudio )
-	postscript? (
-		app-text/epstool
-		media-gfx/pstoedit
-		media-gfx/transfig
-	)
-	qhull? ( media-libs/qhull:0= )
-	qrupdate? ( sci-libs/qrupdate:0= )
-	readline? ( sys-libs/readline:0= )
-	sndfile? ( media-libs/libsndfile )
-	sparse? (
-		sci-libs/arpack:0=
-		sci-libs/camd:0=
-		sci-libs/ccolamd:0=
-		sci-libs/cholmod:0=
-		sci-libs/colamd:0=
-		sci-libs/cxsparse:0=
-		sci-libs/umfpack:0=
-	)
-	ssl? (
-		dev-libs/openssl:0=
-	)
-	sundials? ( <sci-libs/sundials-6.2.0:= )
-	X? ( x11-libs/libX11:0= )"
-# bug #846968 for sundials < dep
-DEPEND="${RDEPEND}
-	dev-util/gperf
-	doc? (
-		dev-texlive/texlive-fontsrecommended
-		dev-texlive/texlive-plaingeneric
-		dev-texlive/texlive-metapost
-		virtual/latex-base
-	)
-	java? ( >=virtual/jdk-1.6.0 )
-	qrupdate? ( app-misc/pax-utils )
-	sparse? ( app-misc/pax-utils )
-	|| ( media-gfx/imagemagick media-gfx/graphicsmagick[imagemagick] )"
-BDEPEND="
-	virtual/pkgconfig
-	gui? ( dev-qt/linguist-tools:5 )"
-
-PATCHES=(
-	"${FILESDIR}"/${PN}-5.1.0-pkgbuilddir.patch
-	"${FILESDIR}"/${PN}-4.2.2-ncurses-pkgconfig.patch
-	"${FILESDIR}/${PN}-6.4.0-slibtool.patch"
-	"${FILESDIR}"/${PN}-6.4.0-omit-qtchooser-qtver.patch
-)
-
-src_prepare() {
-	default
-
-	# nasty prefix hacks for fltk:1 linking
-	if use prefix; then
-		use opengl && append-ldflags -Wl,-rpath,"${EPREFIX}/usr/$(get_libdir)/fltk-1"
-	fi
-
-	# occasional fail on install, force regeneration (bug #401189)
-	rm doc/interpreter/contributors.texi || die
-
-	eautoreconf
-}
-
-src_configure() {
-	# unfortunate dependency on mpi from hdf5 (bug #302621)
-	use hdf5 && has_version sci-libs/hdf5[mpi] && \
-		export CXX=mpicxx CC=mpicc FC=mpif77 F77=mpif77
-
-	# tell autoconf where to find qt binaries, fix bug #837752
-	export MOC="$(qt5_get_bindir)/moc" UIC="$(qt5_get_bindir)/uic" RCC="$(qt5_get_bindir)/rcc" \
-		LRELEASE="$(qt5_get_bindir)/lrelease" QCOLLECTIONGENERATOR="$(qt5_get_bindir)/qcollectiongenerator" \
-		QHELPGENERATOR="$(qt5_get_bindir)/qhelpgenerator"
-
-	# Some of these use_with flags are a bit mismatched. The configure
-	# script offers only --without-foo, and detects "foo" automatically
-	# unless --without-foo is specified. Passing --with-foo is not an
-	# error, however, so it kind of works. We wind up with, for example,
-	#
-	# --with-sundials_ida (no-op) with USE="sundials"
-	# --without-sundials_ida (disables it) with USE="-sundials"
-	#
-	# The --enable-link-all-dependencies flag is needed because
-	# otherwise, the build system appends --no-undefined to LDFLAGS and
-	# then proceeds to undefine things. GNU libtool ignores this, but
-	# slibtool (for example) does not (bug 776583).
-	econf \
-		--localstatedir="${EPREFIX}/var/state/octave" \
-		--with-blas="$($(tc-getPKG_CONFIG) --libs blas)" \
-		--with-lapack="$($(tc-getPKG_CONFIG) --libs lapack)" \
-		--disable-64 \
-		--disable-jit \
-		--enable-link-all-dependencies \
-		--enable-shared \
-		--with-z \
-		--with-bz2 \
-		$(use_enable static-libs static) \
-		$(use_enable doc docs) \
-		$(use_enable java) \
-		$(use_enable readline) \
-		$(use_with curl) \
-		$(use_with fftw fftw3) \
-		$(use_with fftw fftw3f) \
-		$(use_enable fftw fftw-threads) \
-		$(use_with glpk) \
-		$(use_with hdf5) \
-		$(use_with opengl) \
-		$(use_with opengl fltk) \
-		$(use_with ssl openssl) \
-		$(use_with portaudio) \
-		$(use_with qhull) \
-		$(use_with qrupdate) \
-		$(use_with gui qt 5) \
-		$(use_with sndfile) \
-		$(use_with sparse arpack) \
-		$(use_with sparse umfpack) \
-		$(use_with sparse colamd) \
-		$(use_with sparse ccolamd) \
-		$(use_with sparse cholmod) \
-		$(use_with sparse cxsparse) \
-		$(use_with sundials sundials_ida) \
-		$(use_with X x)
-}
-
-src_compile() {
-	export VARTEXFONTS="${T}/fonts" # otherwise it will write to /var/cache/fonts/ and trip sandbox
-	default
-	if use java; then
-		pax-mark m "${S}/src/.libs/octave-cli"
-	fi
-}
-
-src_install() {
-	default
-	if use doc; then
-		dodoc $(find doc -name '*.pdf')
-	else
-		# bug 566134, macros.texi is installed by make install if use doc
-		insinto /usr/share/${PN}/${PV}/etc
-		doins doc/interpreter/macros.texi
-	fi
-	[[ -e test/fntests.log ]] && dodoc test/fntests.log
-	use java && \
-		java-pkg_regjar "${ED}/usr/share/${PN}/${PV}/m/java/octave.jar"
-	echo "LDPATH=${EPREFIX}/usr/$(get_libdir)/${PN}/${PV}" > 99octave || die
-	doenvd 99octave
-}
-
-pkg_postinst() {
-	xdg_icon_cache_update
-	xdg_mimeinfo_database_update
-	xdg_desktop_database_update
-}
-
-pkg_postrm() {
-	xdg_icon_cache_update
-	xdg_mimeinfo_database_update
-	xdg_desktop_database_update
-}
diff --git a/sci-mathematics/octave/octave-6.4.0-r4.ebuild b/sci-mathematics/octave/octave-6.4.0-r5.ebuild
index 4bc8ceb0934f..b3eb587fad29 100644
--- a/sci-mathematics/octave/octave-6.4.0-r4.ebuild
+++ b/sci-mathematics/octave/octave-6.4.0-r5.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=8
@@ -119,6 +119,9 @@ src_prepare() {
 }
 
 src_configure() {
+	# libstdc++ bug, bug #887815
+	append-cxxflags -U_GLIBCXX_ASSERTIONS
+
 	# unfortunate dependency on mpi from hdf5 (bug #302621)
 	use hdf5 && has_version sci-libs/hdf5[mpi] && \
 		export CXX=mpicxx CC=mpicc FC=mpif77 F77=mpif77
diff --git a/sci-mathematics/octave/octave-7.3.0-r1.ebuild b/sci-mathematics/octave/octave-7.3.0-r2.ebuild
index 50d77f9706b7..2d09264e6440 100644
--- a/sci-mathematics/octave/octave-7.3.0-r1.ebuild
+++ b/sci-mathematics/octave/octave-7.3.0-r2.ebuild
@@ -1,9 +1,9 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=8
 
-inherit autotools fortran-2 java-pkg-opt-2 pax-utils qmake-utils toolchain-funcs xdg
+inherit autotools flag-o-matic fortran-2 java-pkg-opt-2 pax-utils qmake-utils toolchain-funcs xdg
 
 DESCRIPTION="High-level interactive language for numerical computations"
 HOMEPAGE="https://www.gnu.org/software/octave/"
@@ -144,6 +144,9 @@ src_prepare() {
 }
 
 src_configure() {
+	# libstdc++ bug, bug #887815
+	append-cxxflags -U_GLIBCXX_ASSERTIONS
+
 	# Unfortunate dependency on mpi from hdf5 (bug #302621)
 	use hdf5 && has_version sci-libs/hdf5[mpi] && \
 		export CXX=mpicxx CC=mpicc FC=mpif77 F77=mpif77