Developers-guide-maintenance
Modifying, Testing, and Debugging
Before working on changes to ACL2, consider
sending email to the acl2-devel list (acl2-devel@utlists.utexas.edu),
explaining what you have in mind. This will avoid duplication and also
provide an opportunity for feedback. In particular, you may want to wait for
confirmation from Kaufmann or Moore that at least one of them will be willing
to review your patch; otherwise they make no commitment to do so, and your
efforts might be wasted!
Please try to limit your modifications to those that are directly related
to what you intend to change. For example, please don't delete comments in a
source file or a book. (If you feel moved to do so, at least first check with
an author of the file you propose to change.) That said, it's certainly it's
fine to fix typos.
Detailed steps for making a contribution are outlined in the topic, developers-guide-contributing.
Development
The first step towards changing ACL2 is typically to create a patch file,
which here we call patch.lisp. It will typically have the following
shape.
;;; Github commit hash as of your starting ACL2 version (see below)
;;; Comments at the top (perhaps an email thread with a request for the
;;; change)
(redef+)
<your code>
(redef-)
(reset-prehistory) ; optional
The reason to record the github commit hash is so that Kaufmann and Moore
can correctly merge in your changes even after there have been several ACL2
commits. You can get that hash by running the following command under the
main ACL2 directory.
git rev-parse HEAD
Next, start copying into patch.lisp the source functions that you want
to modify. (As already noted, it is helpful for this process to use
meta-. in Emacs.) It is often best to keep the functions in order: if
f calls g and both are defined (or redefined) in patch.lisp,
then the definition of g should precede the definition of f in
patch.lisp.
Now modify those source functions and write any additional supporting
functions that you need. Try to use existing source functions when possible.
perhaps finding them by using the Emacs command, meta-x tags-apropos.
For example, to find a function that concatenates a list of strings, you could
run meta-x tags-apropos append and then search for string in the
resulting display; you would find string-append-lst, and you could run
the Emacs command meta-. on that word in order to find its definition in
the sources, to see if it has the desired functionality. You may also find it
useful to consult the documentation topic, system-utilities.
If there are further changes that you wish to make to the ACL2 source code
which are not of the form of function definitions or redefinitions — for
example, if you want to add or modify a top-level comment, or put some of the
new functions in a particular file or a newly created file, etc. — then
feel free to add instructions that reflect your intent in comments in
patch.lisp, within reason. We will be reading over patch.lisp
manually, so human-directed comments are welcome — the exact format of
patch.lisp is not rigid.
Initial testing
Test your patch by starting ACL2 and evaluating the following form in the
loop (but see below for an exception). The use of :ld-pre-eval-print is
optional, but can be helpful when debugging since it prints each form before
evaluating it.
(ld "patch.lisp" :ld-pre-eval-print t)
EXCEPTION: the form above may not work if your patch file has any
occurrences of the acl2-loop-only readtime conditional (preceded either
by #+ or by #-). In that case, run LP! as follows. NOTE: if
you are making changes that affect definition processing, then you may need to
switch the order: first load, then after (LP!), run ld.
:q
(LP!)
(ld "patch.lisp" :ld-pre-eval-print t)
:q
(load "patch.lisp") ; only needed if #-acl2-loop-only occurs in patch.lisp
(LP)
Remark (only rarely to be considered). If efficiency is a concern and you
are using a Lisp implementation that does not compile on-the-fly (as of this
writing, that includes Lisps other than CCL and SBCL), then put
(set-compile-fns t) near the top of patch.lisp, and replace (load
"patch.lisp") just above by the following (perhaps first adding
(in-package "ACL2") at the top of patch.lisp):
(load "patch.lisp")
(compile-file "patch.lisp")
(load "patch")
Now test your patch. A quick test could be the following.
(mini-proveall) ; should complete normally
(ubt! 1) ; back to just after reset-prehistory was evaluated
You might also want to do your own tests. In some cases, you could even
add a book of tests in directory books/system/tests/. If the change was
inspired by problems with a specific event in an existing book, the following
can be useful.
(ld "foo.port")
(rebuild "foo.lisp" t)
:ubt <bad-event-name>
<bad-event>
Installing and building
When you are satisfied that all is well, take your copy of ACL2 and install
the patches: for each system function redefined in patch.lisp, replace the
definition in your copy of the ACL2 sources with the redefinition, preceded by
new supporting definitions as necessary. Then in your acl2-sources directory,
build the system; see developers-guide-build.
Since ACL2 insists that functions, macros, and constants are introduced
before they are referenced, you might need to move some definitions around.
You might even need to move then to ``earlier'' files (see developers-guide-background). This is normal. Although a file name like
``rewrite.lisp'' is suggestive of its contents, and ideally the file
contains code that reflects the intent of the filename, nevertheless this is
not a rule; ACL2 implementors often need to move definitions forward in
support of other functions.
The following two additional steps are occasionally advisable, especially
for patches that change definitions that are in :logic mode.
Feel free to ask an ACL2 author if they are necessary; as of this writing,
that would be Matt Kaufmann, at kaufmann@cs.utexas.edu.
- Run ``make proofs''. That should conclude with the message,
``Initialization SUCCEEDED.''
- Do a ``devel'' build, regression, and check. See verify-guards-for-system-functions, specifically the six steps at the end of
the topic.
Regression testing
Now do a regression test. The most complete regression is done using the
regression-everything target in the top-level ACL2 sources directory, or
equivalently, the everything target in the books/ directory. Please
install a SAT solver first; see satlink::sat-solver-options.
Note that the ``everything'' level of testing may only work for CCL
and SBCL; for other Lisps, or for ACL2(p) or ACL2(r), just use the
regression target in the top-level ACL2 sources directory or,
equivalently, the all target in the books/ directory. This could
take a few hours — perhaps more than 5 hours or even more than 8 hours,
depending on the Lisp and the machine. But feel free to do only an
everything regression for ACL2 using CCL or SBCL, ignoring ACL2(p) and
ACL2(r).
make clean-books ; \
(time nice make -j 8 regression-everything) >& make-regression-everything.log&
A search for ** in the log will determine whether there have been any
failures; equivalently, in most cases, a failure has occurred when there is a
non-zero exit status.
It is a good idea to keep a record of the time it
takes to complete a regression using a given host Lisp and a given
value for the -j argument of `make'. If there is a jump of more
than a percent or two that is not attributable to book changes, then perhaps
the change is degrading performance. Of course, that time increase could be
noise; we have observed significantly more reliable timings, for example, on
Linux than on Mac. There are wonderful tools books/build/critpath.pl and
books/build/compare.pl for narrowing time increases to the level of
individual books, which you can investigate interactively, for example using
profiling; see profile-ACL2 and profile-all. (Also, Allegro CL
has a particularly nice statistical profiler.) Here is the first step, to be
run in two ACL2 directories, DIR1 and DIR2, that you want to compare
after having run a regression test in each.
cd books
find . -name '*.cert.time' -print | sed 's/[.]time$//' | sort > certs.txt
./build/critpath.pl -t certs.txt --write-costs timingfile > timing.txt
Then run the following command anywhere, which produces a file
compare.txt showing results, sorted two different ways.
<path_to_acl2>/books/build/compare.pl \
DIR1/books/timingfile \
DIR2/books/timingfile > compare.txt
Documentation
[JUST TOUCH ON THIS SECTION]
Be sure to document your changes. This will typically involve adding a
release note to a topic like note-8-2. The XDOC source code
documentation for ACL2 resides in the community book
books/system/doc/acl2-doc.lisp. If the change is not user visible, then
a Lisp comment in the corresponding defxdoc form is probably best; the
existing (defxdoc note-xxx ...) forms can provide guidance on this.
Minor output changes don't generally require any release note. Be sure to
keep the xdoc documentation at a user level, not at the level of the
implementation. Note that it is good practice to explain your changes as
noted above — that is, in the text or comments of a defxdoc
release note form — rather than merely in GitHub commit messages.
Every user should be able to find changes documented in the release notes, and
every developer should additionally be able to find pertinent Lisp comments;
neither will necessarily look back in GitHub logs (some may, but some may
not).
If your changes are related to community-books, consider adding
links to topics defined in those books as described in the ``Remark for
Experienced Users'' in the documentation topic, documentation.
Also be sure to comment your code well with Lisp comments, at an
implementation level. For example, don't say ``union is commutative'' without
explaining that you mean this with respect to set equality, not
ordinary (Lisp) equality.
Whoever actually commits and pushes to github — just Kaufmann and
Moore as of this writing, but ideally others in the future — should also
synchronize generated ACL2 source file doc.lisp (see developers-guide-build) with books/system/doc/acl2-doc.lisp.
When you add new documentation in community book
books/system/doc/acl2-doc.lisp for a symbol that is the name of a
function, macro, or constant, there is a check in the community book
books/misc/check-acl2-exports.lisp that the symbol belongs to the list,
*acl2-exports*. Rather than add the symbol immediately to that list,
however, it may be best to override the check for that symbol, as indicated in
the definition of the constant, *acl2-exports-exclusions*, in
books/misc/check-acl2-exports.lisp. The reason for this delay is that if
you change *acl2-exports*, many books may need to be recertified, which
could be inconvenient for users. This issue is documented in the definition
of the constant *ACL2-exports*; see the ``WARNING'' comment there.
Debugging
[JUST TOUCH ON THIS SECTION]
The art of debugging is... an art. Some tools that can help with debugging
are trace$, trace!, break-on-error, set-debugger-enable, walkabout, iprinting, and (rarely) disassemble$. Also see debugging.
A common way to debug an unexpected error is to invoke
(set-debugger-enable t) and (break-on-error). This may put you in
the debugger when there is an error. Each host Lisp has its own debugger
commands for looking at the backtrace; for example, in CCL the command is
:b, while in SBCL it is backtrace. CCL's debugger lets you easily
explore individual forms in the backtrace. Here is an
edited log showing how that works.
ACL2 !>(defun f (x) (declare (xargs :mode :program)) (car x))
Summary
Form: ( DEFUN F ...)
Rules: NIL
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
F
ACL2 !>(set-debugger-enable t)
<state>
ACL2 !>(f 3)
> Error: Fault during read of memory address #x1D
> While executing: F, in process listener(1).
> Type :GO to continue, :POP to abort, :R for a list of available restarts.
> If continued: Skip evaluation of (acl2::acl2-default-restart)
> Type :? for other options.
1 > :b
*(25819710) : 0 (F 3) 16
(25819770) : 1 (RAW-EV-FNCALL F (3) ('3) ((STATE . ACL2_INVISIBLE::|The Live State Itself|)) ((COMMAND-LANDMARK GLOBAL-VALUE 7662 # "/Users/kaufmann/acl2/acl2-git-scratch/books/system/doc/") (EVENT-LANDMARK GLOBAL-VALUE 9539 DEFUN F ...) (F ABSOLUTE-EVENT-NUMBER . 9539) (CLTL-COMMAND GLOBAL-VALUE DEFUNS :PROGRAM NIL ...) (TOP-LEVEL-CLTL-COMMAND-STACK GLOBAL-VALUE #) ...) NIL NIL T) 1253
(25819840) : 2 (EV (F '3) ((STATE . ACL2_INVISIBLE::|The Live State Itself|)) ACL2_INVISIBLE::|The Live State Itself| ((STATE . ACL2_INVISIBLE::|The Live State Itself|)) NIL T) 357
<<... etc. ...>>
(25819F98) : 21 (FUNCALL #'#<(:INTERNAL CCL::THREAD-MAKE-STARTUP-FUNCTION)>) 277
1 > (:form 1) ; show the form labeled with 1 in the backtrace
(RAW-EV-FNCALL 'F '# '# '# ...)
1 > (walkabout (unquote (nth 5 *)) state) ; world
Commands:
0, 1, 2, ..., nx, bk, pp, (pp n), (pp lev len), =, (= symb), and q.
((COMMAND-LANDMARK GLOBAL-VALUE 7662 ...)
(EVENT-LANDMARK GLOBAL-VALUE 9539 ...)
(F ABSOLUTE-EVENT-NUMBER . 9539)
...)
:
Some problems are, of course, more awkward to debug. One that pops up from
time to time is an error like this.
> Error: value NIL is not of the expected type NUMBER.
> While executing: CCL::+-2, in process listener(1).
That particular sort of error may indicate that the state argument of
some function was passed incorrectly, perhaps in the wrong argument
position.
In rare cases an error may occur for which the backtrace isn't helpful or
even makes little sense. Something to try is to build with safety 3, for
example as follows.
make ACL2_SAFETY=3 PREFIX=safety-3-
If your test case involves including books, then also clean the books or
use set-compiler-enabled to avoid loading their compiled files. Then
try again with the new executable; of course, if you cleaned the books, then
first recertify as appropriate using the new executable. ACL2 will run more
slowly, but in return it will do a lot more checking along the way and might
well provide a much better backtrace than before.
If you are reading this and have more debugging suggestions, by all means
consider adding them here!
Finishing up
Now feel free to send all changed files and also the starting git commit
hash (or even the entire patch file, too) for review, to whoever has offered
to look at your patch! Some day others besides Kaufmann and Moore may be
authorized to commit and push source code changes directly to GitHub; but
getting someone else to review the changes could still be a good thing to
do.
When you are ready to have your patch incorporated into ACL2, follow the
detailed steps for making a contribution outlined in the topic, developers-guide-contributing.
General guidance
We close this chapter with some relevant tips and observations, some of
which may also be found elsewhere in this Guide.
- Small examples help when testing new features or bug fixes. For a bug fix
it is important to have an example that exhibits the bug, both to guarantee
that there really is a problem and to use to test your patch. Ideally the
example will be small, as this is useful for reading the output from tracing
functions or debugger backtraces, and small examples are often helpful for
understanding the problem. Consider adding one or more relevant tests to
books/system/tests/ or perhaps, if appropriate, books/demos/.
- Often it is best to avoid making a more sweeping change than necessary,
instead waiting for users to complain. This process has several advantages:
it avoids needless code complications; the user's complaint may help to inform
the nature of the additional changes; and it may take significantly less time
to complete the implementation, especially if there is a simple fix that is
clearly correct and solves the problem.
- Look for precedents, since new code is probably more likely to be correct
to the extent it is analogous to existing code. ACL2 is a complex system with
invariants that are not always explicit, so to the extent that you can follow
the existing implementation of some feature, you may avoid introducing bugs or
undesirable behavior. For example, if you want to add a new key to the ACL2-defaults-table, find an existing such key and do a tags-search for it,
and mimic the implementation of that existing key to the extent it makes
sense. Try to pick a key that is little-used, so that the tags-search mainly
hits on the essential aspects of being a key in the acl2-defaults-table.
For another example: to arrange for adding system-attachments to the
summary, the process was to follow how hint-events is put into the
summary, so a first step was to do tags-search for ``hint-events''.
- At what point during the development of a source code change is it best to
write comments and user-level documentation? It may be good to write an
outline before coding, as a guide towards what you want. But ACL2
implementation work can be tricky, which may lead you to change the
specification slightly; so it is probably best to leave detailed documentation
until after the other work is done, including testing.
- Expect to take considerable time writing comments,
documentation, and output (e.g., for warnings and errors). These are
important and may take longer than the implementation work itself.
NEXT SECTION: developers-guide-contributing
