Version 2.9 of ACL2 is available locally for linux
machines. A version based on Gnu Common is available at ~manolios/public/acl2/v2.9-linux/gcl-saved_acl2.
A version based on Allegro Common Lisp is available at
(The above links get you to the directories in which the ACL2
executables reside only if you are running your browser on a CoC
If you want to install ACL2, look at the ACL2 Web page for
instructions. You need a common lisp compliant lisp. A free lisp
that I recommend is GCL. Perhaps the easiest thing to do is to
use one of the existing executables.
For Linux, use a GCL rpm to install GCL, and then installing
ACL2 is easy: just follow the instructions on the ACL2 Web page.
Read appendix A of Computer-Aided Reasoning (CAR) for
information on using the ACL2 system. Appendix B also contains
useful information. Finally, the Hyper-Card
for ACL2 Programming is a consise Web page with useful
information for beginners.
Emacs is the extensible, customizable, self-documenting real-time
display editor. Most ACL2 users run ACL2 inside of an Emacs shell
buffer. See Appendix A, Section A.3.5 of CAR for more
information. In addition, the subdirectory emacs of the
ACL2 distribution contains files (e.g.,
emacs-acl2.el) containing emacs commands that simplify
ACL2/Emacs interaction. Emacs is available both on the Unix
(/usr/local/bin/emacs) and Windows environments (in the
Here is a version of my emacs
file that has all the functions I will use in class.
ACL2 is built on top of Common Lisp compilers. GCL
is a the official Common Lisp for the GNU project, therefore it
is free. GCL currently compiles itself and the primary free
software Lisp applications, Maxima and ACL2, on eleven GNU/Linux
architectures (x86 powerpc s390 sparc arm alpha ia64 hppa m68k
mips mipsel), Windows, Sparc Solaris, and FreeBSD. Locally, it is
installed in the directory ~manolios/public/gcl/gcl-2.6.5.
ACL2 is built on top of Common Lisp compilers.
Allegro is the Common Lisp that I used to compile ACL2 locally.
Allegro is a commercial product of Franz Inc. Locally, it is
installed in the directory /usr/local/acl62. The
executable we will use is /usr/local/acl62/alisp. HTML
can be accessed via the URL /usr/local/acl62/doc/introduction.htm.
Last modified: Tue Oct 19 19:55:36 EDT 2004