There are several points we want to make at the outset.
Without a sense of how to use ACL2, there is significant risk that an attempt to modify its source code could be truly misguided.
There are at least the following reasons for its incompleteness.
The ACL2 source code resides on the filesystem of the Computer Science Department at the University of Texas. These files are kept in sync with the github sources, of course. So unless something goes horribly wrong with github, the sources may reasonably be said also to reside at
[JUST TOUCH ON THIS SECTION]
These essays can provide very helpful introductions, at a higher level than may be found in Lisp comments that are inside definitions. You can search for the string
; Essay on ...
by using, for example,
; Essay on make-event
If your search is case-insensitive, then you will find ``; Essay on
Make-event''. Such an essay is not necessarily complete, or even close to
being complete, but it is a good starting point before modifying source code
As of this writing there are nearly 100 such essays! This manual does not begin to cover them all; in fact it barely touches on most of them, at best. Moreover, some important components of ACL2 have no high-level essay.
Example 1. Suppose you encounter the
Example 2. What is the flow of the ACL2 waterfall? By using the
waterfall waterfall1-lst waterfall1 waterfall0 waterfall0-with-hint-settings waterfall0 waterfall-step
User-level documentation is in community book
By contrast, system-level documentation is in Lisp comments found in the
ACL2 sources and in this Guide. Those comments are geared towards
implementors; so while they are written with care, they sometimes assume
implementation-level background. For example, the word ``primitive'' is
sometimes used for any built-in function, while other times it might suggest
the more limited notion implemented by the constant
Please read the comments in a definition carefully before you modify it! In particular, there are often comments warning you to ``keep in sync'' with one or more other definitions, which need to be heeded.
It is often helpful to read user-level documentation before reading system-level documentation when preparing to modify ACL2. Often the user-level documentation will be on specific topics, such as make-event as described above. But user-level documentation may also provide general background; in particular, the topic programming-with-state is highly recommended for anyone who is considering doing system development. However, for most ACL2 system-level documentation, it is best to put it in the ACL2 sources as Lisp comments or in this Guide, rather than elsewhere in the documentation, to avoid confusing or intimidating typical users.
The topic system-utilities is a borderline case. These utilities were created for developing the ACL2 system. However, users increasingly do ``systems programming'' in ACL2; so, this topic collects some system-level utilities that may benefit such users.
Feel free to modify this guide! You can, if you like, run modifications by the acl2-devel mailing list before making changes.
Exploration of the ACL2 system is perhaps most efficient when goal-directed, i.e., when you are trying to understand specific aspects of the system. That said, a quick browse of this entire guide is recommended for ACL2 system developers.
NEXT SECTION: developers-guide-emacs