• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
          • Note-2-8
          • Note-2-7
            • Note-2-7-bug-fixes
            • Note-2-7-new-functionality
            • Note-2-7-proofs
            • Note-2-7-other
            • Note-2-7-system
            • Note-2-7-rules
            • Note-2-7-guards
            • Note-2-7-proof-builder
          • Note-8-6
          • Note-8-2
          • Note-7-0
          • Note-8-5
          • Note-8-3
          • Note-8-1
          • Note-8-0
          • Note-7-1
          • Note-6-4
          • Note-2-9-3
          • Note-2-9-1
          • Note-8-4
          • Note-7-2
          • Note-6-5
          • Note-4-0
          • Note-2-9-2
          • Note-3-6
          • Note-3-3
          • Note-3-2-1
          • Note-3-0-1
          • Note-2-9-5
          • Note-2-5
          • Note-1-5
          • Note-6-1
          • Note-4-3
          • Note-4-2
          • Note-4-1
          • Note-3-5
          • Note-3-4
          • Note-3-2
          • Note-3-0-2
          • Note-2-9-4
          • Note-2-9
          • Note-1-8
          • Note-1-7
          • Note-1-6
          • Note-1-4
          • Note-1-3
          • Note-7-4
          • Note-7-3
          • Note-6-3
          • Note-6-2
          • Note-6-0
          • Note-5-0
          • Note-8-7
          • Note-1-9
          • Note-2-2
          • Note-1-8-update
          • Note-3-5(r)
          • Note-2-3
          • Release-notes-books
          • Note-3-6-1
          • Note-1-2
          • Note-2-4
          • Note-2-6
          • Note-2-0
          • Note-3-0
          • Note-3-2(r)
          • Note-2-7(r)
          • Note-1-1
          • Note-3-4(r)
          • Note-3-1
          • Note-2-8(r)
          • Note-2-1
          • Note-2-9(r)
          • Note-2-6(r)
          • Note-3-1(r)
          • Note-3-0(r)
          • Note-3-0-1(r)
          • Note-2-5(r)
          • Note-4-3(r)
          • Note-4-2(r)
          • Note-4-1(r)
          • Note-4-0(r)
          • Note-3-6(r)
          • Note-3-3(r)
          • Note-3-2-1(r)
        • Version
        • Acknowledgments
        • Pre-built-binary-distributions
        • Common-lisp
        • Git-quick-start
        • Copyright
        • Building-ACL2
        • ACL2-help
        • Bibliography
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Note-2-7

Note-2-7-system

ACL2 Version 2.7 Notes on System-level Changes

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.