This used to be a pain, but it's much simpler now. First, we have a preference in the Eclipse preferences (under ACL2s > ACL2) that allows one to specify the directory that contains your ACL2 image, whether it's "saved_acl2", "run_acl2", or "bin/acl2.exe" under that directory.
If you don't specify that preference, we check to see if an "ACL2 Image" is installed in Eclipse, in which case we attempt to use that.
Next we check the environment variable ACL2_HOME for the directory.
Next the java property acl2.home. Then if none of those is fruitful,
we just try executing "acl2" and see what happens.
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
`acl2' would look like this (4 arguments, each underlined):
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:
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:
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. ;)
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.)
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":
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.
Wrapping the ACL2 process
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.
sh -c echo "$$"; exec "$0" "$@" acl2
kill -INT pid
kill -TERM pid
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.
How undo and redo are implemented
How modes are implemented
<?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>