49316 – app-sci/acl2-2.8.ebuild - industrial strength theorem prover (New Package)

Bug 49316 - app-sci/acl2-2.8.ebuild - industrial strength theorem prover (New Package)

Summary: app-sci/acl2-2.8.ebuild - industrial strength theorem prover (New Package)

Status:	CONFIRMED

Alias:	None

Product:	Gentoo Linux
Classification:	Unclassified
Component:	New packages (show other bugs)
Hardware:	All Linux

Importance:	Normal normal (vote)
Assignee:	Default Assignee for New Packages

URL:	http://www.cs.utexas.edu/users/moore/...
Whiteboard:
Keywords:	EBUILD

Depends on:
Blocks:

Reported:	2004-04-28 13:50 UTC by Thomas Veith (RETIRED)
Modified:	2019-06-04 12:29 UTC (History)
CC List:	4 users (show)

See Also:
Package list:
Runtime testing required:	---

Attachments
acl2-2.8.ebuild (acl2-2.8.ebuild,1.10 KB, text/plain) 2004-04-28 13:51 UTC, Thomas Veith (RETIRED)	Details
View All Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.

Description Thomas Veith (RETIRED) gentoo-dev

2004-04-28 13:50:34 UTC

An interesting quote about the ACL2-System:

ACL2 is used in industry. Remember the Intel FDIV bug? The first Pentium [trademark, Intel, Inc] could not divide floating-point numbers correctly and it reportedly cost Intel $500 million to fix. At the time that was happening, we used ACL2 to verify that the floating point division microcode on AMD's competing microprocessor, the AMD-K5, was correct. AMD used ACL2 to verify the elementary floating-point operations for the recently released Athlon.

Reproducible: Always
Steps to Reproduce:

Comment 1 Thomas Veith (RETIRED) gentoo-dev

2004-04-28 13:51:12 UTC

Created attachment 30271 [details]
acl2-2.8.ebuild

This builds the ACL2 system

Comment 2 Robin Johnson archtester

2005-01-16 14:41:34 UTC

I don't know how base-system got this...

Comment 3 Daniel Douglas 2008-07-31 11:54:01 UTC

(In reply to comment #2)
> I don't know how base-system got this...
> 

Yes this should probably fall under the category of lisp. Maybe even mathematics, science, or emulation. Either way, acl2 is very mainstream and widely used. It should definitely be in the tree.

Comment 4 Justin Lecher (RETIRED) gentoo-dev

2010-05-28 22:02:55 UTC

latest release is 3.6

Comment 5 Dongxu Li 2011-04-12 16:05:42 UTC

acl2-4.2.ebuild in science overlay

Comment 6 Dongxu Li 2011-04-13 20:19:06 UTC

I don't like the idea of building books in /usr/share in pkg_postinst().

Hope upstream will allow building in another folder and copying over.