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
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
To include
(value-triple (gc$))