Research on User Interfaces

Term Hiding and Highlighting for the ACL2 Theorem Prover

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.

The links below do not work, but you may still find the descriptions meaningful

Term Hiding

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.

Term Highlighting

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 "".

These files have been lost to the hole that is our network. It looks like someone deleted the partition storing them, and I didn't notice until recently. The reality is that it was an interesting project that was never written up or adopted. It looks to me like ACL2's gag-mode obviates the need for this technology, but I still think it was worth doing for me at the time.

How to's

A short version of the how to
A long version of the how to

(X)Emacs customization file



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

Patch files


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


Valid XHTML 1.1!