Gentoo Websites Logo
Go to: Gentoo Home Documentation Forums Lists Bugs Planet Store Wiki Get Gentoo!
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
: 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)
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

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 Gentoo Infrastructure gentoo-dev Security 2005-01-16 14:41:34 UTC
I don't know how base-system got this...
Comment 3 Dan 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.