How to keep track of rewriting ACL2?

Here are some relevant footprint shapes created by Matt Kaufman:

(trace$ (rewrite :cond (null ancestors)
                 :entry (list 'rewrite term alist)
                 :exit (list 'rewrite (cadr values))))

(trace$ (rewrite-with-lemma
         :entry
         (list 'rewrite-with-lemma
               term
               (base-symbol (access rewrite-rule lemma :rune)))
         :exit
         (list 'rewrite-with-lemma (cadr values) (caddr values))))

(open-trace-file "my-trace-file") ; since renamed to big-trace.txt

      

        
        
        
      

    

Then run your proof you want to track

(close-trace-file)

      

        
        
        
      

    

For this example, open the trace file, my-trace-file, in your favorite text editor.

As for your second question, 80% or more of ACL2 experts will say no, you don't need to know what's going on with the rewriter. I accidentally disagree with them, so I wrote this Q&A (as I will indirectly link to it via Google). You should also look into the "break-rewrite" and "dmr" options. See the Debugging section of the ACL2 documentation for more information.