ACL2 Version 2.8 News

---

• Directions have been provided for How to build/install ACL2 on GCL on Mac OS X.

  ---

• For CMUCL users: If CMUCL was installed by extracting to /usr/local/, then you will probably need a patch, which you can obtain in either of the following two ways.
  • Download a modification of function save-acl2-in-cmulisp, then replace the existing definition with this one in source file acl2-init.lisp.
  • Download a modification of the entire source file acl2-init.lisp.
  Thanks to Bill Pase for bringing this issue to our attention.

  ---

• Ray Richards noticed that there are several different definitions of firstn in the distributed books:

  books/bdd/bdd-primitives.lisp
  books/data-structures/list-defuns.lisp
  books/misc/csort.lisp
  books/ordinals/ordinal-definitions.lisp
  

  ACL2 will thus complain if you try to include two or more of the above books. You can fix the problem by modifying the definition of firstn in each of these books to be as follows:

  (defun firstn (n l)
    "The sublist of L consisting of its first N elements."
    (declare (xargs :guard (and (true-listp l)
                                (integerp n)
                                (<= 0 n))))
    (cond ((endp l) nil)
          ((zp n) nil)
          (t (cons (car l)
                   (firstn (1- n) (cdr l))))))
  

• OpenMCL and CMUCL users who use defstobj with :inline t may want to install patch file patch-defstobj.lisp. Thanks to John Matthews for bringing this problem to our attention.