• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
        • Term
        • Ld
        • Hints
        • Type-set
        • Ordinals
        • Clause
        • ACL2-customization
        • With-prover-step-limit
        • Set-prover-step-limit
        • With-prover-time-limit
        • Local-incompatibility
        • Set-case-split-limitations
        • Subversive-recursions
        • Specious-simplification
        • Defsum
        • Gcl
        • Oracle-timelimit
        • Thm
        • Defopener
        • Case-split-limitations
        • Set-gc-strategy
        • Default-defun-mode
        • Top-level
        • Reader
        • Ttags-seen
        • Adviser
        • Ttree
        • Abort-soft
        • Defsums
        • Gc$
          • Gc-verbose
        • With-timeout
        • Coi-debug::fail
        • Expander
        • Gc-strategy
        • Coi-debug::assert
        • Sin-cos
        • Def::doc
        • Syntax
        • Subversive-inductions
      • Output-controls
      • Macros
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Miscellaneous
  • ACL2-built-ins

Gc$

Invoke the garbage collector

This function is provided so that the user can call the garbage collector of the host Lisp from inside the ACL2 loop. Specifically, a call of gc$ is translated into a call of a function below on the same arguments.

Allegro CL:            excl:gc
CCL                    ccl::gc
CLISP                  ext:gc
CMU Common Lisp        system::gc
GCL                    si::gbc [default argument list: (t)]
LispWorks              hcl::gc-generation [default argument list:
                                           (7) for 64-bit OS, else (3)]
SBCL                   sb-ext:gc

The arguments, if any, are as documented in the underlying Common Lisp. It is up to the user to pass in the right arguments, although we may do some rudimentary checks.

Also see gc-verbose.

Evaluation of a call of this macro always returns nil.

To include gc$ in a book, one can use value-triple:

(value-triple (gc$))

Subtopics

Gc-verbose
Control printing from the garbage collector