Debugging
Advice and tools for debugging performance problems and failed gl proofs.
A GL proof attempt can end in several ways. Ideally, GL will either
quickly prove your conjecture, or disprove it and show you counterexamples to
help diagnose the problem. But things will not always end so well.
Capacity Problems
- GL is running out of memory.
- Symptoms: your ACL2 process is using too much memory and your machine is
swapping, or you are seeing frequent garbage collection messages
that seem unsuccessful—that is, few bytes are freed by each GC.
- There are memory-management tools that may help to avoid these
problems. You may need to look into optimization techniques.
- GL has enough memory, but is running forever.
- You may be running into a bad case for GL's symbolic execution strategy, or
your problem may be too hard for the back-end solver (BDDs, SAT). See performance-problems for some tools and advice for dealing with these
situations.
Other Problems
- GL is failing to prove coverage.
- Symptoms: You are seeing failed ACL2 proof goals after GL says
it is proving coverage.
- It might be that your :g-bindings aren't sufficient to cover your theorem's
hypotheses, or GL's strategy for proving coverage is misbehaving. See coverage-problems for advice on debugging this situation.
- GL produces false counterexamples.
- This is easy to identify because GL will print False counterexample!
and direct you to false-counterexamples.
Subtopics
- False-counterexamples
- Coverage-problems
- Proving the coverage obligation in GL-based proofs.
- Performance-problems
- Memory-management
