CW

print to the comment window
Major Section:  ACL2-BUILT-INS

Example:

(cw "The goal is ~p0 and the alist is ~x1.~%"
    (untranslate term t nil)
    unify-subst)
Logically, this expression is equivalent to nil. However, it has the effect of first printing to the so-called ``comment window'' the fmt string as indicated. Thus, cw is like fmt (see fmt) except in three important ways. First, it is a macro whose calls expand to calls of a :logic mode function. Second, it neither takes nor returns the ACL2 state; logically cw simply returns nil, although it prints to a comment window that just happens to share the terminal screen with the standard character output *standard-co*. Third, its fmt args are positional references, so that for example
(cw "Answers: ~p0 and ~p1" ans1 ans2)
prints in the same manner as:
(fmt "Answers: ~p0 and ~p1"
     (list (cons #\0 ans1) (cons #\1 ans2))
     *standard-co* state nil)
Typically, calls of cw are embedded in prog2$ forms, e.g.,
(prog2$ (cw ...)
        (mv a b c))
which has the side-effect of printing to the comment window and logically returning (mv a b c).

General Form:
(cw fmt-string arg1 arg2 ... argn)
where n is between 0 and 9 (inclusive). The macro uses fmt-to-comment-window, passing it the column 0 and evisc-tuple nil, after assembling the appropriate alist binding the fmt vars #\0 through #\9; see fmt. If you want
(a) more than 10 vars,
(b) vars other than the digit chars,
(c) a different column, or
(d) a different evisc-tuple,
then call fmt-to-comment-window instead.

Also see cw!, which is useful if you want to be able to read the printed forms back in.

Finally, we discuss another way to create formatted output that also avoids the need to pass in the ACL2 state. The idea is to use wormholes; see wormhole. Below is a function you can write, along with some calls, providing an illustration of this approach.

(defun my-fmt-to-comment-window (str alist)
  (wormhole 'my-fmt-to-comment-window
            '(lambda (whs) whs)
            (list str alist)
            '(pprogn
              (fms (car (@ wormhole-input))
                   (cadr (@ wormhole-input))
                   *standard-co*
                   state
                   nil)
              (value :q))
            :ld-verbose nil
            :ld-error-action :return ; harmless return on error
            :ld-prompt nil))

; A non-erroneous call:
(my-fmt-to-comment-window "Here is ~x0 for your inspection~%"
                          (list (cons #\0 'foo)))

; An error inside the fmt string (unbound fmt var); note that even
; with the error, the wormhole is exited.
(my-fmt-to-comment-window "Here is ~x1 for your inspection~%"
                          (list (cons #\0 'foo)))

; A guard violation in the binding; note that even with the error,
; the wormhole is exited.
(my-fmt-to-comment-window "Here is ~x0 for your inspection~%"
                          (list (cons #\0 (car 'foo))))