Ld-history
Saving and querying command history
See ld for background on the ACL2 read-eval-print loop. The
present topic pertains to a history kept for commands issued to that loop,
which we call an ``ld-history'' (pronounced ``ell dee history''). Here are
some things to keep in mind when reading this topic.
- Each entry in the history includes the input command, the value returned,
and other information, as explained further below.
- This is about commands, not events: that is, we are concerned with forms
that are submitted for evaluation to the top-level loop. See command.
- An entry is saved for every command submitted by the user, even if it
doesn't change the ACL2 world — e.g., (+ 3 4) — and
even if it undoes commands — e.g., :ubt.
- Keyword commands are turned into s-expressions before saving an entry; see
keyword-commands. For example, the input :ubt :x is stored in an
entry as the input (ubt ':x).
- When an entry is saved for a command C that is evaluated in the
context of a call of local, where C evaluates to an error-triple, then C is stored in the entry as (local C) unless
C is already a call of local. (Technical Aside: This behavior
supports local portcullis commands.)
- The ld-history saves entries not only for commands issued in the original
top-level loop, but also for commands issued in (recursive) calls of ld — but not during make-event expansion.
- Entries are generally saved even when there are errors. However, entries
are not saved for commands that exit with raw Lisp errors.
Also see community-books file books/demos/ld-history-input.lsp
for examples. The output from calling ld on that file (by calling the
run-script tool in books/demos/ld-history-book.acl2) is in community-books file books/demos/ld-history-log.txt.
The ld-history is a stack, represented as a list with the most recent
commands at the front. But by default ACL2 is in single-entry mode,
where the list is kept at length 1: an entry is saved in the ld-history only
for the most recent command, and the previous entry is discarded. We now
describe relevant utilities, including one that can switch to
multiple-entry mode, where all entries are kept until a utility is
called explicitly to discard old entries. Note that the mode is determined by
the length of the ld-history: single-entry mode when length 1, multiple-entry
mode when length 2 or more.
- (ld-history state)
This utility returns a list of structures, denoted ``ld-history entries'',
with the most recent one first. By default, this list has length 1, but that
can be changed; see adjust-ld-history below. Each entry in the list is
recognized by the following predicate. NOTE: This query is evaluated
before the ld-history stored in the ACL2 state is updated with a new entry,
based on the current command; so the previous command will be at the top of
the returned stack, not the current command. (In particular, submitting the
form (ld-history state) at the ACL2 prompt does not put that form at the
front of the returned list.)
- (weak-ld-history-entry-p x)
This function returns t if x has the shape of an entry in the
ld-history list, else nil.
- Here are accessors for an ld-history entry, which we think of as returning
its fields. The formal parameter entry below is an entry in (i.e.,
member of) (ld-history state); an example call is thus
(ld-history-entry-input (car (ld-history state))).
- (adjust-ld-history x state)
X is t, nil, or an integer. The result is an error-triple (mv nil value state), where value and the effect are
as follows, and where if there is no change (i.e., the effect is a no-op) then
value is (:no-change :length N) where N is the current length
of the ld-history.
- T:
Change to multiple-entry mode, where an entry is saved for every command, not
just the most recent command. There is no change if already in multiple-entry
mode; otherwise the returned value is (:saving-ld-history t).
- NIL:
Change to single-entry mode, where an entry is saved only for the most recent
command. There is no change if already in single-entry mode; otherwise the
returned value is (:saving-ld-history nil), and all old entries will
be discarded (to produce a single-element ld-history).
- Positive integer k:
Replace the current ld-history by its first k entries, except there is no
change if in single-entry mode or if k is not less than the length of the
current ld-history. Note that by ``current ld-history'' we refer to the
ld-history in effect at the time adjust-ld-history is invoked, which does
not include the current command being evaluated. (Thus, even if k is 1,
multiple-entry mode will be preserved: the ld-history will have 2 entries
immediately after the current command completes.) The returned value is
(:ld-history-truncated :old-length LEN :new-length k), where LEN is
the length of the current ld-history before the change.
- Negative integer -k:
This is intended to specify removal of the oldest k entries from the
current ld-history. Thus, it is treated identically to argument k2 where
k2 is the sum of -k and the length of the current ld-history, but
only if that sum is positive; else there is no change. For example, suppose
that -k is -3. If the current ld-history, h, has length 2 or 3,
then there is no change; but if h has length 10, then it is to be
replaced by (take 7 h) and the length will actually thus be 8 after the
current command completes.
Note that a call of adjust-ld-history is not an event that can
be placed directly in books or encapsulate forms.
Remark. If (adjust-ld-history n state) is evaluated while in
multiple-entry mode, where n is a positive integer less than the current
length of the ld-history, then the new ld-history after returning to the
prompt will have length n+1. That's essentially because it will have
length n immediately after that call of adjust-ld-history is
evaluated, and then a new entry for the current command (which could be that
call itself, if that's what was submitted at the prompt) will be pushed onto
the ld-entry just before returning to the prompt. We say ``essentially''
because there is a Special Case: when n is 1 then a 2-element list of
entries (e1 e2) is created where e2 has fields that are all
nil; then when the new entry e is pushed onto the ld-history,
e2 is dropped so that the new ld-history is (e e1). This
special-case trick is also used in multiple-entry mode when n is -k
where k is one less than the length of the current ld-history, since that
is treated the same as (adjust-ld-history 1 state); and this trick is
also used when (adjust-ld-history t state) switches from single-entry
mode to multiple-entry mode. End of Remark.
Finally we discuss the user-data field of a ld-history entry, which (as
noted above) has default nil. It is accessed using
(ld-history-entry-user-data entry). It is set automatically when
the ld-history is extended with a new entry: the function call
(set-ld-history-entry-user-data input error-flg stobjs-out/value state),
is executed where the actuals are the other fields of the entry as indicated,
e.g., the first actual is the input field of the new entry
(as returned by the function, ld-history-entry-input). Although
set-ld-history-entry-user-data returns nil by default, this can be
changed by providing your own function with a :guard of t
and the same formal parameters (which however may be renamed, other than
state). To make that change, define a function, which here we call
my-user-data, and then attach it to set-ld-history-entry-user-data,
as follows.
(defun my-set-user-data (input error-flg stobjs-out/value state)
(declare (xargs :guard t))
...)
(defattach-system set-ld-history-entry-user-data my-set-user-data)
The following example illustrates how to store the length of the ACL2 world in the user-data. Note that the world present in the state at the time the user-data is set, computed as (w state), is almost
the final world produced by the command — it is missing just one triple,
a so-called command marker.
(defun my-world-length (input error-flg stobjs-out/value state)
(declare (xargs :guard t :stobjs state)
(ignore input error-flg stobjs-out/value))
(len (w state)))
(defattach-system set-ld-history-entry-user-data my-world-length)
A subsequent inspection of the stored user-data shows the length of the
current world, for example as follows.
ACL2 !>(ld-history-entry-user-data (car (ld-history state)))
125914
ACL2 !>
Notice that we used len, not length, since the :guard specified for our function needs to be t. Alternative
definitions, which however are less efficient, are as follows.
(defun my-world-length (input error-flg stobjs-out/value state)
(declare (xargs :guard t :stobjs state)
(ignore input error-flg stobjs-out/value))
(and (true-listp (w state))
(length (w state))))
(defun my-world-length (input error-flg stobjs-out/value state)
(declare (xargs :guard t :stobjs state)
(ignore input error-flg stobjs-out/value))
(ec-call (length (w state))))
Here is how to restore the original behavior, i.e., the default where
the user-data is set to nil.
(defattach-system set-ld-history-entry-user-data
set-ld-history-entry-user-data-default)
