Developers-guide-emacs
Emacs As a Critical Tool for ACL2 Developers
Emacs has traditionally been used by ACL2 system developers. In
principle, any text editor would suffice. But as of this writing, we don't
know how to maintain ACL2 effectively without using Emacs. It is not the goal
here to give an Emacs tutorial; but here are some Emacs utilities that are
particularly useful to ACL2 developers.
- meta-.
Move to the indicated definition in the ACL2 sources (must
initialize with meta-x visit-tags-table). This is much faster than
bringing up the file in an editor and searching for the definition. Use a
prefix argument to find the next match if desired.
- meta-x tags-apropos
Bring up all symbols whose definition matches
the given regular expression. One can find a suitable such symbol and use
meta-. to go rapidly to its definition.
- meta-x tags-search
Find an occurrence of a given regular
expression, using meta-, to find subsequent occurrences.
- meta-x tags-query-replace
Replace occurrences of a given regular
expression with a given string, with a query each time, using meta-, to
find subsequent occurrences.
- meta-x compare-windows
After splitting the window in two
(say, with control-x 2), compare the upper window with the lower. This
is particularly useful when comparing two versions of some source code, for
example, the original version and a modified version.
The file emacs/emacs-acl2.el has many helpful utilities, so you may
want to load it in your ~/.emacs file.
- For example, it defines ctl-t w as a shortcut for meta-x
compare-windows, and it defines ctl-t q to do the same thing but
ignoring whitespace (by providing a prefix argument for meta-x
compare-windows).
- Maintain emacs/emacs-acl2.el with taste: avoid using fancy Emacs Lisp
code that could be difficult for others to maintain. If one is competent at
maintaining the ACL2 sources base, then a little Emacs Lisp competence should
be sufficient for maintaining emacs/emacs-acl2.el as well. So avoid
fancy Emacs features not already found in use in that file.
NEXT SECTION: developers-guide-background
