When terms change between printings in ACL2, the user wants to find changes quickly. Two modifications to ACL2 and an (X)Emacs feature make this possible.
When a formula gets HUGE, it takes up a lot of space on the screen. Particularly, parts of formulas deep in the tree are often irrelevant to the current proof step. It would be nice to have ACL2/(X)Emacs hide this huge amount of text in a buffer to be shown when the user unhides it via the mouse or a keyboard stroke. The first modification does this exactly. Anything that is unchanged from the previously printed formula and is deeper than a default depth of seven is hidden automatically for the user to unhide.
When a formula is large, it may take the user awhile to realize how his/her formula changed from one printing to the next. A simple example would be realizing that something buried inside the formula went from (cdr x) to (cddr x). When a formula's term changes from the previous printing, it is printed in color to bring it more quickly to the user's eye. If a formula is perceived to be so different that it is not even related to the previously printed formula, colored printing is disabled for that particular printing.
I have prepared using both these options or just the hiding option. Please read at least the shorter how-to. You can either download and load/ld the patches or download the images. Either way, you need to load-file the customize-hideshow.el file after or while starting (X)Emacs. If you would like to use the patches method, download "patch-files.zip".
If you are on the local UT network, all of these files are accessible from /u/ragerdl/acl2-public/.
A short version of the how to
A long version of the how to
emacs-hiding-only.el
emacs-hiding-and-highlighting.el
You will need to make both the shell script and gcl image executable.
ACL2 2.9.1 binary built on GCL 2.6.6 - hiding only
Shell Startup Script
GCL Binary
ACL2 2.9.1 binary built on GCL 2.6.6 - hiding and highlighting
Shell Startup Script
GCL Binary
The sources below are currently for version
2.9.1
of ACL2. Just swap out the basis.lisp downloaded for the basis.lisp in the
acl2-sources directory. If you would like a 2.9.0 version, please let me know.
Hiding Only basis.lisp
Hiding and Highlighting basis.lisp