Developers-guide-programming
Programming Considerations
This chapter discusses some things to keep in mind when modifying
the ACL2 sources. It is not intended to discuss any particular aspects of the
ACL2 source code, but rather, to highlight some general principles.
ALL OF THIS TOPIC IS VERY IMPORTANT.
Keep the user in mind
Error and warning messages take time to write, but can (obviously) be
really helpful to users. Avoid trying to say too much in one message, instead
pointing to one or more documentation topics for elaboration if
appropriate.
It is generally fine to change a system utility's behavior or even to
delete its definition. However, this is discouraged if that utility is
documented; otherwise there could be an annoyed user who is adversely
affected.
Program defensively
It is a good idea to look for precedents. See also the discussion of
precedents in the topic, developers-guide-maintenance.
Add assertions and errors when appropriate. For example, the function
all-runes-in-ttree contains a large case expression, which covers
each tag that could occur in a tag tree. The last case is an error whose
message mentions the bad tag together with the values associated with that
tag.
Check invariants. For example, the function check-acl2-initialization
checks some properties that are expected to hold at the end of a build; in
particular, it calls check-none-ideal, which reports logic-mode
functions that are not guard-verified. (If a logic-mode function is
not guard-verified, then it may run slowly. We don't want built-in functions
to run slowly.)
Use installed worlds
Fundamental utilities for ACL2 programmers are the function, getprop, and its associated abbreviation, getpropc. Getprop is
defined in the logic to walk through a given logical world, much as
assoc walks through a given association list. However, getprop
is defined ``under-the-hood'' with raw Lisp code (see the discussion of
acl2-loop-only in developers-guide-background) so that if the
world is what we call ``installed'', typically (w state), then access is
essentially constant-time. The ACL2 utilities set-w, set-w!,
extend-world, and retract-world all may be invoked to install
worlds, but it is rarely necessary or even advisable to call these directly.
They are typically used in the implementations of events.
Typically, ACL2 system programming passes along worlds that are installed,
and one needn't think about whether a world is installed or not. A major
exception is when code recurs through the world, looking for a suitable
triple. Consider the source code definition of new-verify-guards-fns1;
we include an elided version of it here.
(defun new-verify-guards-fns1 (wrld installed-wrld acc)
(declare (xargs :guard ...))
(cond ((or (endp wrld) ...)
...)
((and (eq (cadar wrld) 'symbol-class)
(eq (cddar wrld) :COMMON-LISP-COMPLIANT)
(getpropc (caar wrld) 'predefined nil installed-wrld))
(new-verify-guards-fns1 (cdr wrld)
installed-wrld
(cons (caar wrld) acc)))
(t (new-verify-guards-fns1 (cdr wrld) installed-wrld acc))))
We may reasonably assume from its name that the argument
installed-wrld is an installed world. That's a good thing, since it
guarantees that the getpropc call above will be fast. Suppose, by
contrast, that the definition had been made in the following, more
``straightforward'', manner.
(defun BAD-new-verify-guards-fns1 (wrld acc)
(declare (xargs :guard ...))
(cond ((or (endp wrld) ...)
...)
((and (eq (cadar wrld) 'symbol-class)
(eq (cddar wrld) :COMMON-LISP-COMPLIANT)
(getpropc (caar wrld) 'predefined nil wrld))
(BAD-new-verify-guards-fns1 (cdr wrld)
(cons (caar wrld) acc)))
(t (BAD-new-verify-guards-fns1 (cdr wrld) installed-wrld acc))))
As we cdr down the given world, we deal with worlds that are not the
installed world. The getpropc call will then need to walk linearly
through its world until it finds the desired property — typically very
far from constant-time behavior.
Note that there are occasions for which the world is extended a bit before
properties are obtained, and that's fine. For example, in the source code
definition of function chk-acceptable-defuns1 we find a call
(putprop-x-lst1 names 'symbol-class symbol-class wrld1), which
contributes to an extension of wrld1 that will ultimately be used for
definitional processing, including the termination proof. The prover makes
many calls of getprop (typically via getpropc) on that extended
world. Normally this isn't a problem: getprop will then walk linearly
through the new part of the world but will soon hit the installed world, and
then finish its work quickly. When large mutual-recursion nests are
involved, this could be problematic, except that this issue is taken care of
by the big-mutrec hack; see for example the definition of
defuns-fn1. But we're getting into the weeds now; our point is that
getprop and getpropc do best with worlds that are installed or are
modest extensions of installed worlds.
More generally, program efficiently
Program with tail-recursion when possible, as tail-recursive functions are
less likely to cause stack overflows and might also execute more
efficiently.
Undoubtedly there are many other tips that could be given here on efficient
programming. Maybe they'll be added over time.
Write good comments
This is a matter of taste, and tastes vary. Probably we can all agree that
obvious bits of simple code need not be commented; for example, the code
(append lst1 lst2) does not need a comment ``concatenate the two
lists''. At the other extreme, probably we can all agree that a complex
algorithm deserves a comment. When in doubt it might be best to write a bit
too much rather than a bit too little. A good guiding principle is to imagine
yourself reading the code ten or twenty years later; will it make sense?
NOTE: If a comment is worth putting into a git commit message, then it's
probably worth putting into the source code or documentation.
Use good names
For new names, avoid common strings so that it's easy to tags-search for
them later. Good examples include "rune" and "pspv" for the
data structures, ``RUle NamE'' and ``Prover SPecial Variable'' (see the record
prove-spec-var). (With the Emacs command meta-x tags-apropos you
can see many function names that mention include these two strings.) A
thesaurus such as thesaurus.com may be
helpful in naming a notion.
Do not abbreviate excessively. Good naming examples may be found in the
fields of the record prove-spec-var. These fields are not well
commented, but the names are helpful; for example, the field name
user-supplied-term is suggestive of the contents of that field, i.e., the
term supplied to the prover by the user. For another example, the function
rewrite-with-linear hints at its purpose, which is to use linear
arithmetic during rewriting. If we see a call of this function we can get a
sense of what it's about. That would be more difficult if the function were
named rwl.
But this is a matter of taste. For example, the function
assume-true-false hints at its functionality, which, roughly speaking, is
to extend a type-alist by assuming an IF test either true or
false. So why is there a function mv-atf? This is not such a huge
transgression, since it's only used in the implementation of
assume-true-false, so if you see it then your head is probably in a place
where the abbreviation atf makes sense.
Add tests
This is something that could probably be done more often; as of this
writing, unit testing of specific features is relatively rare or in Lisp
comments. The community-books directories books/system/tests/ and
books/demos/ are places to put small, specific tests, and others exist
elsewhere, for example, the four test files
books/misc/defabsstobj-example-*.lisp. So there really aren't specific
places to place tests. If you run the following command in the books/
directory, you will find that there are likely well over 100 books that do
some sort of testing, albeit not necessarily of specific features implemented
in the ACL2 source code (159 of these as of this writing).
find . -name '*test*.lisp' -print | fgrep -v quicklisp | wc -l
In general, be careful
Of course, that's easier said than done! But please, at the least, make
some effort to avoid introducing inefficiencies, unclear code, or (especially)
unsoundness.
Let us consider one example: the question of whether to skip certain checks
when proofs are skipped. You may want to look for precedents (as discussed
above). You may find that when (ld-skip-proofsp state) is
'include-book or 'include-book-with-locals, the function
load-theory-into-enabled-structure avoids a call of
chk-theory-invariant (actually shown as chk-theory-invariant@par;
see the discussion of ACL2(p) in the chapter, developers-guide-background). Thus, theory invariants are checked
when (ld-skip-proofsp state) is t, i.e., when we are skipping proofs
but not including a book (as discussed in the chapter, developers-guide-logic). The idea here is that when including a certified
book, we check theory-invariants just once, at the end of the book inclusion
process, for efficiency. So one way to be careful is to do various checks
even when (ld-skip-proofsp state) is t, even if these checks are to
be skipped when including books.
NEXT SECTION: developers-guide-prioritizing
