Implementation Notes for ACL2s

Peter C. Dillinger

Wrapping the ACL2 process

To support interruption of the ACL2 process, we need more information/functionality than Java provides through its java.lang.Process API. Roughly, we execute ACL2 in a wrapper that outputs as its first line of text an ID number that can be used to interrupt the process. All output after that is that of ACL2. The plugin captures that ID number and uses it when needed.

On Unix variants (Linux, Mac OS X), the wrapper for an invocation of `acl2' would look like this (4 arguments, each underlined):

sh -c echo "$$"; exec "$0" "$@" acl2

Basically, this uses the standard Bourne shell to echo its process id and then execs (keeping the same pid) acl2--or any other command used there. To interrupt or terminate acl2 (respectively), we execute one of these:

kill -INT pid
kill -TERM pid

On Windows machines, things are not this easy. We use a wrapper called hiddencon(.exe) that opens a new console, immediately hides it (flicker; sorry), outputs an id number, and executes a program "attached" to that console. Then we can invoke sendctrlc(.exe) with that id to asynchronously deliver a "Ctrl+C" equivalent to that console, interrupting the program. sendbreak(.exe) likewise sends a "Ctrl+Break" equivalent, which causes the program to terminate.

These auxillary programs (hiddencon, sendctrlc, sendbreak) are included with the ACL2s plugin, so there's nothing extra to install. It's a bit of a mess, but it seems to work reliably these days.

Some wacky details of hiddencon.exe:
The stdin and stdout of the program are inherited from the wrapper--not connected to the console, so one might wonder what the console is for. The answer: Windows has no "interrupt" signal. When one types "Ctrl+C" in a console, the console takes care of notifying the process in some weird way. Windows has a mechanism for programmatically initiating a "Ctrl+C" equivalent, but its really only practical from a process that is "attached" to that console. With this in mind, the job of the wrapper is to enable any other process to initiate an "interrupt" on the console it created. The wrapper has a thread that reads and processes events from its Windows event queue, and one type of event, which could be initiated by anyone who knows the thread id of that wrapper thread, causes the wrapper to send an "interruption" to the hidden console.

Hooks: How/what ACL2 functionality is modified for ACL2s

Here I discuss the stuff that is common to all modes, including "Compatible" mode. See the guide section on modes and "How modes are implemented" below.

To support the kind of interaction ACL2s provides requires lots of cooperation and metadata from ACL2. Thus when we run ACL2 for an interactive session, we install some changes that disallow some things, spit out metadata for some things, and provide some system-level extensions in functionality. All of these ACL2 modifications are part of the "acl2s_hooks" plugin:

After these are included at startup, RESET-PREHISTORY is used to suggest to newbies that ACL2 is starting fresh, but (strip-cars (global-val 'known-package-alist (w state))) should reveal the "ACL2S" package is defined, and :ttags-seen accurately suggests how severely spoiled your session is.

A consequence of including the standard hacking books for this code is that if you want to include them in your code in ACL2s, it will appear redundant during interactive development but is needed for certification as a book, for which none of the above are required/included.

If you run into a case in which you really need to do something differently between interactive development and certification (like when i'm doing interactive development on the hooks books--my head hurts!), you can use the feature-based reader macros #+acl2s and #-acl2s. :acl2s is added to *features* for interactive development only. Please don't abuse. ;)

How undo and redo are implemented

The super-history book of the acl2s_hooks plugin implements a stack of old "states". Actually there are two stacks: an undo stack and a redo stack. An undo pops the undo stack, pushes that "state" onto the redo stack, and then installs the "state" on the top of the undo stack. A redo pops the redo stack, pushes that "state" onto the undo stack, and installs it as current. Any other "state"-changing form empties the redo stack, and the resulting "state" is pushed onto the undo stack.

Now I've put "state" in quotes and not called it "the world" because this notion of state is not that same as ACL2's state stobj and is more than just ACL2's world. Our super-history states are the world and a bunch of state-global variables that store things like the current package, guard-checking setting, and other things that affect whether things might pass or fail, and what they mean. The complete list is ACL2S::*SETTINGS-GLOBALS* in the categorize-input book of the acl2s_hooks. This is similar to--but not exactly--what is saved and restored by make-event. (Our undo/redo mechanism predates the release of make-event.)

How modes are implemented

Since version 0.9.0, ACL2s' session modes other than "Compatible" come from an independent plugin, acl2s_modes. (Note that all three plugins "acl2s," "acl2s_hooks," and "acl2s_modes" are installed with the feature "acl2s.") Thus, third party Eclipse plugins can also add their own session modes to ACL2s. To do so, they must extend the "acl2s.modedir" extension point, like in the plugin.xml for an example "Bob's mode":

<?xml version="1.0" encoding="UTF-8"?>
<?eclipse version="3.2"?>
   <extension point="acl2s.modedir">
      <include-book-dir-entry keyword=":bobs-mode"/>
      <dependency keyword=":acl2s-modes"/>
            name="Bob's Mode"
            short_desc="Favorite mode of some hypothetical person named Bob"
            long_desc="this is an optional long description"
            extra_imports="(defun-bob defmacro-bob)"
      <certify-order-element book="defun-bob"/>
      <certify-order-element book="defmacro-bob"/>

The plugin is a JAR file with such a plugin.xml file, a proper manifest file, and any books and supporting files needed for the mode.

All of the components shown above are optional, and all but the include-book-dir-entry can have multiple instances. ACL2 will be given the root install directory of the plugin with add-include-book-dir and the keyword in include-book-dir-entry. In fact, ACL2s will create a "dir.lsp" file with that form whenever the plugin is used. Specifying an include-book-dir-entry is required if the initialization of any modes need to refer to that directory for including books. (The current directory will not be set to the plugin directory.)

Each include-book keyword directory used in your mode initialization (other than yourself and :system) should be listed as a dependency. Bob's mode uses "ccg" from :acl2s-modes.

Technically, only the name and short_desc are required for a mode. The non-obvious parts:

Each certify-order-element names a book to be certified with the ACL2s system books, in the order given. You should name all the books in this mode directory your modes depend on. Note that here, like in include-book and certify-book, ".lisp" is not included in the name.