Major Section: NOTE-2-8
ACL2 now runs on OpenMCL, ``an opensourced Common Lisp implementation, derived from Digitool's Macintosh Common Lisp product.'' Thanks to Greg Wright and Robert Krug for doing most of the work for this port.
When (LP) is first executed, the underlying raw Lisp package
will change to "ACL2" (if that is not already the current package in
raw Lisp). This is a minor change that will probably not be noticed, since
up to now it has probably been the case that the ACL2 executable starts up
with "ACL2" as the underlying raw Lisp package. But this change was
made because we have been informed that ACL2 executables based on OpenMCL
need not start up with "ACL2" as the underlying raw Lisp package.
ACL2 now runs on MCL 5.0. Thanks to Pascal Costanza for updates to the
instructions in file mcl-acl2-startup.lisp and for an update to the
ACL2 sources (parameter *compiled-file-extension*).