		Search-engine friendly clone of the ACL2 documentation.

Developers-guide

Developers-guide-introduction

Introduction

This Developer's Guide is intended to provide an overview of how to maintain the ACL2 source code.

There are several points we want to make at the outset.

Experienced users only, please

Without a sense of how to use ACL2, there is significant risk that an attempt to modify its source code could be truly misguided.

This guide is highly incomplete!

There are at least the following reasons for its incompleteness.

Comments in the source code may already suffice for a given topic.
The source code is large and complex; this guide is, ideally, manageable.
At the time this manual is being created, many aspects of the system are difficult to explain because the writers have forgotten them — and that's OK!
- It is typical to read comments (which are sometimes extensive) when modifying the source code, often after reading some user-level documentation, to get up to speed. As we encounter comments that aren't clear (and correct), we fix them.

Where do the definitive sources reside?

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

https://github.com/acl2/acl2

Some longer source code comments are called ``Essays''.

[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, grep or the Emacs utility meta-x tags-search. For example, suppose you are trying to understand make-event. Then a first step might be to review its user-level documentation (for make-event and its subtopics); but after that, you could search with grep, or with a tags-search, for the following string.

; 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 that supports make-event.

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.

For example, there is no essay on induction. In such cases the relevant source comments are generally found inside definitions. For example, in the case of induction one can start with the function, induct, and read its comments and code to start exploring the rather complex ACL2 implementation of induction.

Some initiative and hacking are necessary.

Example 1. Suppose you encounter the pspv argument in the source function simplify-clause, and you don't know what that is. You can then search for pspv and you'll find the following: (access prove-spec-var pspv :rewrite-constant). Now access is a basic record-accessing utility that we do cover in this manual; and we'll also talk about the use of Emacs to find definitions. So you'll know to use the Emacs command, meta-. , to take you to the definition of the record structure, prove-spec-var. There, you'll find a few comments that explain this structure; unfortunately, however, not many. The field names can provide a clue. One of the fields is rewrite-constant, so if you're exploring the pspv because of its effect on rewriting, you can guess that this field is relevant. So let's say that you want to know about the rewrite-constant field. Using meta-. once again, you can find the rewrite-constant record structure definition; and this time there are many comments.

Example 2. What is the flow of the ACL2 waterfall? By using the Emacs command, meta-. , we can develop this call graph.

waterfall
  waterfall1-lst
    waterfall1
      waterfall0
      waterfall0-with-hint-settings
        waterfall0
          waterfall-step

User-level documentation vs. system-level documentation

User-level documentation is in community book books/system/doc/acl2-doc.lisp and appears in the acl2+books combined manual and the ACL2 User's Manual. (This Guide is an exception, of course; it is included in the acl2-books combined manual but it is at the system level, not at the user level.) See developers-guide-build for how that documentation is integrated into ACL2 builds.

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 *primitive-formals-and-guards*; the context may help in understanding the intended meaning (though perhaps, eventually, someone will use ``built-in'' for all uses of the broader notion). Sometimes an Essay (see above) may provide helpful background; indeed, comments sometimes direct the reader to an Essay.

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.

This is a living document.

Feel free to modify this guide! You can, if you like, run modifications by the acl2-devel mailing list before making changes.

Do not feel obligated to read this guide linearly, cover-to-cover!

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