MEMORY REQUIREMENTS. We have successfully run a small but nontrivial test suite on a Sparc 2 with 16 megabytes of main memory, but performance appears to be somewhat better with more memory. See PROBLEMS near the end of this file for further details.
Roughly speaking, getting ACL2 up on your system involves (a) obtaining the sources, (b) creating an executable binary image from the sources, and (c) testing the image. The documentation for ACL2 is among the source files and is discussed further below in DOCUMENTATION.
You may obtain the sources and certain executable image files via the Web, ftp, or magnetic tape. If we do not distribute an appropriate image, we tell you below how to build it from the sources.
Download the gzip'd tar source file for the most recent version.
This `make' works for the Common Lisps listed in SYSTEM REQUIREMENTS. It may only work on Sun Sparcs and 486/66 PCs, for all we know about the portability of Unix `makefile' code. See the file makefile for further details. If this `make' command does not work for you, please see the instructions for NON-UNIX systems below.
You can now skip to the section GETTING INTO THE ACL2 COMMAND LOOP.
You will find that /pub/acl2/v1-9/acl2-sources contains many files, subdirectories, sub-subdirectories, etc. We mean for you to copy over to your local connected directory the entire structure of files and subdirectories. Thus, when this ftp operation is done, your local connected directory should have a subdirectory named acl2-sources and it should contain (at some level) everything obtained by the ftp. Your local acl2-sources subdirectory will now look exactly as though you had obtained our acl2.tar.gz and done the gunzip, tar and rm steps of the UNIX INSTALLATION INSTRUCTIONS.
Next we describe how to create a suitable binary image containing ACL2. This takes some time and you should know how to save the resulting image so that it does not have to be constructed from scratch each time you wish to use ACL2. The time taken to carry out the initialization process depends on the host processor but may be an hour or two. The size of the resulting binary image is dependent on which Lisp was used, but it may be in the vicinity of 15 megabytes. See the file "mcl-acl2-startup.lisp" for Macintosh directions.
Invoke your local Common Lisp, which should be one of those listed in SYSTEM
REQUIREMENTS. Filenames in this Lisp session should default to the
acl2-sources directory, e.g., for GCL, connect to the acl2-sources directory
before invoking GCL or, after entering GCL, do
(si::chdir "
Then type the following sequence of Lisp commands,
(load "acl2.lisp")
(in-package "ACL2")
(compile-acl2)
The commands above will compile the ACL2 sources and create compiled object
files on your acl2-sources subdirectory. Now exit your Common Lisp and invoke
a fresh copy of it (mainly to avoid saving an image with the garbage created by
the compilation process). Again arrange to connect to the acl2-sources
subdirectory. In the fresh lisp type:
(load "acl2.lisp")
(in-package "ACL2")
(load-acl2)
(initialize-acl2)
This will load the new object files in the Lisp image and bootstrap ACL2 by
reading and processing the source files. But the attempt at initialization
will end in an error! The message will say that it is impossible to finish
because a certain file was compiled during the processing, thus dirtying the
image yet again. So now exit your Common Lisp and invoke a fresh copy of it
(again arranging to connect to your acl2-sources subdirectory). Then, in the
fresh lisp type:
(load "acl2.lisp") ; (load "acl2-init.lisp") ; if to use our save
(in-package "ACL2")
(quick-compile-acl2 t t)
(initialize-acl2)
This will load the new object files into the Lisp image, and bootstrap ACL2 by
reading and processing the source files. This run will succeed and leave you
at the top level of your Lisp. However, if you invoke (LP) you will enter the
ACL2 command loop.
We recommend that you save the resulting image to an executable file using
whatever save mechanism exist in your Common Lisp. For consistency with the
QUICK AND EASY INSTALLATION INSTRUCTIONS, above, we suggest you save the binary
image to the file named
ACL2 !>
Typically after typing an ACL2 term, you must type a `
Some images start up in our command loop. Others start up in the host Common
Lisp. If your image starts in Common Lisp, you get into the ACL2
command loop by executing the Common Lisp function (ACL2::LP) or,
simply, (LP) if the current package is "ACL2".
To get out of the ACL2 command loop, type the form :q to it. This returns you
to the host Common Lisp. You may re-enter the command loop with (LP) as above.
Note that when you are in the host Common Lisp you can overwrite or destroy
ACL2 by executing (in)appropriate Common Lisp.
:mini-proveall
This will cause a moderately long sequence of commands to be processed, each of
which is first printed out as though you had typed it. Each will print some
text, generally a proof of some conjecture. None should fail.
We distribute several files of definitions and theorems with ACL2. These
``books'' have been contributed mainly by users and are on the subdirectory
acl2-sources/books. See acl2-sources/books/README for information. The
general topic of books is discussed thoroughly in the ACL2 documentation; see
the BOOKS node in the documentation tree.
Books should be `certified' before they are used. We do not distribute
certificates with our books. You should generate them locally as a test of
your ACL2 image.
It is easy to re-certify all the distributed books in Unix. We recommend you
do this. While connected to the acl2-sources directory, execute
make certify-books-test
This will create several megabytes of output and take several hours. To remove
the output, stand in the same directory as above and execute:
rm -f books/*.log
rm -f books/*/*.out
rm -f books/*/*.log
We apologize to non-Unix users: we do not provide non-Unix instructions for
recertifying the distributed books. The certification methods provided by the
authors of the books vary greatly and we codified them in the Unix makefile
used above. Most subdirectories of acl2-sources/books contain either a README
file or a certify.lisp file. Users who wish to certify one of these books and
who cannot figure out (from these scant clues) what to type to ACL2 should not
hesitate to contact the authors.
Two Web-based guided tours of ACL2 are available from the home page noted
below. If you are already familiar with Nqthm, you might find it useful to
look at the documentation node NQTHM-TO-ACL2. Another useful documentation
topic for beginning ACL2 users is the node TUTORIAL.
ftp://dirleton.csres.utexas.edu/pub/acl2/v1-9/acl2-sources/doc/HTML/acl2-doc.html
The home page provides a selected bibliography, guided tours of the system, the
complete hypertext documentation tree, and instructions for obtaining the
sources via a Web browser.
Once you install ACL2 (as described above) the html form of the documentation
is available locally as acl2-sources/doc/HTML/acl2-doc.html.
IMPORTANT NOTE: If you have installed ACL2, we urge you to browse your local
copy of the documentation rather than our Web copy, simply to reduce Web
traffic and the demand on our ftp machine.
meta-x info
and then, if you are unfamiliar with Info, type
control-h m
to see a list of commands available. In particular, type
g (
to enter the ACL2 documentation. Alternatively, your system administrator can
add an ACL2 node to the top-level Info menu. The appropriate entry might read:
* ACL2 1.9: (
If you are using Lucid Emacs instead of Gnu Emacs, you will find it
more aesthetic to use
Note: The Emacs Info and Postscript versions of our documentation were created
using the file acl2-sources/doc/texinfo.tex, which is copyrighted by the Free
Software Foundation, Inc. (See that file for copyright and license
information.)
acl2-sources/doc/TEX/acl2-book.ps.
The file currently prints out as about 800 pages. There is an index, followed
by a Table of Contents, both at the end of the document. The corresponding
.tex file is also provided.
make large LISP=xxx
while connected to the acl2-sources directory. The `xxx' above should be
replaced by the name of your local Common Lisp. This will create
For non-Unix systems, the ``large'' image can be built in your local Common
Lisp by
(load "acl2.lisp")
(in-package "ACL2")
(compile-acl2 nil)
(load-acl2 nil)
(initialize-acl2 'include-book *acl2-pass-2-files* nil)
When done, save the image to an executable binary file.
Once you have an image of ACL2 containing documentation strings, and you are in
the ACL2 command loop, you may query the documentation on a given topic
by typing the command
:doc
where
README ; This file
acl2-sources/
LICENSE ; Current version of license
README ; This file, same as in parent directory except that updates may
; not show up in the version in the acl2-sources/ directory.
TAGS ; Handy for looking at source files with emacs
*.lisp ; ACL2 source files.
all-files.txt ; List of all files in this directory and subdirectories
books/ ; Examples, potentially useful in others' proofs. See books/README.
doc/ ; ACL2 documentation in various formats
emacs/ ; Miscellaneous emacs and file utilities, not well documented
init.lsp ; Useful for building the system.
interface/
emacs/ ; Support for ACL2 "proof trees". See interface/emacs/README.doc.
infix/ ; ACL2 infix printer by Mike Smith. See interface/infix/README.
makefile ; For Unix make. See README.
reports/ ; Some written material on ACL2 besides the documentation.
saved/ ; Empty directory for backing up copies during make; not important
acl2.tar.gz; gzip'd tar file containing all of acl2-sources/ (see below)
acl2.tar.gz.SUM ; result of our running sum acl2.tar.gz
images/ ; Some gzip'd tar'd executables; see images/README.
split/ ; The result of splitting up acl2.tar.gz; see split/README
cat split-acl2.tar.gz* > acl2.tar.gz
If you are using Version 3.2.0 of Lispworks, there is probably a bug in
the definition of logeqv. Harlequin has sent us a patch; if anyone asks us for
it, we will ask Harlequin if we may forward their patch.
If you are running on GCL or AKCL on a machine with only 16 megabytes of RAM,
it may be a good idea to have a file ~/acl2-init.lsp containing the following
form, which will help to keep the ACL2 process small as you are running it:
(setq acl2::*acl2-allocation-alist* nil).
In one test on a not-quite-current version of the system, we found the
following times (minutes:seconds) using a Sparc 2.
31:42 64 megabytes main memory
33:37 64 megabytes main memory, using the SETQ form above
63:52 16 megabytes main memory
43:09 16 megabytes main memory, using the SETQ form above
If you are running Linux Slackware v3.0:
1 Fetch GCL v2.2 plus fixes. Install it using the standard makefile.
The GCL v1.0 binaries that come with Slackware were not built
correctly (it fails to load compiled *.o files).
2 Add the following lines at the end of acl2_sources/init.lsp
#+gcl
(setq COMPILER::*SPLIT-FILES* 100000)
This way the lisp compiler splits large C source files in files of
about 100K. Without this line, some systems do not have enough
memory to compile the C files. (We saw this problem arise on a
machine with 16Mb of actual memory plus 16Mb of virtual memory.)
3 Install ACL2 using the standard makefile. It requires about 25Mb
of free disk space (besides space for source files).
(Thanks to Vanderlei Moraes Rodrigues for the Slackware notes.)
It is the understanding of Computational Logic, that, as of August 22, 1995,
ACL2 may be exported to any country except as follows:
- Both electronic transfer and export of magnetic tape to Iraq and Yugoslavia
require specific licensing by OFAC.
- Electronic transfer to North Korea and Libya is prohibited.
However, OFAC should be consulted for the current status of these and any
other embargoes.
GETTING INTO THE ACL2 COMMAND LOOP
ACL2 presents itself as a read-eval-print loop, where the forms read and
evaluated are ACL2 terms, not arbitrary Common Lisp. We sometimes call this
loop the ``ACL2 command loop.'' The initial prompt of the ACL2 command loop is
TESTING
After building the binary image, you should test it. The easiest test is to
type the following term to the ACL2 command loop:
DOCUMENTATION
ACL2's documentation is a hypertext document that, if printed in book form, is
about 800 pages or about 1.5 megabytes of text. Its hypertext character makes
it far more pleasing to read with an interactive browser. The documentation is
available in four formats: HTML, Texinfo, Postscript and ACL2 documentation
strings. All of this material is copyrighted by Computational Logic, Inc.
Html
The ACL2 Home Page is
Emacs Info
This is a very convenient format for accessing the ACL2 documentation from
within Emacs. In Emacs, invoke
Postscript
A Postscript file containing all the documentation is in
ACL2 Documentation Strings
The ACL2 system has facilities for browsing the documentation. However this
requires that the documentation be stored as strings in the Lisp image. To
save space, the images mentioned so far in this document, do not contain
resident documentation strings. To build such an image on a Unix system,
invoke
SUMMARY OF DISTRIBUTION
A list of all files may be found in the file all-files.txt. In addition to
that file, the distribution includes the following.
SAVING SPACE
For those really pressed for space, we note that it is not necessary to fetch
the whole `acl2.tar.gz' file in order to build acl2. That file includes more
than just the ACL2 sources proper. It suffices, for building ACL2, via the
instructions above, to fetch only the acl2-sources/*.lisp files, which take up
`only' about 5 megabytes, together with the files acl2-sources/makefile and
acl2-sources/init.lsp.
PROBLEMS
If you have difficulties with ftp time outs after establishing an ftp
connection, please try logging in again using a dash (-) as the first character
of your password - this will turn off the continuation messages that may be
confusing your ftp client. If that doesn't solve your problems, and you have
encountered problems ftping the long file acl2.tar.gz because your `get' times
out, an alternative is to get all of the many files in the directory split/,
each of which matches the pattern `split-acl2.tar.gz*' (e.g., using an `mget'
command). Once you have got all these files, concatenate them together in
alphabetic order, e.g., with the command
USEFUL ADDRESSES
If you would like to join the unmoderated ACL2 mailing list, acl2@cli.com, send
to acl2-request@cli.com a message containing as its body (NOT its Subject) the
the single word `subscribe'. To get general information about the mailing
list, send the word `info' (this will not subscribe you to the mailing list).
To send a message to all who receive ACL2 mail, send the message to
acl2@cli.com. Finally, please report bugs in ACL2 to acl2-bugs@cli.com.
EXPORT/RE-EXPORT LIMITATIONS
ACL2 may be exported under a "General License GTDA" ("General Technical Data
Available to All Destinations") to any countries except those subject to
embargoes under various laws administered by the Office of Foreign Assets
Control ("OFAC") of the U. S. Department of the Treasury.
This page is URL http://www.computationallogic.com/software/caeti/acl2/README.html