From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from lists.gentoo.org (pigeon.gentoo.org [208.92.234.80]) by finch.gentoo.org (Postfix) with ESMTP id 08AA713827E for ; Mon, 9 Dec 2013 15:06:46 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 0E834E0B98; Mon, 9 Dec 2013 15:06:43 +0000 (UTC) Received: from smtp.gentoo.org (smtp.gentoo.org [140.211.166.183]) (using TLSv1 with cipher AECDH-AES256-SHA (256/256 bits)) (No client certificate requested) by pigeon.gentoo.org (Postfix) with ESMTPS id 8FE5EE0BC6 for ; Mon, 9 Dec 2013 15:06:42 +0000 (UTC) Received: from hornbill.gentoo.org (hornbill.gentoo.org [94.100.119.163]) (using TLSv1 with cipher AECDH-AES256-SHA (256/256 bits)) (No client certificate requested) by smtp.gentoo.org (Postfix) with ESMTPS id 74DDB33F438 for ; Mon, 9 Dec 2013 15:06:41 +0000 (UTC) Received: from localhost.localdomain (localhost [127.0.0.1]) by hornbill.gentoo.org (Postfix) with ESMTP id 0D679E56CE for ; Mon, 9 Dec 2013 15:06:40 +0000 (UTC) From: "Justin Lecher" To: gentoo-commits@lists.gentoo.org Content-Transfer-Encoding: 8bit Content-type: text/plain; charset=UTF-8 Reply-To: gentoo-dev@lists.gentoo.org, "Justin Lecher" Message-ID: <1386601570.226e93fdba1e89adb663241cf6fe32c4e280e5e9.jlec@gentoo> Subject: [gentoo-commits] proj/sci:master commit in: sci-mathematics/acl2/ X-VCS-Repository: proj/sci X-VCS-Files: sci-mathematics/acl2/ChangeLog sci-mathematics/acl2/acl2-6.3.ebuild sci-mathematics/acl2/metadata.xml X-VCS-Directories: sci-mathematics/acl2/ X-VCS-Committer: jlec X-VCS-Committer-Name: Justin Lecher X-VCS-Revision: 226e93fdba1e89adb663241cf6fe32c4e280e5e9 X-VCS-Branch: master Date: Mon, 9 Dec 2013 15:06:40 +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-Archives-Salt: 804e05af-c434-4228-86bd-ff8be620717f X-Archives-Hash: a2c683b093205cc146e9dead26544260 commit: 226e93fdba1e89adb663241cf6fe32c4e280e5e9 Author: Justin Lecher gentoo org> AuthorDate: Mon Dec 9 15:06:10 2013 +0000 Commit: Justin Lecher gentoo org> CommitDate: Mon Dec 9 15:06:10 2013 +0000 URL: http://git.overlays.gentoo.org/gitweb/?p=proj/sci.git;a=commit;h=226e93fd Squashed commit of the following: commit fc52b002e2c028c5df04a4b9868b42989a934b03 Author: Justin Lecher gentoo.org> Date: Mon Dec 9 16:05:48 2013 +0100 sci-mathematics/acl2: Add missing die Package-Manager: portage-2.2.7 commit 79cdf0b10e55b0426e379dba02393c37c381753a Author: zcj 163.com> Date: Mon Dec 9 21:16:12 2013 +0800 sci-mathematics/acl2-6.3: add new USE into metadata.xml commit adf57931576d698bb613be4f7470e991efe6f0d0 Author: zcj 163.com> Date: Mon Dec 9 16:48:24 2013 +0800 sci-mathematics/acl2-6.3: clean up commit 7cfe9431208ac8d2e2194e8ef07ba2c9c8a6d8cd Author: zcj 163.com> Date: Mon Dec 9 15:51:19 2013 +0800 sci-mathematics/acl2: Version bump to 6.3 Signed-off-by: Justin Lecher gentoo.org> --- sci-mathematics/acl2/ChangeLog | 5 ++- sci-mathematics/acl2/acl2-6.3.ebuild | 69 ++++++++++++++++++++++++++++++++++++ sci-mathematics/acl2/metadata.xml | 32 +++++++++++++---- 3 files changed, 98 insertions(+), 8 deletions(-) diff --git a/sci-mathematics/acl2/ChangeLog b/sci-mathematics/acl2/ChangeLog index 5b182f9..4c1c852 100644 --- a/sci-mathematics/acl2/ChangeLog +++ b/sci-mathematics/acl2/ChangeLog @@ -1,7 +1,10 @@ # ChangeLog for sci-mathematics/acl2 -# Copyright 1999-2011 Gentoo Foundation; Distributed under the GPL v2 +# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2 # $Header: $ + 09 Dec 2013; Justin Lecher acl2-6.3.ebuild, metadata.xml: + Add missing die + 15 Aug 2011; Dongxu Li +acl2-4.3.ebuild: Updated metadata diff --git a/sci-mathematics/acl2/acl2-6.3.ebuild b/sci-mathematics/acl2/acl2-6.3.ebuild new file mode 100644 index 0000000..794d34e --- /dev/null +++ b/sci-mathematics/acl2/acl2-6.3.ebuild @@ -0,0 +1,69 @@ +# Copyright 1999-2013 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="GPL-2" +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/metadata.xml b/sci-mathematics/acl2/metadata.xml index f0da4f8..d0675a2 100644 --- a/sci-mathematics/acl2/metadata.xml +++ b/sci-mathematics/acl2/metadata.xml @@ -1,11 +1,29 @@ - sci-mathematics - - dongxuli2011@gmail.com - Dongxu Li - ACL2 industrial strength theorem prover - - 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. + sci-mathematics + + dongxuli2011@gmail.com + Dongxu Li + ACL2 industrial strength theorem prover + + +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. + + + + build community books, the canonical collection of open-source libraries + + + + Install HTML documentation + + + + build community books from ACL2 community workshops + +