		Search-engine friendly clone of the ACL2 documentation.

Debugging

Tools for debugging failed or slow proofs, or misbehaving functions.

Subtopics

Break-rewrite: A version of the ACL2 rewriter with interactive breaks
Proof-builder: An interactive tool for controlling ACL2's proof processes.
Accumulated-persistence: To get statistics on which runes are being tried
Cgen: Counterexample Generation a.k.a Disproving for ACL2
Forward-chaining-reports: To see reports about the forward chaining process
Proof-tree: Proof tree displays
Print-gv: Print a form whose evaluation caused a guard violation
Dmr: Dynamically monitor rewrites and other prover activity
With-brr-data: Finding the source of a term in prover output
Splitter: Reporting of rules whose application may have caused case splits
Guard-debug: Generate markers to indicate sources of guard proof obligations
Set-debugger-enable: Control whether Lisp errors and breaks invoke the Lisp debugger
Redo-flat: Redo on failure of a progn, encapsulate, or certify-book
Time-tracker: Display time spent during specified evaluation
Set-check-invariant-risk: Affect certain program-mode updates to stobjs or arrays
Removable-runes: Compute runes to disable
Efficiency: Efficiency considerations
Explain-near-miss: show why a rule's pattern and the :target do not match
Tail-biting: Rewriting a true term to NIL
Failed-forcing: How to deal with a proof failure in a forcing round
Sneaky: A debugging tool for ACL2 programs. The sneaky functions allow you to save and mutate global variables, even without access to state.
Invariant-risk: Potential slowdown for program-mode updates to stobjs or arrays
Failure: How to deal with a failure to admit an event
Measure-debug: Generate markers to indicate sources of measure proof obligations
Dead-events: Using proof supporters to identify dead code and unused theorems
Compare-objects: show differences between two ACL2 objects
Prettygoals: Experimental tool for displaying proof goals in a prettier way.
Remove-hyps: Macro for defining a theorem with a minimal set of hypotheses
Type-prescription-debugging: Improve a built-in type-prescription rule
Pstack: Seeing what the prover is up to
Trace: Tracing functions in ACL2
Set-register-invariant-risk: Avoid invariant-risk checking for specified functions
Walkabout: Explore an ACL2 cons tree
Disassemble$: Disassemble a function
Nil-goal: How to proceed when the prover generates a goal of NIL
Cw-gstack: Debug a rewriting loop or stack overflow
Set-guard-msg: Specify what is printed when a guard is violated
Find-lemmas: Find lemmas that mention specified function symbols
Watch: Initiate the printing of profiling information to view in Emacs
Quick-and-dirty-subsumption-replacement-step: (advanced topic) controlling a heuristic in the prover's clausifier
Profile-all: profile essentially all functions
Profile-ACL2: profile essentially all ACL2 functions
Set-print-gv-defaults: Set default keyword values for print-gv
Minimal-runes: Compute runes to leave enabled
Spacewalk: A tool that analyzes the memory usage in your ACL2 session. (CCL Only)
Try-gl-concls: Find true conclusions using GL
Near-misses: Approximate event name matches