Setting up ACL2 on a Mac...

[jdiamond]

Much thanks to Sandip and Matt for all the time they spent helping me
get ACL2 installed on my Mac. I'd like to return the favor by sharing
what we learned...

=====================================================================
Recently I spent a bit of time unsuccessfully trying to both set up
ACL2 (with a LISP subsystem) as well as get a LISP plug in working for
Eclipse. For Eclipse I initially tried Dandelion, and then CUSP, both
without full success. For ACL2, I went ot the ACL2 website, picked a
random LISP (I think it was allegro), and again failed to make it
work.

< I did this because (1) I was hoping to use ACL2 to help reverse
engineer the HWK questions, and (2) I was hoping that any LISP plug in
for Eclipse would help me avoid learning emacs. >

I have since learned that it is absolutely not worth your time
attempting such things, as there is a specific, known way to do these
things.

=====================================================================
For eclipse, there is a full ACL2 plug in called ACL2s. I have not
tried to use it yet.
=====================================================================

For command line ACL2, you need to first install a Lisp engine. The
only one that is supposed to work out of the box is "Closure Common
Lisp", or CCL for short. (Formerly known as OpenMCL.) But the catch
is that if you follow the acl2 links to the ccl website and download
and install it, you get a version that is missing a key script to
allow it to work with acl2.

Instead you must use subversion to get CCL. Go to the directory you'd
like to install CCL and type:

# for Intel based Macs:
svn co http://svn.clozure.com/publicsvn/openmcl/release/1.2/darwinx8664/ccl

# for PowerPC based Macs:
svn co http://svn.clozure.com/publicsvn/openmcl/release/1.2/darwinppc/ccl

# for Linux:
replace "darwin" with "linux"

Once you get all the files, there will be a subdirectory called
"scripts". The one "ccl64" will act as your LISP engine. Then, once
you install acl2, you type

make LISP=MyCCLPath/ccl/scripts/ccl64

That is, use the script in place of the executable.

Once you do this, you can run ACL2 in a shell by executing (or double
clicking)
MyACL2Path/acl2-sources/saved_acl2
(which is again a script)