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