This site is for community-driven development for the basic ACL2 libraries, which deal with topics like arithmetic, data structures, and hardware modelling. We're working with the authors of ACL2 and our changes are eventually incorporated into official ACL2 releases.
The statistics below correspond to runs of
regression using community books
the acl2-books project
books/clause-processors/SULFA/, for ACL2
executables built on Linux platforms as indicated. Not shown are
results of testing on Windows and Mac OS X. Each regression was run
on Ubuntu Linux.
workshops/books. The wall clock time was close to 3 hours, far exceeding all the times just below even though those include certification of the above books.
17121.010u 570.180s 2:03:26.55 238.8% 0+0k 231264+1293128io 365pf+0w
18786.760u 778.230s 1:59:34.37 272.7% 0+0k 406504+3298312io 426pf+0w
18272.610u 379.770s 2:08:32.22 241.8% 0+0k 218288+1358464io 324pf+0w
22538.290u 498.680s 2:32:32.52 251.7% 0+0k 427992+1622792io 603pf+0w
21345.800u 935.270s 1:13:29.73 505.2% 0+0k 326624+1530776io 1825pf+0w
23760.990u 494.720s 1:21:12.82 497.7% 0+0k 225960+1512856io 1523pf+0w
29884.140u 703.070s 1:40:01.15 509.6% 0+0k 477576+1812312io 2079pf+0w
23144.374u 710.308s 2:33:41.31 258.6% 0+0k 347088+3101128io 254pf+0w
27832.755u 426.454s 3:20:08.68 235.3% 0+0k 278848+1286616io 274pf+0w
63694.864u 936.738s 7:38:22.49 235.0% 0+0k 179000+1574976io 245pf+0w
ACL2 Course Materials
At some point, perhaps "ACL2 Course Materials" may be a top-level link on the
ACL2 home page. For now, we provide some links.