* [gentoo-commits] proj/sci:master commit in: sci-mathematics/acl2/, sci-mathematics/acl2/files/
@ 2023-01-12 12:08 Andrew Ammerlaan
0 siblings, 0 replies; 3+ messages in thread
From: Andrew Ammerlaan @ 2023-01-12 12:08 UTC (permalink / raw
To: gentoo-commits
commit: d686c7d94ac7cfbf82252a0723ffb8c0d0aaa8c2
Author: Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
AuthorDate: Thu Jan 12 12:08:26 2023 +0000
Commit: Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
CommitDate: Thu Jan 12 12:08:26 2023 +0000
URL: https://gitweb.gentoo.org/proj/sci.git/commit/?id=d686c7d9
sci-mathematics/acl2: remove duplicate
Signed-off-by: Andrew Ammerlaan <andrewammerlaan <AT> gentoo.org>
sci-mathematics/acl2/acl2-8.3-r1.ebuild | 86 ---------------------
sci-mathematics/acl2/acl2-8.3-r2.ebuild | 89 ----------------------
sci-mathematics/acl2/acl2-8.4-r1.ebuild | 89 ----------------------
sci-mathematics/acl2/acl2-8.4.ebuild | 86 ---------------------
.../acl2/files/acl2-use_make_variable.patch | 13 ----
sci-mathematics/acl2/metadata.xml | 25 ------
6 files changed, 388 deletions(-)
diff --git a/sci-mathematics/acl2/acl2-8.3-r1.ebuild b/sci-mathematics/acl2/acl2-8.3-r1.ebuild
deleted file mode 100644
index d0bb4eade..000000000
--- a/sci-mathematics/acl2/acl2-8.3-r1.ebuild
+++ /dev/null
@@ -1,86 +0,0 @@
-# Copyright 1999-2021 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-inherit elisp-common
-
-DESCRIPTION="Industrial strength theorem prover"
-HOMEPAGE="https://www.cs.utexas.edu/users/moore/acl2/"
-SRC_URI="https://github.com/acl2/acl2/archive/${PV}/${P}.tar.gz"
-
-SLOT="0"
-LICENSE="BSD"
-KEYWORDS="~amd64 ~x86"
-IUSE="books doc emacs"
-
-BDEPEND="
- dev-lisp/sbcl
- emacs? ( >=app-editors/emacs-23.1:* )
-"
-DEPEND="
- dev-lisp/sbcl:=
- books? ( dev-lang/perl )
- doc? ( dev-lang/perl )
-"
-RDEPEND="${DEPEND}"
-
-PATCHES=( "${FILESDIR}"/${PN}-use_make_variable.patch )
-
-src_prepare() {
- find . -type f -name "*.bak" -delete
- find . -type f -name "*.orig" -delete
- # Remove sparc binary inadvertently included in upstream
- rm books/workshops/2003/schmaltz-al-sammane-et-al/support/acl2link || die
- default
-}
-
-src_compile() {
- emake LISP="sbcl --noinform --noprint \
- --no-sysinit --no-userinit --disable-debugger"
-
- if use books; then
- emake "ACL2=${S}/saved_acl2" basic
- fi
-
- if use doc; then
- emake "ACL2=${S}/saved_acl2" DOC
- fi
-
- if use emacs; then
- elisp-compile emacs/*.el
- fi
-}
-
-src_install() {
- local SAVED_NAME=saved_acl2
- sed -e "s:${S}:/usr/share/acl2:g" -i ${SAVED_NAME} || die
- dobin ${SAVED_NAME}
-
- insinto /usr/share/acl2
- doins ${SAVED_NAME}.core
- if use books; then
- sed -e "/5/a export ACL2_SYSTEM_BOOKS=/usr/share/acl2/books/" \
- -i ${SAVED_NAME} || die
- doins -r books
- fi
-
- DOCS=( books/README.md )
- if use doc; then
- HTML_DOCS=( doc/HTML/. )
- fi
- einstalldocs
-
- if use emacs; then
- elisp-install ${PN} emacs/*{.el,elc}
- doins TAGS
- fi
-}
-
-pkg_postinst() {
- use emacs && elisp-site-regen
-}
-
-pkg_postrm() {
- use emacs && elisp-site-regen
-}
diff --git a/sci-mathematics/acl2/acl2-8.3-r2.ebuild b/sci-mathematics/acl2/acl2-8.3-r2.ebuild
deleted file mode 100644
index 03cd890b4..000000000
--- a/sci-mathematics/acl2/acl2-8.3-r2.ebuild
+++ /dev/null
@@ -1,89 +0,0 @@
-# Copyright 1999-2021 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-inherit elisp-common
-
-DESCRIPTION="Industrial strength theorem prover"
-HOMEPAGE="https://www.cs.utexas.edu/users/moore/acl2/"
-SRC_URI="https://github.com/acl2/acl2/archive/${PV}/${P}.tar.gz"
-
-SLOT="0"
-LICENSE="BSD"
-KEYWORDS="~amd64 ~x86"
-IUSE="books doc emacs"
-
-BDEPEND="
- dev-lisp/sbcl
- emacs? ( >=app-editors/emacs-23.1:* )
-"
-DEPEND="
- dev-lisp/sbcl:=
- books? ( dev-lang/perl )
- doc? ( dev-lang/perl )
-"
-RDEPEND="${DEPEND}"
-
-PATCHES=( "${FILESDIR}"/${PN}-use_make_variable.patch )
-
-src_prepare() {
- find . -type f -name "*.bak" -delete
- find . -type f -name "*.orig" -delete
- # Remove sparc binary inadvertently included in upstream
- rm books/workshops/2003/schmaltz-al-sammane-et-al/support/acl2link || die
- default
-}
-
-src_compile() {
- emake LISP="sbcl --noinform --noprint \
- --no-sysinit --no-userinit --disable-debugger"
-
- if use books; then
- emake "ACL2=${S}/saved_acl2" basic
- fi
-
- if use doc; then
- emake "ACL2=${S}/saved_acl2" DOC
- fi
-
- if use emacs; then
- elisp-compile emacs/*.el
- fi
-}
-
-src_install() {
- local SAVED_NAME=saved_acl2
- sed -e "s:${S}:/usr/share/acl2:g" -i ${SAVED_NAME} || die
- if use books; then
- sed -e "5iexport ACL2_SYSTEM_BOOKS=/usr/share/acl2/books/" \
- -i ${SAVED_NAME} || die
- fi
- dobin ${SAVED_NAME}
-
- insinto /usr/share/acl2
- doins ${SAVED_NAME}.core
-
- if use books; then
- doins -r books
- fi
-
- DOCS=( books/README.md )
- if use doc; then
- HTML_DOCS=( doc/HTML/. )
- fi
- einstalldocs
-
- if use emacs; then
- elisp-install ${PN} emacs/*{.el,elc}
- doins TAGS
- fi
-}
-
-pkg_postinst() {
- use emacs && elisp-site-regen
-}
-
-pkg_postrm() {
- use emacs && elisp-site-regen
-}
diff --git a/sci-mathematics/acl2/acl2-8.4-r1.ebuild b/sci-mathematics/acl2/acl2-8.4-r1.ebuild
deleted file mode 100644
index cb1098877..000000000
--- a/sci-mathematics/acl2/acl2-8.4-r1.ebuild
+++ /dev/null
@@ -1,89 +0,0 @@
-# Copyright 1999-2021 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-inherit elisp-common
-
-DESCRIPTION="Industrial strength theorem prover"
-HOMEPAGE="https://www.cs.utexas.edu/users/moore/acl2/"
-SRC_URI="https://github.com/acl2/acl2/archive/${PV}/${P}.tar.gz"
-
-SLOT="0"
-LICENSE="BSD"
-KEYWORDS="~amd64 ~x86"
-IUSE="books doc emacs"
-
-BDEPEND="
- >=dev-lisp/sbcl-1.5.2
- emacs? ( >=app-editors/emacs-23.1:* )
-"
-DEPEND="
- dev-lisp/sbcl:=
- books? ( dev-lang/perl )
- doc? ( dev-lang/perl )
-"
-RDEPEND="${DEPEND}"
-
-PATCHES=( "${FILESDIR}"/${PN}-use_make_variable.patch )
-
-src_prepare() {
- find . -type f -name "*.bak" -delete
- find . -type f -name "*.orig" -delete
- # Remove sparc binary inadvertently included in upstream
- rm books/workshops/2003/schmaltz-al-sammane-et-al/support/acl2link || die
- default
-}
-
-src_compile() {
- emake LISP="sbcl --noinform --noprint \
- --no-sysinit --no-userinit --disable-debugger"
-
- if use books; then
- emake "ACL2=${S}/saved_acl2" basic
- fi
-
- if use doc; then
- emake "ACL2=${S}/saved_acl2" DOC
- fi
-
- if use emacs; then
- elisp-compile emacs/*.el
- fi
-}
-
-src_install() {
- local SAVED_NAME=saved_acl2
- sed -e "s:${S}:/usr/share/acl2:g" -i ${SAVED_NAME} || die
- if use books; then
- sed -e "5iexport ACL2_SYSTEM_BOOKS=/usr/share/acl2/books/" \
- -i ${SAVED_NAME} || die
- fi
- dobin ${SAVED_NAME}
-
- insinto /usr/share/acl2
- doins ${SAVED_NAME}.core
-
- if use books; then
- doins -r books
- fi
-
- DOCS=( books/README.md )
- if use doc; then
- HTML_DOCS=( doc/HTML/. )
- fi
- einstalldocs
-
- if use emacs; then
- elisp-install ${PN} emacs/*{.el,elc}
- doins TAGS
- fi
-}
-
-pkg_postinst() {
- use emacs && elisp-site-regen
-}
-
-pkg_postrm() {
- use emacs && elisp-site-regen
-}
diff --git a/sci-mathematics/acl2/acl2-8.4.ebuild b/sci-mathematics/acl2/acl2-8.4.ebuild
deleted file mode 100644
index dfc3967ed..000000000
--- a/sci-mathematics/acl2/acl2-8.4.ebuild
+++ /dev/null
@@ -1,86 +0,0 @@
-# Copyright 1999-2021 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-inherit elisp-common
-
-DESCRIPTION="Industrial strength theorem prover"
-HOMEPAGE="https://www.cs.utexas.edu/users/moore/acl2/"
-SRC_URI="https://github.com/acl2/acl2/archive/${PV}/${P}.tar.gz"
-
-SLOT="0"
-LICENSE="BSD"
-KEYWORDS="~amd64 ~x86"
-IUSE="books doc emacs"
-
-BDEPEND="
- >=dev-lisp/sbcl-1.5.2
- emacs? ( >=app-editors/emacs-23.1:* )
-"
-DEPEND="
- dev-lisp/sbcl:=
- books? ( dev-lang/perl )
- doc? ( dev-lang/perl )
-"
-RDEPEND="${DEPEND}"
-
-PATCHES=( "${FILESDIR}"/${PN}-use_make_variable.patch )
-
-src_prepare() {
- find . -type f -name "*.bak" -delete
- find . -type f -name "*.orig" -delete
- # Remove sparc binary inadvertently included in upstream
- rm books/workshops/2003/schmaltz-al-sammane-et-al/support/acl2link || die
- default
-}
-
-src_compile() {
- emake LISP="sbcl --noinform --noprint \
- --no-sysinit --no-userinit --disable-debugger"
-
- if use books; then
- emake "ACL2=${S}/saved_acl2" basic
- fi
-
- if use doc; then
- emake "ACL2=${S}/saved_acl2" DOC
- fi
-
- if use emacs; then
- elisp-compile emacs/*.el
- fi
-}
-
-src_install() {
- local SAVED_NAME=saved_acl2
- sed -e "s:${S}:/usr/share/acl2:g" -i ${SAVED_NAME} || die
- dobin ${SAVED_NAME}
-
- insinto /usr/share/acl2
- doins ${SAVED_NAME}.core
- if use books; then
- sed -e "/5/a export ACL2_SYSTEM_BOOKS=/usr/share/acl2/books/" \
- -i ${SAVED_NAME} || die
- doins -r books
- fi
-
- DOCS=( books/README.md )
- if use doc; then
- HTML_DOCS=( doc/HTML/. )
- fi
- einstalldocs
-
- if use emacs; then
- elisp-install ${PN} emacs/*{.el,elc}
- doins TAGS
- fi
-}
-
-pkg_postinst() {
- use emacs && elisp-site-regen
-}
-
-pkg_postrm() {
- use emacs && elisp-site-regen
-}
diff --git a/sci-mathematics/acl2/files/acl2-use_make_variable.patch b/sci-mathematics/acl2/files/acl2-use_make_variable.patch
deleted file mode 100644
index 32e0f05da..000000000
--- a/sci-mathematics/acl2/files/acl2-use_make_variable.patch
+++ /dev/null
@@ -1,13 +0,0 @@
-use make variable to avoid QA issue: "make[1]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule"
-
---- a/GNUmakefile
-+++ b/GNUmakefile
-@@ -576,7 +576,7 @@ doc/home-page.html: doc/home-page.lisp
- # xdoc::save that populates doc/manual/ (not under books/).
- acl2-manual: check-books
- rm -rf doc/manual books/system/doc/acl2-manual.cert
-- cd books ; make USE_QUICKLISP=1 system/doc/acl2-manual.cert
-+ cd books ; $(MAKE) USE_QUICKLISP=1 system/doc/acl2-manual.cert
- rm -rf doc/manual/download/*
-
- # WARNING: The dependency list just below isn't complete, since it
diff --git a/sci-mathematics/acl2/metadata.xml b/sci-mathematics/acl2/metadata.xml
deleted file mode 100644
index b3d826757..000000000
--- a/sci-mathematics/acl2/metadata.xml
+++ /dev/null
@@ -1,25 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
-<pkgmetadata>
- <maintainer type="person">
- <email>dongxuli2011@gmail.com</email>
- <name>Dongxu Li</name>
- <description>Industrial strength theorem prover</description>
- </maintainer>
- <maintainer type="project">
- <email>sci-mathematics@gentoo.org</email>
- <name>Gentoo Mathematics Project</name>
- </maintainer>
- <longdescription>
- ACL2 is both a programming language in which you can model computer systems and
- a tool to help you prove properties of those models. ACL2 is part of the
- Boyer-Moore family of provers, for which its authors have received the 2005 ACM
- Software System Award.
- </longdescription>
- <use>
- <flag name="books">build community books, the canonical collection of open-source libraries</flag>
- </use>
- <upstream>
- <remote-id type="github">acl2/acl2</remote-id>
- </upstream>
-</pkgmetadata>
^ permalink raw reply related [flat|nested] 3+ messages in thread* [gentoo-commits] proj/sci:master commit in: sci-mathematics/acl2/, sci-mathematics/acl2/files/
@ 2021-09-12 7:38 Andrew Ammerlaan
0 siblings, 0 replies; 3+ messages in thread
From: Andrew Ammerlaan @ 2021-09-12 7:38 UTC (permalink / raw
To: gentoo-commits
commit: a9a6dc87759ff69f93105d2b85b5cd90755380e5
Author: Lucas Mitrak <lucas <AT> lucasmitrak <DOT> com>
AuthorDate: Mon Aug 9 03:09:54 2021 +0000
Commit: Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
CommitDate: Sun Sep 12 07:37:31 2021 +0000
URL: https://gitweb.gentoo.org/proj/sci.git/commit/?id=a9a6dc87
sci-mathematics/acl2: fix TAGS install, add emacs/doc flags, etc
* version bump
* EAPI bump
* Remove eutils because it is no longer necessary and deprecated
* inherit elisp-common for compiling/installing emacs files
* Add emacs use flag for emacs files and TAGS file
* Add app-editor/emacs to BDEPEND if its needed during compilation
* Add doc use flag for compiling and installing html docs
* Add dev-lang/perl as a DEPEND for doc
* Change SRC_URI to upstream and updated github
* Update metadata.xml to this new SRC_URI
* Add patch which changes `make` to $(MAKE) in GNUmakefile for Q/A
* Add src_prepare which deletes *.bak, *.orig, and sparc binary acl2link
* Remove `emake certify-books` because certify-books no longer exists
* Add `emake basic` because it is the one which is the default [1]
* emake basic is much faster so the einfos are removed
* Add `emake DOC` to compilation phase if DOC use flag is enabled
* Add `elisp-compile` to compilation phase if emacs use flag is enabled
* Install README.md always and html docs if doc use flag is enabled
* Install emacs files and TAGS file is emacs use flag is enabled
* Add `use emacs && elisp-site-regen` to postinst() and postrm() phases
Currently, sci-mathematics/acl2 will not always install successfully.
This is because the TAGS file is only created if the etags program is
installed. The etags program is installed when emacs is
installed. Therefore, an emacs use flag is added so the TAGS file is
installed only when it is enabled. Since app-editors/emacs is required
for the CBUILD, the dependency is added to the BDEPEND. In order to
compile/install emacs files, the elisp-common eclass is inherited.
This compilation and installation only takes place if the emacs use
flag is enabled. The `elisp-site-regen` is added to pkg_postinst() and
pkg_postrm() with the requirement of the emacs use flag being enabled.
If the doc flag is enabled, then `emake DOC` is executed and the html
docs are installed; however, the README.md is always installed. Since
dev-lang/perl is needed for this compilation, it is added as a
conditional requirement. If the books use flag is enabled, then the
books will be compiled using `emake basic`. The reason `emake basic`
was chosen instead of `emake regression` is because the latter is
stated as being "usually unnecessary" [1] and that "most users will not
want to use this target" [2] while the former is the default [1]
and stated as "a convenient starting place" [3]. Every book is made
before for major releases, so it is unecessary to to build all for an
install. Since the compilation of the books is much faster, the einfo
messages are removed. In addition, the SRC_URI for the previous ebuild
is behind in commits [4] and is simply a clone. Therefore, the main
github repo replaced it. The metadata is updated to this change also.
A src_prepare phase was added which copies debian's Changelog of this
package [5]. The entry on 2015-10-21 of this Changelog shows that
the *.bak and *.orig files were removed to clean the target. Also,
the inadvertent sparc binary acl2link was removed. This sparc binary
lacks source code and therefore violates the GNU GPL. Debian filed a
bug about this binary and the solution was to delete it [6].
A patch is added so a Q/A warning is not given: "make[1]: warning:
jobserver unavailable: using -j1. Add '+' to parent make rule".
The patch changes a make command to use the variable $(MAKE). This
patch will be made available upstream via a github pull request.
Finally, eutils is removed due to being depreciated and the EAPI is
bumped.
[1] https://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/
index.html?topic=ACL2____BOOKS-CERTIFICATION
[2] https://github.com/acl2/acl2/blob/8.3/books/GNUmakefile#L61
[3] https://github.com/acl2/acl2/blob/8.3/books/GNUmakefile#L48
[4] https://github.com/acl2-devel/acl2-devel
[5] https://debian.pkgs.org/9/debian-main-arm64/
acl2_7.2dfsg-3_arm64.deb.html
[6] https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=787368
Closes: https://bugs.gentoo.org/755368
Package-Manager: Portage-3.0.20, Repoman-3.0.2
Signed-off-by: Lucas Mitrak <lucas <AT> lucasmitrak.com>
Closes: https://github.com/gentoo/sci/pull/1109
Signed-off-by: Andrew Ammerlaan <andrewammerlaan <AT> gentoo.org>
sci-mathematics/acl2/acl2-8.4.ebuild | 86 ++++++++++++++++++++++
.../acl2/files/acl2-use_make_variable.patch | 13 ++++
sci-mathematics/acl2/metadata.xml | 2 +-
3 files changed, 100 insertions(+), 1 deletion(-)
diff --git a/sci-mathematics/acl2/acl2-8.4.ebuild b/sci-mathematics/acl2/acl2-8.4.ebuild
new file mode 100644
index 000000000..d0bb4eade
--- /dev/null
+++ b/sci-mathematics/acl2/acl2-8.4.ebuild
@@ -0,0 +1,86 @@
+# Copyright 1999-2021 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit elisp-common
+
+DESCRIPTION="Industrial strength theorem prover"
+HOMEPAGE="https://www.cs.utexas.edu/users/moore/acl2/"
+SRC_URI="https://github.com/acl2/acl2/archive/${PV}/${P}.tar.gz"
+
+SLOT="0"
+LICENSE="BSD"
+KEYWORDS="~amd64 ~x86"
+IUSE="books doc emacs"
+
+BDEPEND="
+ dev-lisp/sbcl
+ emacs? ( >=app-editors/emacs-23.1:* )
+"
+DEPEND="
+ dev-lisp/sbcl:=
+ books? ( dev-lang/perl )
+ doc? ( dev-lang/perl )
+"
+RDEPEND="${DEPEND}"
+
+PATCHES=( "${FILESDIR}"/${PN}-use_make_variable.patch )
+
+src_prepare() {
+ find . -type f -name "*.bak" -delete
+ find . -type f -name "*.orig" -delete
+ # Remove sparc binary inadvertently included in upstream
+ rm books/workshops/2003/schmaltz-al-sammane-et-al/support/acl2link || die
+ default
+}
+
+src_compile() {
+ emake LISP="sbcl --noinform --noprint \
+ --no-sysinit --no-userinit --disable-debugger"
+
+ if use books; then
+ emake "ACL2=${S}/saved_acl2" basic
+ fi
+
+ if use doc; then
+ emake "ACL2=${S}/saved_acl2" DOC
+ fi
+
+ if use emacs; then
+ elisp-compile emacs/*.el
+ fi
+}
+
+src_install() {
+ local SAVED_NAME=saved_acl2
+ sed -e "s:${S}:/usr/share/acl2:g" -i ${SAVED_NAME} || die
+ dobin ${SAVED_NAME}
+
+ insinto /usr/share/acl2
+ doins ${SAVED_NAME}.core
+ if use books; then
+ sed -e "/5/a export ACL2_SYSTEM_BOOKS=/usr/share/acl2/books/" \
+ -i ${SAVED_NAME} || die
+ doins -r books
+ fi
+
+ DOCS=( books/README.md )
+ if use doc; then
+ HTML_DOCS=( doc/HTML/. )
+ fi
+ einstalldocs
+
+ if use emacs; then
+ elisp-install ${PN} emacs/*{.el,elc}
+ doins TAGS
+ fi
+}
+
+pkg_postinst() {
+ use emacs && elisp-site-regen
+}
+
+pkg_postrm() {
+ use emacs && elisp-site-regen
+}
diff --git a/sci-mathematics/acl2/files/acl2-use_make_variable.patch b/sci-mathematics/acl2/files/acl2-use_make_variable.patch
new file mode 100644
index 000000000..32e0f05da
--- /dev/null
+++ b/sci-mathematics/acl2/files/acl2-use_make_variable.patch
@@ -0,0 +1,13 @@
+use make variable to avoid QA issue: "make[1]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule"
+
+--- a/GNUmakefile
++++ b/GNUmakefile
+@@ -576,7 +576,7 @@ doc/home-page.html: doc/home-page.lisp
+ # xdoc::save that populates doc/manual/ (not under books/).
+ acl2-manual: check-books
+ rm -rf doc/manual books/system/doc/acl2-manual.cert
+- cd books ; make USE_QUICKLISP=1 system/doc/acl2-manual.cert
++ cd books ; $(MAKE) USE_QUICKLISP=1 system/doc/acl2-manual.cert
+ rm -rf doc/manual/download/*
+
+ # WARNING: The dependency list just below isn't complete, since it
diff --git a/sci-mathematics/acl2/metadata.xml b/sci-mathematics/acl2/metadata.xml
index 6035ff684..b3d826757 100644
--- a/sci-mathematics/acl2/metadata.xml
+++ b/sci-mathematics/acl2/metadata.xml
@@ -20,6 +20,6 @@
<flag name="books">build community books, the canonical collection of open-source libraries</flag>
</use>
<upstream>
- <remote-id type="github">acl2-devel/acl2-devel</remote-id>
+ <remote-id type="github">acl2/acl2</remote-id>
</upstream>
</pkgmetadata>
^ permalink raw reply related [flat|nested] 3+ messages in thread* [gentoo-commits] proj/sci:master commit in: sci-mathematics/acl2/, sci-mathematics/acl2/files/
@ 2015-03-29 10:24 Justin Lecher
0 siblings, 0 replies; 3+ messages in thread
From: Justin Lecher @ 2015-03-29 10:24 UTC (permalink / raw
To: gentoo-commits
commit: b4f72187a5b3973e5afeb7c09a04735d46a9f932
Author: zcj <ustcscgy <AT> 163 <DOT> com>
AuthorDate: Wed Mar 25 12:27:42 2015 +0000
Commit: Justin Lecher <jlec <AT> gentoo <DOT> org>
CommitDate: Wed Mar 25 12:27:42 2015 +0000
URL: https://gitweb.gentoo.org/proj/sci.git/commit/?id=b4f72187
sci-mathematics/acl2: Version bump, drop old; USE flags change.
sci-mathematics/acl2/ChangeLog | 9 +++-
sci-mathematics/acl2/acl2-6.3.ebuild | 69 ---------------------------
sci-mathematics/acl2/acl2-7.0.ebuild | 50 +++++++++++++++++++
sci-mathematics/acl2/files/set-booksdir.patch | 11 -----
sci-mathematics/acl2/metadata.xml | 20 +++-----
5 files changed, 63 insertions(+), 96 deletions(-)
diff --git a/sci-mathematics/acl2/ChangeLog b/sci-mathematics/acl2/ChangeLog
index 995db65..baff65a 100644
--- a/sci-mathematics/acl2/ChangeLog
+++ b/sci-mathematics/acl2/ChangeLog
@@ -1,7 +1,13 @@
# ChangeLog for sci-mathematics/acl2
-# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
+# Copyright 1999-2015 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
+*acl2-7.0 (25 Mar 2015)
+
+ 25 Mar 2015; zcj <ustcscgy@163.com> +acl2-7.0.ebuild, -acl2-6.3.ebuild,
+ -files/set-booksdir.patch, metadata.xml:
+ sci-mathematics/acl2: sci-mathematics/acl2 version bump, drop old
+
12 Nov 2014; Justin Lecher <jlec@gentoo.org> -acl2-4.2.ebuild,
-acl2-4.3.ebuild:
Drop old
@@ -28,4 +34,3 @@
12 Apr 2011; Dongxu Li <dongxuli2011@gmail.com> +acl2-4.2.ebuild +ChangeLog +metadata.xml :
Initial import. #49316
-
diff --git a/sci-mathematics/acl2/acl2-6.3.ebuild b/sci-mathematics/acl2/acl2-6.3.ebuild
deleted file mode 100644
index 5302b3c..0000000
--- a/sci-mathematics/acl2/acl2-6.3.ebuild
+++ /dev/null
@@ -1,69 +0,0 @@
-# Copyright 1999-2014 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: $
-
-EAPI=5
-
-inherit eutils
-
-DESCRIPTION="ACL2 industrial strength theorem prover"
-HOMEPAGE="http://www.cs.utexas.edu/users/moore/acl2/"
-SRC_URI="
- http://www.cs.utexas.edu/users/moore/${PN}/v${PV/\./-}/distrib/${PN}.tar.gz -> ${P}.tar.gz
- books? ( https://acl2-books.googlecode.com/files/books-${PV}.tar.gz
- workshops? ( http://acl2-books.googlecode.com/files/workshops-${PV}.tar.gz ) )"
-
-SLOT="0"
-LICENSE="BSD"
-KEYWORDS="~amd64 ~x86"
-IUSE="+books workshops html"
-
-REQUIRED_USE="workshops? ( books )"
-
-DEPEND="
- dev-lisp/sbcl
- books? ( dev-lang/perl )"
-RDEPEND="${DEPEND}"
-
-S="${WORKDIR}/${PN}-sources"
-
-src_unpack() {
- default
- if use books; then
- mv "${WORKDIR}/books" "${S}"/ || die
- if use workshops; then
- mv "${WORKDIR}/workshops" "${S}/books/" || die
- fi
- fi
-}
-
-src_compile() {
- emake LISP="sbcl --noinform --noprint"
-
- if use books; then
- echo
- einfo "Building certificates ..."
- einfo "(this may take hours to finish)"
- emake regression
- fi
-}
-
-src_install() {
- sed -e "s:${S}:/usr/share/acl2:g" -i saved_acl2 || die
- if use books; then
- sed -e "/5/a export ACL2_SYSTEM_BOOKS=/usr/share/acl2/books/" \
- -i saved_acl2 || die
- fi
- dobin saved_acl2
-
- insinto /usr/share/acl2
- doins TAGS saved_acl2.core
- if use books; then
- doins -r books
- fi
-
- if use html; then
- dohtml -r doc/HTML
- fi
- doinfo doc/EMACS/*
-}
diff --git a/sci-mathematics/acl2/acl2-7.0.ebuild b/sci-mathematics/acl2/acl2-7.0.ebuild
new file mode 100644
index 0000000..c1bfb90
--- /dev/null
+++ b/sci-mathematics/acl2/acl2-7.0.ebuild
@@ -0,0 +1,50 @@
+# Copyright 1999-2015 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI=5
+
+inherit eutils
+
+DESCRIPTION="Industrial strength theorem prover"
+HOMEPAGE="http://www.cs.utexas.edu/users/moore/acl2/"
+SRC_URI="https://github.com/acl2/acl2/archive/${PV}.tar.gz -> ${P}.tar.gz"
+
+SLOT="0"
+LICENSE="BSD"
+KEYWORDS="~amd64 ~x86"
+IUSE="books"
+
+DEPEND="
+ dev-lisp/sbcl:=
+ books? ( dev-lang/perl )"
+RDEPEND="${DEPEND}"
+
+src_compile() {
+ emake LISP="sbcl --noinform --noprint \
+ --no-sysinit --no-userinit --disable-debugger"
+
+ if use books; then
+ echo
+ einfo "Building certificates ..."
+ einfo "(this may take hours to finish)"
+ emake regression
+ fi
+}
+
+src_install() {
+ SAVED_NAME=saved_acl2h
+ sed -e "s:${S}:/usr/share/acl2:g" -i ${SAVED_NAME} || die
+ if use books; then
+ sed -e "/5/a export ACL2_SYSTEM_BOOKS=/usr/share/acl2/books/" \
+ -i ${SAVED_NAME} || die
+ fi
+ dobin ${SAVED_NAME}
+ dosym ${SAVED_NAME} /usr/bin/saved_acl2
+
+ insinto /usr/share/acl2
+ doins TAGS ${SAVED_NAME}.core
+ if use books; then
+ doins -r books
+ fi
+}
diff --git a/sci-mathematics/acl2/files/set-booksdir.patch b/sci-mathematics/acl2/files/set-booksdir.patch
deleted file mode 100644
index 4f4d433..0000000
--- a/sci-mathematics/acl2/files/set-booksdir.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- a/books/Makefile-generic 2011-04-12 14:42:17.790165650 -0400
-+++ b/books/Makefile-generic 2011-04-12 14:55:54.436829607 -0400
-@@ -55,7 +55,7 @@
- # Determine the location of this Makefile-generic. NOTE: We have
- # tried $(realpath $(dir ...)) and similarly for abspath, but they
- # have returned the empty string, presumably an error.
--BOOKS_DIR := $(dir $(word $(words $(MAKEFILE_LIST)),$(MAKEFILE_LIST)))
-+BOOKS_DIR := /usr/share/acl2/books/
-
- # and use that to determine the default location of ACL2. To override,
- # set the ACL2 variable on the command line or in the environment.
diff --git a/sci-mathematics/acl2/metadata.xml b/sci-mathematics/acl2/metadata.xml
index d0675a2..47ab9ca 100644
--- a/sci-mathematics/acl2/metadata.xml
+++ b/sci-mathematics/acl2/metadata.xml
@@ -5,25 +5,17 @@
<maintainer>
<email>dongxuli2011@gmail.com</email>
<name>Dongxu Li</name>
- <description>ACL2 industrial strength theorem prover</description>
+ <description>Industrial strength theorem prover</description>
</maintainer>
<longdescription>
-ACL2 is both a programming language in which you can model computer systems and
-a tool to help you prove properties of those models. ACL2 is part of the
-Boyer-Moore family of provers, for which its authors have received the 2005 ACM
+ACL2 is both a programming language in which you can model computer systems and
+a tool to help you prove properties of those models. ACL2 is part of the
+Boyer-Moore family of provers, for which its authors have received the 2005 ACM
Software System Award.
-</longdescription>
+ </longdescription>
<use>
<flag name="books">
build community books, the canonical collection of open-source libraries
-</flag>
- </use>
- <use>
- <flag name="html"> Install HTML documentation</flag>
- </use>
- <use>
- <flag name="workshops">
- build community books from ACL2 community workshops
-</flag>
+ </flag>
</use>
</pkgmetadata>
^ permalink raw reply related [flat|nested] 3+ messages in thread
end of thread, other threads:[~2023-01-12 12:08 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2023-01-12 12:08 [gentoo-commits] proj/sci:master commit in: sci-mathematics/acl2/, sci-mathematics/acl2/files/ Andrew Ammerlaan
-- strict thread matches above, loose matches on Subject: below --
2021-09-12 7:38 Andrew Ammerlaan
2015-03-29 10:24 Justin Lecher
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox