Major Section: NOTE-2-7
ACL2 now runs (once again) under LispWorks, specifically, LispWorks 4.2.0. However, we needed a patch, which presumably will be unnecessary after 4.2.7. From LispWorks support:
Users with LispWorks4.2.7 should ask us at lisp-support@xanalys.com for the transform-if-node patch. It will be helpful if they quote (Lisp Support Call #11372) when doing so. Also, they must send a bug form generated from their LispWorks image: instructions at http://www.lispworks.com/support/bug-report.html.
File books/Makefile-generic has been improved so that failed attempts to
certify a book will cause the make to fail. Previously, an existing
.cert file was left in place, and that sufficed for the make to be
considered a success. Now, the old .cert file is first removed when
recertification is found to be necessary.
A change has been made to source file acl2.lisp to accommodate GCL 2.4.3.
(ACL2 Version 2.6 does not work with some versions of GCL 2.4.3.)
The error message has been improved when certain forms are typed to raw Lisp
and the ACL2 loop has never been entered (with (LP)).
The following symbols in the ACL2 package have been made untouchable, meaning
that they are not available to the user: ev-fncall, ev, ev-lst,
ev-acl2-unwind-protect, ev-fncall!, and user-stobj-alist-safe.
The reason is that these functions can not be called safely except under
certain restrictions. If you want to call the ACL2 evaluator, consider using
the built-in system functions trans-eval or simple-translate-and-eval.
CLISP Version_2.30 implements a notion of ``locking'' the "LISP" package that is incompatible with building ACL2. (CLISP Version_2.27 does not appear to have had this feature.) We have gotten around this problem by unlocking the "LISP" package in ACL2 images built on such CLISPs.
Automatic proclaiming for GCL, which has (for a long time) been done for
functions in compiled books, has been improved. Formerly, the only time a
non-trivial output type (i.e., other than t) was inferred was when
macroexpansion produced an explicit call of the. Now, if
expressions can also generate non-t output types. Consider the following
example.
(defmacro the-fixnum (n)
(list 'the '(signed-byte 29) n))
(defmacro 1+f (x)
(list 'the-fixnum
(list '1+ (list 'the-fixnum x))))
(defun foo (x)
(declare (type (unsigned-byte 27) x))
(if (zp x)
0
(1+f (foo (1-f x)))))
Formerly, the proclaim forms for foo, before and after this
improvement, are as shown below.
(PROCLAIM '(FTYPE (FUNCTION ((UNSIGNED-BYTE 27)) T) FOO)) ;old (PROCLAIM '(FTYPE (FUNCTION ((UNSIGNED-BYTE 27)) (SIGNED-BYTE 29)) FOO)) ;new
Compiler info messages sent to error stream were eliminated for CMUCL.
