• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
    • Break-rewrite
    • Proof-builder
    • Accumulated-persistence
    • Cgen
    • Proof-tree
    • Forward-chaining-reports
    • Print-gv
    • Dmr
    • Splitter
    • Guard-debug
    • Set-debugger-enable
    • Redo-flat
    • Time-tracker
    • Set-check-invariant-risk
    • Removable-runes
    • Efficiency
    • Tail-biting
    • Failed-forcing
    • Sneaky
    • Invariant-risk
    • Failure
    • Measure-debug
    • Dead-events
    • Remove-hyps
    • Type-prescription-debugging
    • Pstack
    • Set-register-invariant-risk
    • Trace
      • Trace$
      • Wet
      • Trace!
      • Break-on-error
      • Set-trace-evisc-tuple
      • Untrace$
      • Open-trace-file
      • Open-trace-file!
      • Close-trace-file
    • Walkabout
    • Disassemble$
    • Nil-goal
    • Cw-gstack
    • Set-guard-msg
    • Find-lemmas
    • Watch
    • Quick-and-dirty-subsumption-replacement-step
    • Profile-all
    • Profile-ACL2
    • Set-print-gv-defaults
    • Minimal-runes
    • Spacewalk
    • Try-gl-concls
    • Near-misses
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Trace

Set-trace-evisc-tuple

Set the trace evisc tuple

A trace evisc-tuple, which is set by this utility, provides a means to restrict printing during tracing. See evisc-tuple for an introduction to evisc-tuples; also see set-evisc-tuple and see set-iprint.

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 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 state) 
 
; Set trace evisc tuple back to its default: 
(set-trace-evisc-tuple nil state) 
 
; 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.  (Note: calling trace-evisceration-alist 
; directly requires removing this function as `untouchable', which requires a 
; trust tag; see remove-untouchable.) 
(set-trace-evisc-tuple 
 (evisc-tuple 3 4 (trace-evisceration-alist state) nil) 
 state) 
 
General Forms: 
 
(set-trace-evisc-tuple nil state) ; trace evisc-tuple set to standard value 
(set-trace-evisc-tuple   t state) ; 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 state) 
                                  ; tracing set to use indicated evisc-tuple 

See trace$ for a discussion of ACL2 tracing. The evisc-tuple used by that trace utility is the one last installed by set-trace-evisc-tuple (or by set-evisc-tuple for the trace-evisc-tuple) — initially to the default of nil — unless overridden 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.