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.

1 comment:

hanbing said...

Hi, this is Hanbing.

On using ACL2 in Emacs, I guess many of us rarely need to do "selection" for copy/pastes.

There is a predefined keyboard macro that "grabs" a S-expression form yours source file and "throw" it into a user shell buffer and move the cursor to point to next form in the source code.

I found this quite helpful. Maybe eclispe can do the same thing.