OBSERVATION

print an observation 
Major Section:  ACL2-BUILT-INS

Here is a typical application of observation. 

ACL2 !>(let ((ctx 'top-level)
             (name 'foo))
         (observation ctx
                      "Skipping processing of name ~x0."
                      name))

ACL2 Observation in TOP-LEVEL:  Skipping processing of name FOO.
<state>
ACL2 !>
Observation prints an initial ``ACL2 Observation...: '', and then prints the indicated message using formatted printing (see fmt). Notice in the example above that evaluation of a call of observation returns state. Indeed, observation is actually a macro whose expansion takes and returns the ACL2 state. A similar utility, observation-cw, is available that does not take or return state; rather, it returns nil as the suffix ``cw'' suggests that a ``comment window'' is the target of this printing, rather than the state. For example: 
ACL2 !>(let ((ctx 'top-level)
             (name 'foo))
         (observation-cw ctx
                         "Skipping processing of name ~x0."
                         name))

ACL2 Observation in TOP-LEVEL:  Skipping processing of name FOO.
NIL
ACL2 !>
Observation-cw takes exactly the same arguments as observation, but observation-cw does its printing in a so-called ``wormhole''; see wormhole. 

General Forms:
(observation    ctx fmt-string fmt-arg1 fmt-arg2 ... fmt-argk)
(observation-cw ctx fmt-string fmt-arg1 fmt-arg2 ... fmt-argk)
where ctx generally evaluates to a symbol (but see below), and fmt-string together with the fmt-argi are suitable for passing to fmt. Output begins and ends with a newline.

Recall from the example above that the output from a call of observation (or observation-cw) begins with ``ACL2 Observation'' and additional characters ending in ``: '', for example `` in TOP-LEVEL: '', followed by formatted output produced from fmt-string with the given fmt-argi. The characters printed immediately following the string ``ACL2 Observation'' depend on the value of ctx. If ctx is nil, nothing is printed. If ctx is a non-nil symbol, it is printed using fmt directive ~x. If ctx is a cons pair whose car is a symbol, formatted printing is applied to the string "(~x0 ~x1 ...)", where #\0 and #\1 are bound respectively to that car and cdr. Otherwise, ctx is printed using fmt directive ~@.

We next discuss situations in which printing is inhibited for observation and observation-cw. No printing is done when observation is among the inhibited output types; see set-inhibit-output-lst. Moreover, no printing is done by observation during include-book. If you want to avoid printing from observation-cw during include-book, then you need to manage that yourself.