		Search-engine friendly clone of the ACL2 documentation.

Safe-mode

Safe-mode-cheat-sheet

Working around ``program-only'' issues

This cheat sheet gives workarounds for errors caused by attempts to evaluate executable-counterparts (see evaluation) of so-called program-only functions. This most often occurs when safe-mode is active. Recall that safe-mode can be set by (assign safe-mode t), and also is used during macroexpansion and other logical acts that might involve :program mode functions.

The problems manifest with a hard error like this:

HARD ACL2 ERROR in PROGRAM-ONLY:  The call
<term>
is an illegal call of a function that has been marked as ``program-
only,'' presumably because it has special raw Lisp code and safe-mode
is active.  See :DOC program-only for further explanation and a link
to possible workarounds.
(See :DOC set-iprint to be able to see elided values in this message.)

When the term is a call of ev-w, an unsafe hack allowing such calls is as follows. Warning: This may result in unsoundness! (On a related note: For discussion about unsoundness when converting such program-mode functions to logic mode, see program-only.)

(value :q)
(setf (symbol-function (*1*-symbol 'ev-w))
      (symbol-function 'ev-w))
(lp)

Typically that just leads to other similar errors and so you discover the call tree, each of whose functions can be handled similarly (also in raw Lisp):

(setf (symbol-function (*1*-symbol 'ev-rec))
      (symbol-function 'ev-rec))
(setf (symbol-function (*1*-symbol 'ev-fncall-rec))
      (symbol-function 'ev-fncall-rec))
(setf (symbol-function (*1*-symbol 'push-warning))
      (symbol-function 'push-warning))

Other times you may avoid the problem by defining your own utilities. For example, in safe-mode you can't use the utility without-evisc (which is useful when iprinting is active). But the following works, provided form evaluates to an error-triple.

(defmacro without-evisc-error-triple (form)
  `(state-global-let*
    ((abbrev-evisc-tuple nil set-abbrev-evisc-tuple-state)
     (gag-mode-evisc-tuple nil set-gag-mode-evisc-tuple-state)
     (term-evisc-tuple nil set-term-evisc-tuple-state)
     (ld-evisc-tuple nil set-ld-evisc-tuple-state))
    ,form))

The following log illustrates how to use this utility to avoid an error caused by without-evisc in safe-mode.

ACL2 !>(set-iprint t)

ACL2 Observation in SET-IPRINT:  Iprinting has been enabled.
ACL2 !>(assign safe-mode t)
 T
ACL2 !>(cw "Something printed with evisceration: ~X01~|"
           '((((DEEP))))
           (evisc-tuple 3 4 nil nil))
Something printed with evisceration: (((#@1#)))
NIL
ACL2 !>(without-evisc-error-triple (value '(((#@1#)))))
 ((((DEEP))))
ACL2 !>