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.
Steps to Reproduce:
Created attachment 30271 [details]
This builds the ACL2 system
I don't know how base-system got this...
(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.
latest release is 3.6
acl2-4.2.ebuild in science overlay
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.