Tools
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
~manolios/public/acl2/v2.9-linux/allegro-saved_acl2.
(The above links get you to the directories in which the ACL2
executables reside only if you are running your browser on a CoC
machine.)
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.
Important Note: In your home directory, place
the following acl2-customization.lisp file.
If you are using your own version of ACL2, then make a copy (in
your ACL2 installation) of the following directory
~manolios/public/acl2/v2.9-linux/books/class and
certify the book "lex.lisp".
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
directory C:\emacs-20.7\bin\).
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
documentation
can be accessed via the URL /usr/local/acl62/doc/introduction.htm.
Last modified: Fri Jan 7 18:03:46 EST 2005