I can't stand it any more. Why does is it so difficult to install experimental software???? Granted, a lot of the stuff I want to try out is academic/experimental, but IT SHOULD NOT BE THIS DIFFICULT! The next time I download a package like this I'm going to tear my hair out:
* A README file that doesn't say what the software does!
* An INSTALL file that goes on for pages and page about cofiguration settings, tweaks to make files, editing this and that...
* After trying to complete the 20 steps correctly, the thing doesn't work!
* A few hours of trying to debug makefiles, configuration files, etc
Give up....

Oh well. I'm going to keep a list of the things I try that I can't get to work:
YAMPA I'm sorry this one has to be first. But the link to the install file (SOE.msi) is broken. I peeked in the folder and found one, then downloaded lots of other stuff, but couldn't get it to work.

ACL2, Emacs and Eclipse

I will not say anything too negative about Emacs here. I suspect my peers might think badly of me simply because I don't use Emacs. But I've been living the the world where text selections should be visible, status bars are drawn by the GUI, and cut/copy/paste are control x/c/v for too long. I just can't handle Emacs.

But I've always liked being able to run a command in an editor window. An editor I wrote in college for VMS, a derivative of Z from Yale, had this features. And of course Emacs does too.

This is a problem, because using ACL2 effectively pretty much requires a good shell window. So I've been hunting around for a solution. Then I thought of Eclipse.

Eclipse has External Tools to run processes. I thought they always ran in batch mode. But I found a trick to run the process in an interactive mode, just like Emacs.

To set it up, just do this:
  1. From the Run/External Tools/External Tools... menu, create a new tool
  2. Set the program location to be the path to the ACL2 executable
  3. Set the working directory to be your directory (I use a variable representing the current project)
  4. Set the arguments to "-". This is the key to make the process take interactive input from the console.
  5. Then just run the tool and ACL2 appears inside a window in eclipse.
I put my input file and the ACL2 window side-by-side and then copy/paste my text.

If you use the Scheme plugin and associate the Scheme Editor with .lisp files (using Preferences/File Assocations), then you will also get paren balancing, syntax coloring and formatting. You have to define some custom settings for ACL2, but this is easy to do. Send me a note and I'll give you my config file.

Oh, and here's what it looks like in action.