ACL2 Version 2.7 News

Executable saved images

See ftp://ftp.cs.utexas.edu:/pub/moore/acl2/v2-7/images/README.html for links to ACL2 executables. Each .md5sum file was created using md5sum. We may add additional links from time to time.

Performance comparisons

Below are times reported when "make regression-fresh" was timed on the same Linux machine for ACL2 images built on top of various Lisp implementations. We have been told that CMUCL may not do nearly this well comparatively under Solaris.

Below, the first number, User time, is probably the most relevant for comparisons. The format (from the man page) is:

         %Uuser %Ssystem %Eelapsed %PCPU (%Xtext+%Ddata %Mmax)k
         %Iinputs+%Ooutputs (%Fmajor+%Rminor)pagefaults %Wswaps