From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from lists.gentoo.org (pigeon.gentoo.org [208.92.234.80]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by finch.gentoo.org (Postfix) with ESMTPS id 8F391158092 for ; Sun, 12 Sep 2021 07:38:04 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id E9959E0844; Sun, 12 Sep 2021 07:38:03 +0000 (UTC) Received: from smtp.gentoo.org (dev.gentoo.org [IPv6:2001:470:ea4a:1:5054:ff:fec7:86e4]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by pigeon.gentoo.org (Postfix) with ESMTPS id C2FC7E0844 for ; Sun, 12 Sep 2021 07:38:03 +0000 (UTC) Received: from oystercatcher.gentoo.org (oystercatcher.gentoo.org [148.251.78.52]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtp.gentoo.org (Postfix) with ESMTPS id C2A65342D5B for ; Sun, 12 Sep 2021 07:38:02 +0000 (UTC) Received: from localhost.localdomain (localhost [IPv6:::1]) by oystercatcher.gentoo.org (Postfix) with ESMTP id 5F2F67E for ; Sun, 12 Sep 2021 07:38:01 +0000 (UTC) From: "Andrew Ammerlaan" To: gentoo-commits@lists.gentoo.org Content-Transfer-Encoding: 8bit Content-type: text/plain; charset=UTF-8 Reply-To: gentoo-dev@lists.gentoo.org, "Andrew Ammerlaan" Message-ID: <1631432251.a9a6dc87759ff69f93105d2b85b5cd90755380e5.andrewammerlaan@gentoo> Subject: [gentoo-commits] proj/sci:master commit in: sci-mathematics/acl2/, sci-mathematics/acl2/files/ X-VCS-Repository: proj/sci X-VCS-Files: sci-mathematics/acl2/acl2-8.4.ebuild sci-mathematics/acl2/files/acl2-use_make_variable.patch sci-mathematics/acl2/metadata.xml X-VCS-Directories: sci-mathematics/acl2/files/ sci-mathematics/acl2/ X-VCS-Committer: andrewammerlaan X-VCS-Committer-Name: Andrew Ammerlaan X-VCS-Revision: a9a6dc87759ff69f93105d2b85b5cd90755380e5 X-VCS-Branch: master Date: Sun, 12 Sep 2021 07:38:01 +0000 (UTC) Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: List-Id: Gentoo Linux mail X-BeenThere: gentoo-commits@lists.gentoo.org X-Auto-Response-Suppress: DR, RN, NRN, OOF, AutoReply X-Archives-Salt: c43bab86-2172-4415-bea0-5bf97ccc8e00 X-Archives-Hash: 0cb1f979cb576df6b8e60666ed207e2a commit: a9a6dc87759ff69f93105d2b85b5cd90755380e5 Author: Lucas Mitrak lucasmitrak com> AuthorDate: Mon Aug 9 03:09:54 2021 +0000 Commit: Andrew Ammerlaan gentoo 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 lucasmitrak.com> Closes: https://github.com/gentoo/sci/pull/1109 Signed-off-by: Andrew Ammerlaan 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 @@ build community books, the canonical collection of open-source libraries - acl2-devel/acl2-devel + acl2/acl2