		Search-engine friendly clone of the ACL2 documentation.

Debugging

Spacewalk

A tool that analyzes the memory usage in your ACL2 session. (CCL Only)

Signature
(spacewalk) → *

This is a debugging aide that collects and prints some space usage information to the console. Usage is simply:

(include-book "centaur/misc/spacewalk" :dir :system)
:spacewalk

You should almost certainly not include the spacewalk book in ordinary ACL2 books, since it will not help you prove anything. You could include it in your ACL2-customization file or similar. We may eventually try to integrate it into the Sidekick.

Logically (spacewalk) just returns nil. Under the hood, we call on various low-level CCL functions to analyze memory usage of various ACL2 data structures.

Definitions and Theorems

Function: spacewalk

(defun spacewalk nil
  (declare (xargs :guard t))
  (let ((__function__ 'spacewalk))
    (declare (ignorable __function__))
    (raise "Under the hood definition not yet installed?")))