Developers-guide-build
Building ACL2 Executables
Building an ACL2 executable is easy: one simply submits `make'
in the top-level ACL2 directory. Here we say a few words about how that works
and comment on some variants.
Building with `make'
The preceding chapter (see developers-guide-background) notes five
or six different Lisps on which ACL2 may be built. There
have been occasions when an ACL2 bug only showed up with one of those Lisps;
so, it is a good idea to build ACL2 in each of them from time to time, when
feasible. Just specify LISP on the command line, typically with
PREFIX specified as well, which is put on the front of saved_acl2.
For example, to build ACL2 in SBCL, you might issue the following shell
command to create an SBCL-based ACL2 executable named
sbcl-saved_acl2.
(make PREFIX=sbcl- LISP=sbcl) >& make-sbcl.log&
DEMO: make-acl2 [alias].
Check the log to see if the build seems to have completed normally, in
particular with ``Initialization SUCCEEDED'' printed near the end of the log.
It is a good idea to do case-insensitive searches for the string,
"compiler", if the Lisp is CCL (you should find four occurrences, all of
them for SET-COMPILER-ENABLED) and for "warning:" for the other Lisp
implementations (you should find no occurrences except in GCL, pertaining to
``trace'').
Let us now provide some analysis of what the invocation of `make' is
doing. If you inspect GNUmakefile, you may see these two lines:
# Top (default) target:
all: large
Thus, ``make'' is really ``make all'', which is mostly ``make
large''. (There was formerly a way to build smaller executables, but no
longer.) That target, in turn, is defined as follows.
large: acl2r full init
Let's briefly consider each of the three targets above. For details, read
GNUmakefile, which is intended to be comprehensible.
- The acl2r target just generates a file acl2r.lisp that is loaded
in to Lisp at start up by the other two targets. It defines features that
support readtime conditionals during the build process.
- The full target compiles source files when compilation is indicated.
Compilation is skipped for host Lisps CCL and SBCL because those Lisps compile
on-the-fly, hence there is no clear advantage to compiling the source
files.
- The init target generates a call of initialize-acl2, which
constructs the initial world — the so-called ``boot-strap world''
— by running ld on ACL2 source files.
Not surprisingly, there are many details that we omit here. We expect ACL2
developers to be able to follow the source code and GNUmakefile where
they lead when it is important to understand details.
Debugging a failed build
When a build fails using ``make'', you can generally re-create the
failure in an interactive session as follows, so that you can use the Lisp
debugger to investigate. First, look for a file ``workxxx'' in the build
directory. It should contain the forms that were executed in Lisp to get to
the error. So, start Lisp, and then execute each of those forms until you get
to the error — it's as simple as that! (Of course, the debugging that
ensues may be simple or complex.)
Documentation
DEMO: make-doc [alias] COVERS WHAT'S BELOW.
The generated file doc.lisp can be built in the ACL2 sources directory
by invoking make DOC or make update-doc.lisp. These each will build
that file in the ACL2 sources directory, which in turn supports the use of
:doc at the terminal without the need to include books. The way that
works is as follows: doc.lisp is generated from
books/system/doc/acl2-doc.lisp, and then doc.lisp is processed with
ld as an ACL2 source file to populate the appropriate documentation
database. That database consists of the alist,
*acl2-system-documentation*, whose keys are the built-in documented
topics.
Warning: If there are functions, macros, or constants that are keys of
*acl2-system-documentation* but do not belong to the constant
*acl2-exports*, then the community book
books/misc/check-acl2-exports.lisp will probably fail to certify. So
whenever doc.lisp is regenerated, it is a good idea to recertify that
book after deleting its .cert file.
If you include links to community-books topics in
acl2-doc.lisp, follow the suggestions in the ``Remark for Experienced
Users'' in the documentation topic, documentation.
Untouchables etc.
Note that during the build, ACL2 does not enforce its usual restrictions
against using untouchables or utilities in the list
*ttag-fns-and-macros*. Be careful! Those restrictions are in place
because their use can destroy the integrity of an ACL2 session. As
developers, we can't be hampered by such restrictions, but in return for this
freedom we take responsibility for wise usage.
Build-time proofs
ACL2 has the ability to ``prove its way through'' some of its source code.
Most proofs are skipped by default. To do such proofs, run `make proofs', which should be done only after
compiling the sources if that would normally be done for the host Lisp that is
being used. To be safe it might be best to build ACL2 first the normal way,
even if CCL or SBCL is being used and hence sources aren't subjected to
compile-file.
Proving termination and guards in books: Making a ``devel'' build
[JUST TOUCH ON THIS SECTION]
Just above, we talk about doing proofs during the build. That is an
admirable thing to do, but it can be difficult to carry out certain proofs,
for at least two reasons: the build environment is not interactive, and there
is no way to include helpful books during the build. Fortunately, there is a
procedure for deferring those proofs until after the build is complete. The
documentation topic verify-guards-for-system-functions provides
details. However, after you have some familiarity with
this procedure you might prefer to follow a script given as a comment in
*system-verify-guards-alist*.
NEXT SECTION: developers-guide-maintenance
