GC$

invoke the garbage collector 
Major Section:  MISCELLANEOUS

This function is provided so that the user can call the garbage collector of the underlying 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
GCL                    si::gbc
CLISP                  ext:gc
CMU Common Lisp        system::gc
Macintosh Common Lisp  ccl::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.

This function always returns nil.