|
|
|---|
|
|
|
|---|
Some details regarding how ACL2s is implemented
To support interruption of the ACL2 process, we need more
information/functionality than Java provides through its
On Unix variants (Linux, Mac OS X), the wrapper for an invocation of
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 pidkill -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.
Here I discuss the stuff that is common to all modes, including "Compatible" mode. See the ACL2s-user-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 (see Why won't ACL2s let me do <blah> in a
session? in the ACL2s-faq), spit out metadata for some
things, and provide some system-level extensions in functionality.
All of these ACL2 modifications are implemented via books
distributed with ACL2 (
After these are included at startup, reset-prehistory
is used to suggest to newbies that ACL2 is starting fresh, but
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. ;)
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
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"?>
<plugin>
<extension point="acl2s.modedir">
<include-book-dir-entry keyword=":bobs-mode"/>
<dependency keyword=":acl2s-modes"/>
<mode
name="Bob's Mode"
short_desc="Favorite mode of some hypothetical person named Bob"
long_desc="this is an optional long description"
book_dev="true"
extra_imports="(defun-bob defmacro-bob)"
init_file="bobs-mode.lsp"
precedence="50"
ttags="((:ccg))">
</mode>
<certify-order-element book="defun-bob"/>
<certify-order-element book="defmacro-bob"/>
</extension>
</plugin>
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.