Tools
An alpha copy of version 2.8 of ACL2 is available locally for linux
machines. A version based on Gnu Common is available at ~manolios/public/acl2/v2.8-linux/gcl-saved_acl2.
A version based on Allegro Common Lisp is available at
~manolios/public/acl2/v2.8-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.
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-2.5.0.
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: Thu Aug 5 16:09:44 EDT 2004