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 email@example.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.
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
The following symbols in the ACL2 package have been made untouchable, meaning
that they are not available to the user:
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
expressions can also generate non-
t output types. Consider the following
(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
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.