LD-PRE-EVAL-PRINT

Major Section:  MISCELLANEOUS

Ld-pre-eval-print is an ld special (see ld). The accessor is (ld-pre-eval-print state) and the updater is (set-ld-pre-eval-print val state). Ld-pre-eval-print must be either t, nil, or :never. The initial value of ld-pre-eval-print is nil.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-pre-eval-print is one of them. If this global variable is t, then before evaluating the form just read from standard-oi, ld prints the form to standard-co. If the variable is nil, no such printing occurs. The t option is useful if you are reading from a file of commands and wish to assemble a complete script of the session in standard-co.

The value :never of ld-pre-eval-print is rarely used. During the evaluation of encapsulate and of certify-book forms, subsidiary events are normally printed, even if ld-pre-eval-print is nil. Thus for example, when the user submits an encapsulate form, all subsidiary events are generally printed even in the default situation where ld-pre-eval-print is nil. But occasionally one may want to suppress such printing. In that case, ld-pre-eval-print should be set to :never. As described elsewhere (see set-inhibit-output-lst), another way to suppress such printing is to execute (set-inhibit-output-lst lst) where lst evaluates to a list including 'prove and 'event.