• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
        • Pl
        • Command
        • Puff
        • Pc
        • Ld-history
        • Oops
        • Extend-pe-table
        • Ubt
        • Puff*
        • Ubi
        • Undo
        • Make-termination-theorem
        • Pe
        • Command-descriptor
        • Gthm
        • Reset-prehistory
        • Formula
        • Pr
        • Pcb
        • Ubu
        • Disable-ubt
        • Pl2
        • Enter-boot-strap-mode
        • Pbt
        • Reset-kill-ring
          • Ubt!
          • U
          • Tthm
          • Pf
          • Ubu!
          • Pr!
          • Pcs
          • Pcb!
          • Get-command-sequence
          • Exit-boot-strap-mode
          • Ubu?
          • Ubt?
          • Ep-
          • Ubt-prehistory
          • Tau-database
          • Ep
          • Pe!
        • Parallelism
        • Programming
        • Start-here
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • History

    Reset-kill-ring

    Save memory by resetting and perhaps resizing the kill ring used by oops

    By default, ACL2 holds on to old logical worlds when you undo commands (see ubt), as documented elsewhere; see oops. You can free up memory by deleting those old worlds using reset-kill-ring.

    Examples:
    (reset-kill-ring t state)   ; replace each element of the kill ring by nil
    (reset-kill-ring 2 state)   ; create a new kill ring of '(nil nil)
    (reset-kill-ring 0 state)   ; create a new kill ring that is empty
    (reset-kill-ring nil state) ; just return the length of the kill ring
    
    General form:
    (reset-kill-ring n state)

    where n evaluates either to t, to nil, or to a nonnegative integer (a natp). If n evaluates to t, it is treated as the length of the current kill ring. If n is nil, then the length k of the current kill ring is returned as a value triple (mv nil k state). If n is a natp, then the kill ring is replaced with a list of n nils.

    In particular, use (reset-kill-ring 0 state) to avoid saving any old logical worlds, at the cost of disabling the effect of the oops command.