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.