Major Section: TRACE
A trace evisc-tuple, which is set by this utility, provides a means to
restrict printing during tracing. By default the ACL2 trace mechanism,
trace$
, automatically deals with stobjs, the logical world, and certain
other large structures. See trace$, in particular the documentation of
trace$
option :hide
. However, even with that default behavior you
may want to restrict what is printed according to the print-level and
print-length of an evisc-tuple; see ld-evisc-tuple.
Examples:; Set trace evisc tuple to a standard value, using current Lisp *print-level* ; and *print-length* variables: (set-trace-evisc-tuple t)
; Set trace evisc tuple back to its default: (set-trace-evisc-tuple nil)
; Set trace evisc tuple to restrict print-level to 3 and print-length to 4, ; while hiding the logical world and suitably printing stobjs even if trace$ ; option ``:hide nil'' is used. (set-trace-evisc-tuple (evisc-tuple 3 4 (trace-evisceration-alist state) nil))
General Forms:
(set-trace-evisc-tuple nil) ; default trace evisc-tuple set to standard value (set-trace-evisc-tuple t) ; default trace evisc-tuple set to hide the ; logical world and deal with stobjs even when ; trace$ option ``:hide nil'' is supplied (set-trace-evisc-tuple evisc-tuple) ; default trace evisc-tuple set to evisc-tuple
See trace$ for a discussion of ACL2 tracing. The evisc-tuple (e.g.,
see ld-evisc-tuple) used by that trace utility is the one last installed by
set-trace-evisc-tuple
-- initially to the default of nil
--
unless overriden by trace option :evisc-tuple
.
Remark. If you use value t
, then ACL2 will ensure that the logical
world and stobjs are kept up-to-date in the trace evisc-tuple.