[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/acl2/
commit: 9a0df2990ef7a70dc77c4ab7170f9f1fe646d23f
Author: Maciej Barć gentoo org>
AuthorDate: Fri Mar 8 09:19:55 2024 +
Commit: Maciej Barć gentoo org>
CommitDate: Fri Mar 8 11:55:09 2024 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=9a0df299
sci-mathematics/acl2: fix find call
Closes: https://bugs.gentoo.org/926430
Signed-off-by: Maciej Barć gentoo.org>
sci-mathematics/acl2/acl2-8.5_p20240307.ebuild | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/sci-mathematics/acl2/acl2-8.5_p20240307.ebuild
b/sci-mathematics/acl2/acl2-8.5_p20240307.ebuild
index 3d2c045b3a81..1e9c0d6d06d5 100644
--- a/sci-mathematics/acl2/acl2-8.5_p20240307.ebuild
+++ b/sci-mathematics/acl2/acl2-8.5_p20240307.ebuild
@@ -96,10 +96,10 @@ src_install() {
HTML_DOCS=( doc/HTML/. )
einstalldocs
- fi
- # Some binaries in "books". Not needed since the sources are there.
- find "${ED}/usr/share/acl2/books" -type f -name "*.elf64" -delete || die
+ # Some binaries in "books". Not needed since the sources are
there.
+ find "${ED}/usr/share/acl2/books" -type f -name "*.elf64"
-delete || die
+ fi
}
pkg_postinst() {
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/acl2/
commit: bf3578213e54dfc4d10373c77edaf6569a47522e
Author: Maciej Barć gentoo org>
AuthorDate: Thu Mar 7 16:55:29 2024 +
Commit: Maciej Barć gentoo org>
CommitDate: Thu Mar 7 17:38:03 2024 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=bf357821
sci-mathematics/acl2: bump to 8.5_p20240307
Signed-off-by: Maciej Barć gentoo.org>
sci-mathematics/acl2/Manifest | 1 +
sci-mathematics/acl2/acl2-8.5_p20240307.ebuild | 111 +
2 files changed, 112 insertions(+)
diff --git a/sci-mathematics/acl2/Manifest b/sci-mathematics/acl2/Manifest
index 7d370521a91f..358eafcc16bc 100644
--- a/sci-mathematics/acl2/Manifest
+++ b/sci-mathematics/acl2/Manifest
@@ -1 +1,2 @@
DIST acl2-8.5.tar.gz 222696244 BLAKE2B
e5aa8360d9f94ed398d11c4e0873818f8f49ed0e072192c7d62dde99b4a7f98b4240b352818e7691ebc98f85ab3c10981c36bb1e35317e50a111c9c7f3f57b33
SHA512
5a2e004713350ae41ced830aa8620c27963eb108baa499f7e52a1c60961b220ef7a026efdfef6cea1063f731b50f3cccbe1583a9957c9cf269b0a958ec83fe48
+DIST acl2-8.5_p20240307.tar.gz 228577404 BLAKE2B
af7b4f9995b568ba733a1071fa8069798091ea66b91acc9fb839a6f9ba7843762d7130f4d6b653054de4adea91569904ee4c3dcd035350616418c13fa762bc10
SHA512
b5484a49702fa6c657ebf9551dcec2b6a9c0632e137db1480f93ef9aec83fc9bdb9ca95c46ed324b4ff6ab1a428c8ca50bd1750e1bfd6c024d46a4d27728a24e
diff --git a/sci-mathematics/acl2/acl2-8.5_p20240307.ebuild
b/sci-mathematics/acl2/acl2-8.5_p20240307.ebuild
new file mode 100644
index ..3d2c045b3a81
--- /dev/null
+++ b/sci-mathematics/acl2/acl2-8.5_p20240307.ebuild
@@ -0,0 +1,111 @@
+# Copyright 1999-2024 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/;
+
+if [[ "${PV}" == ** ]] ; then
+ inherit git-r3
+
+ EGIT_REPO_URI="https://github.com/${PN}/${PN}.git;
+else
+ COMMIT=6ba68b5c8d645ca45185abc4a24ce46e5ae029c5
+ SRC_URI="https://github.com/${PN}/${PN}/archive/${COMMIT}.tar.gz
+ -> ${P}.tar.gz"
+ S="${WORKDIR}/${PN}-${COMMIT}"
+
+ KEYWORDS="~amd64 ~x86"
+fi
+
+LICENSE="BSD"
+SLOT="0"
+IUSE="doc emacs"
+REQUIRED_USE="emacs? ( doc )"
+
+# SBCL <= 2.4.1 is required, see: https://github.com/acl2/acl2/issues/1580
+RDEPEND="
+ <=dev-lisp/sbcl-2.4.1:=
+ 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
+
+ sed -e "s|\"git\" '(\"rev-parse\" \"HEAD\")|\"echo\" '(\"${COMMIT}\")|"
\
+ -i acl2-init.lisp || die
+
+ default
+}
+
+src_compile() {
+ emake LISP="sbcl --no-sysinit --no-userinit --disable-debugger"
+
+ 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
+
+ if use doc ; then
+ emake ACL2="${S}/saved_acl2" basic DOC
+ 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"
+ dosym -r "/usr/share/acl2/${saved_name}" /usr/bin/acl2
+
+ if use emacs ; then
+ doins TAGS
+ elisp-install "${PN}" books/emacs/*.el{,c}
books/interface/emacs/*.el{,c}
+ elisp-site-file-install "${FILESDIR}/${SITEFILE}"
+ fi
+
+ if use doc ; then
+ doins -r books
+
+ HTML_DOCS=( doc/HTML/. )
+ einstalldocs
+ fi
+
+ # Some binaries in "books". Not needed since the sources are there.
+ find "${ED}/usr/share/acl2/books" -type f -name "*.elf64" -delete || die
+}
+
+pkg_postinst() {
+ use emacs && elisp-site-regen
+}
+
+pkg_postrm() {
+ use emacs && elisp-site-regen
+}
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/acl2/
commit: d9e393ff9fb2c2b47da0607b6b0a07a96417a53a
Author: Maciej Barć gentoo org>
AuthorDate: Thu Mar 7 17:14:12 2024 +
Commit: Maciej Barć gentoo org>
CommitDate: Thu Mar 7 17:38:03 2024 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=d9e393ff
sci-mathematics/acl2: restrict supported SBCL versions
Closes: https://bugs.gentoo.org/926360
Signed-off-by: Maciej Barć gentoo.org>
sci-mathematics/acl2/{acl2-8.5-r1.ebuild => acl2-8.5-r2.ebuild} | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/sci-mathematics/acl2/acl2-8.5-r1.ebuild
b/sci-mathematics/acl2/acl2-8.5-r2.ebuild
similarity index 97%
rename from sci-mathematics/acl2/acl2-8.5-r1.ebuild
rename to sci-mathematics/acl2/acl2-8.5-r2.ebuild
index 19e1ea1d83f7..64fd6d8d1ad9 100644
--- a/sci-mathematics/acl2/acl2-8.5-r1.ebuild
+++ b/sci-mathematics/acl2/acl2-8.5-r2.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2023 Gentoo Authors
+# Copyright 1999-2024 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
@@ -15,14 +15,14 @@ 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"
+SLOT="0"
KEYWORDS="~amd64 ~x86"
IUSE="doc emacs"
REQUIRED_USE="emacs? ( doc )"
RDEPEND="
- dev-lisp/sbcl:=
+ <=dev-lisp/sbcl-2.4.1:=
emacs? ( >=app-editors/emacs-25:* )
"
BDEPEND="
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/acl2/
commit: be49653d54c1c8799824bef4bc28e5a5bec75479
Author: Maciej Barć gentoo org>
AuthorDate: Thu May 25 17:52:42 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Thu May 25 17:52:42 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=be49653d
sci-mathematics/acl2: need to rebuild ACL2 "core" on sbcl update
Signed-off-by: Maciej Barć gentoo.org>
sci-mathematics/acl2/{acl2-8.5.ebuild => acl2-8.5-r1.ebuild} | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/sci-mathematics/acl2/acl2-8.5.ebuild
b/sci-mathematics/acl2/acl2-8.5-r1.ebuild
similarity index 99%
rename from sci-mathematics/acl2/acl2-8.5.ebuild
rename to sci-mathematics/acl2/acl2-8.5-r1.ebuild
index c681f996e4fd..19e1ea1d83f7 100644
--- a/sci-mathematics/acl2/acl2-8.5.ebuild
+++ b/sci-mathematics/acl2/acl2-8.5-r1.ebuild
@@ -22,7 +22,7 @@ IUSE="doc emacs"
REQUIRED_USE="emacs? ( doc )"
RDEPEND="
- dev-lisp/sbcl
+ dev-lisp/sbcl:=
emacs? ( >=app-editors/emacs-25:* )
"
BDEPEND="
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/acl2/
commit: 6b673a9c34d8585fe9cf383ba3f1f057f95c6c8a
Author: Maciej Barć gentoo org>
AuthorDate: Sun Jan 8 13:47:13 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Sun Jan 8 14:08:24 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=6b673a9c
sci-mathematics/acl2: install TAGS if USE=emacs
Closes: https://bugs.gentoo.org/890176
Signed-off-by: Maciej Barć gentoo.org>
sci-mathematics/acl2/acl2-8.5.ebuild | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/sci-mathematics/acl2/acl2-8.5.ebuild
b/sci-mathematics/acl2/acl2-8.5.ebuild
index bea58cd4e997..c681f996e4fd 100644
--- a/sci-mathematics/acl2/acl2-8.5.ebuild
+++ b/sci-mathematics/acl2/acl2-8.5.ebuild
@@ -66,7 +66,6 @@ src_install() {
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
@@ -76,6 +75,7 @@ src_install() {
einstalldocs
fi
if use emacs ; then
+ doins TAGS
elisp-install ${PN} \
books/emacs/*.el{,c}\
books/interface/emacs/*.el{,c}
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/acl2/files/, sci-mathematics/acl2/
commit: c2cefd413637c6d457d9a552f93c617f834fca70
Author: Maciej Barć gentoo org>
AuthorDate: Sat Jan 7 23:35:06 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Sun Jan 8 00:29:18 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=c2cefd41
sci-mathematics/acl2: new package; add 8.5
Signed-off-by: Maciej Barć gentoo.org>
sci-mathematics/acl2/Manifest | 1 +
sci-mathematics/acl2/acl2-8.5.ebuild| 92 +
sci-mathematics/acl2/files/50acl2-gentoo.el | 6 ++
sci-mathematics/acl2/metadata.xml | 20 +++
4 files changed, 119 insertions(+)
diff --git a/sci-mathematics/acl2/Manifest b/sci-mathematics/acl2/Manifest
new file mode 100644
index ..7d370521a91f
--- /dev/null
+++ b/sci-mathematics/acl2/Manifest
@@ -0,0 +1 @@
+DIST acl2-8.5.tar.gz 222696244 BLAKE2B
e5aa8360d9f94ed398d11c4e0873818f8f49ed0e072192c7d62dde99b4a7f98b4240b352818e7691ebc98f85ab3c10981c36bb1e35317e50a111c9c7f3f57b33
SHA512
5a2e004713350ae41ced830aa8620c27963eb108baa499f7e52a1c60961b220ef7a026efdfef6cea1063f731b50f3cccbe1583a9957c9cf269b0a958ec83fe48
diff --git a/sci-mathematics/acl2/acl2-8.5.ebuild
b/sci-mathematics/acl2/acl2-8.5.ebuild
new file mode 100644
index ..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 ..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 ..df9ae811037d
--- /dev/null
+++ b/sci-mathematics/acl2/metadata.xml
@@ -0,0 +1,20 @@
+
+https://www.gentoo.org/dtd/metadata.dtd;>
+
+
+
+sci-mathemat...@gentoo.org
+Gentoo Mathematics Project
+
+
+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
