Ld-pre-eval-filter
Determines which forms ld evaluates
Ld-pre-eval-filter is an ld special (see ld).
The accessor is (ld-pre-eval-filter state) and the updater is
(set-ld-pre-eval-filter val state). Ld-pre-eval-filter must be
either :all, :query, or a new name that could be defined (e.g., by
defun or defconst). (There is actually a value that may on
rare occasions be set by the ACL2 system, :illegal-state; we ignore that
value here, but the curious reader is welcome to see illegal-state.)
The initial value of ld-pre-eval-filter is :all.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co. Note that the ACL2 top-level loop (see lp) results from
an invocation of ld.
However, there are various flags that control ld's behavior and
ld-pre-eval-filter is one of them. If the filter is :all, then
every form read is evaluated. If the filter is :query, then after a form
is read it is printed to standard-co and the user is asked if the form
is to be evaluated or skipped. If the filter is a new name, then all forms
are evaluated until that name is introduced, at which time ld
terminates normally.
The :all filter is, of course, the normal one. :Query is useful
if you want to replay selected the commands in some file. The new name
filter is used if you wish to replay all the commands in a file up
through the introduction of the given one.
