This document is organized roughly by the way the ACL2s components are currently packaged and distributed. Java components are only in the ACL2s Plugin. ACL2/Lisp components are sprinkled throughout, including some code quoted in the Java components. Note that .lisp files are always books, using ACL2s-style preambles. .lsp files are never books. Some .lisp files are used without direct certification, using "inline-book". C code is also here and there, but is only used to make up for lack of good shell scripting in Windows.
Note that the "acl2s" feature for Eclipse includes the "acl2s" plugin, the "acl2s-hooks" plugin, and the "acl2s-modes" plugin. Note also that "acl2s-plugin" is what I call one component of the "acl2s" plugin, because it is the only Eclipse-specific part of that plugin.
Here is everything distributed in the plugin for Eclipse named "ACL2s," with ID "acl2s". The plugin is unpackaged on the user's system so that "procwrap" executables are available as files in the filesystem. I don't remember whether the "icons" also need to be available as files or can be in a JAR file. To keep from using too many files, the Java components are put in JAR files, which are in the downloaded JAR file for the plugin.
Defying the convention for naming Java packages (supposed to begin with a DNS domain name in "reverse" order), the Java packages for ACL2s are in acl2s.* packages. Also, some libraries from Peter Dillinger that are not ACL2-specific are in org.peterd.util.* packages.
plugin.xml, build.properties, and META-INF/MANIFEST.MF define aspects of the plugin and how it is built. All of these can be modified using a nice Eclipse editor accessed by double-clicking plugin.xml. Here are details relevant to the different tabs of that editor:
The remaining tabs allow direct editing of the files, which is rarely useful.
This is a Java library for communicating with an ACL2 session. It is installed as acl2s-lib.jar as part of the "acl2s" plugin.
One can use ACL2 syntax or an embedding of the ACL2 input universe in Java. One can also parse and unparse between the two in a context-sensitive way. It also includes code for extracting .acl2 files from the preambles of ACL2s-style .lisp books and/or certifying them.
Here are the packages, with short descriptions:
This is a Java library for implementing script management (line-based) interfaces to ACL2. It is in the acl2s.uilib.* packages and depends on acl2s-lib. The Eclipsisms have been abstracted away in the acl2s.uilib_driver package.
The "bread and butter" of this component is the InteractiveSessionManager. This is essentially an asynchronous version of an acl2s.lib.session.InteractiveSession, because it is designed to either receive or probe for inputs and dispatch output to the right place.
Most of this component is supporting the InteractiveSessionManager. An exception is the acl2s.uilib.cmd package, which contains the abstractions for categorizing inputs. This is important for building script management interfaces to ACL2, but is not used directly by the InteractiveSessionManager.
This is the only Java code with a dependency on Eclipse. Thus, it contains all of the Eclipse extensions for the editors, etc. It is in the acl2s.plugin.* packages and depends on acl2s-lib and acl2s-uilib.
Here are the packages, with short descriptions:
A quick note about threading: interacting with Eclipse code is rarely thread-safe, so it usually expects to be done in the "display" thread. If not already in the display thread, you can "access" the display thread with Acl2sPlugin.syncExec(...) or Acl2sPlugin.asyncExec(...).
In acl2s/experimental-src is Java code that has preliminary/experimental support for executing ACL2 code (executable counterparts, that is) directly on my Java embedding of the abstract syntax. The idea would be to finish implementation of the ACL2 primitives (see the paper on the precise description of the ACL2 logic) and then use definitions from the world to execute anything as its executable counterpart (as in proving theorems, stobjs treated as ACL2 objects) would execute.
Short for "Process wrapper." This wraps the ACL2 process on Windows in such a way that it can be interrupted programmatically, as if hitting Ctrl+C in a Windows console window. This is not needed on Unix-style platforms, because we can use a shell script to wrap the process and signals to communicate.
Basically, to send a Ctrl+C to a process in Windows, it needs to have a "console" associated with it. hiddencon.exe executes its first argument with the rest of the arguments as arguments. It then outputs on one line an identifier that can be used to send events. It then listens for Windows-style events in a separate thread. When it receives a particular Windows event, it sends a Ctrl+C (or Ctrl+Break) to the process under the console. sendctrlc.exe with that identifier will send the approriate Windows event to have the managing thread give it a Ctrl+C. sendbreak sends Ctrl+Break, which should kill the process.
This is used by acl2s-lib to implement an OS-independent Java abstraction of an OS process that is interruptable (and killable).
See README for commands to build in cygwin.
Dependencies This component depends on nothing else--except Windows to run it. It is not specific to ACL2. I believe Windows 2000 or greater is required, but that should hardly be an issue any more.
Constraints This is distributed in the ACL2s plugin because it is needed (for windows users) even if the user uses his/her own build of ACL2.
Known Issues When starting a windows process under this system, one can often see a flicker of a console window popping up and disappearing. I did not find an effective way to get around this problem. It should be possible, but might require modifying the design of the framework.
Related Work Emacs does something similar to implement C-c C-c in Windows. Its source code can be consulted if a new implementation is needed.
Unfinished To launch something external (such as the Logic game), I was working on something to start a process in a "detached" way. I believe this is what the "start-*" files are, but I don't recall whether they work. I have a Java abstraction for this in acl2s-lib, org.peterd.util.process.DetachedProcess, but right now it does not actually detach from being "under" Eclipse in Windows.
The plugin uses various icons for UI actions and outline objects, and these are distributed with the plugin. They are in acl2s/icons. I developed these using GIMP, and development files are in icondev. For documentation purposes, these need to be available from the web docs, and this is done with symlinks.
These books contain all of the ACL2 support needed by the Java parts of ACL2s, whether acl2s-lib, acl2s-uilib, or acl2s-plugin. This does not include pure ACL2 extensions that do not concern the parts written in Java; they are in acl2s-modes, which defines all of the standard session modes other than Compatible.
The ACL2s plugin reads certify-order.txt to find out what to certify and in what order. Keep it up-to-date.
It is standard to use :load-compiled-file :comp when including these books, so that the user can benefit from compiled functions without recertification if switching to another underlying Common LISP for the same version of ACL2.
Development note: Many of the books in acl2s-hooks have an IN-PACKAGE statement like this: (in-package #+acl2s "ACL2S-DEV" #-acl2s "ACL2S"). (See also acl2s-pkg.lsp.) This is to support interactive development of these books within ACL2s, which is already running with a copy of the acl2s-hooks. During interactive development in ACL2s, I add ACL2S to the *features* so that I can use the read-time conditionals #+acl2s and #-acl2s to choose different behavior based on whether in interactive development or not. See acl2s.lib.session.MyInteractiveSessionConfig.getStartup(...).
This file contains raw Lisp code that is executed by all interactive sessions before most anything else. Right now, here are the things it does, which should be described in comments:
This book mostly provides the interactive version of BEGIN-BOOK, which makes sure that the session is in a state suitable for a CERTIFY-BOOK. In creating a .acl2 file for an ACL2s .lisp file, BEGIN-BOOK is translated into the call to CERTIFY-BOOK. Consequently, it takes the same parameters as CERTIFY-BOOK, except for the book name and number of events in the portcullis. We omit the book name so that ACL2s books can be renamed without modifying their contents, and we omit the number of events because it is just a sanity check that is not needed in a context with a "certify book" button. The Java class acl2s.lib.certify.MaybeExtractPreamble in acl2s-lib can be used to generate a .acl2 file from the preamble of an ACL2s .lisp file.
This book categorizes inputs, including keyword commands, into one of the categories given in the ACL2s documentation. I use ACL2's functionality for detecting events, so that case is complete. In some cases, inputs that could be categorized as COMMANDs or QUERYs might be categorized as ACTIONs.
The categorizations used to be static in the sense that there were no settings that could change the categorization. (The world can change the categorizations because of macros, stobjs-out, etc.) Now, one can configure which (set of) state globals are tracked in the super-history, which can affect whether something is a COMMAND (undoable) or an ACTION (not necessarily undoable). See Super-history.
acl2s-lib does not care about input categories, because it just operates at the level of inputs, outputs, and the environments in between. The classes in package acl2s.uilib.cmd provide a Java abstraction of the categorization process. ACL2s used to insist that everything that could be history relevant (based on its categorization) would be put above the line. Now it only checks after executing each immediate command whether it modified the super-history, something that can be determined by checking environments in acl2s-lib. Wart: The code that maintains this invariant (that everything "history relevant" is put above the line, even if typed as an "immediate" input at the command prompt) is in acl2s.plugin.editors.lisp.LispDocument.commandCompleted(...). This functionality should be in acl2s-uilib or acl2s-hooks even.
Nevertheless, input categorization does not play as big of a role as it used to. Now, it is mostly used for book development. One could imagine, however, incorporating into introductory modes a warning prompt or warning message before executing ACTIONs. (Right now there is a warning message when undoing an ACTION.)
This book provides the functionality needed for an acl2s.lib.session.InteractiveSession to work. In particular, when activated, it provides the following metadata output:
This book provides supplementary metadata output--that which is not needed by acl2s-lib. Right now, it just marks where checkpoints are in proof output. This output is processed in acl2s.plugin.editors.session.SessionDocument.doProcessOutputLine2(...).
This book is to prevent the user from subverting elements of interactive development in ACL2s--though a user who has declared a trust tag can still be subversive. It works not by filtering the user's input but by requiring a password for certain actions. That password is chosen by the entity installing the protection. The password is stored only as a hash, reversible only by solving a modular square root problem of moderate size. (This is not computationally infeasible, just very inconvenient.)
Here are the protections:
This book maintains a stack of logical states for UNDOing. It also maintains a stack of recently "undone" logical states for REDOing.
Logical State: What constitutes a logical state is an engineering decision. Basically, we want it to include everything that affects the admissibility of input forms, so clearly, the world is not enough. (That's right James Bond.) The admissibility of forms can clearly depend on the current package or guard-checking setting, neither of which is part of the world. However, admissibility could in principle depend on any ACL2 state, since it is all exposed to MAKE-EVENT. One could even write (assert-event (@ foo)), which asserts that a global variable not used internally, FOO, is bound to non-nil. I consider this a degenerate case and do not attempt to handle it, partly because including all global variables in the logical state would probably be costly in memory consumption and execution speed.
The notion of logical state used is the world plus a set of state global variables specified when activating the super-history. This should always include *CRITICAL-SETTINGS-GLOBALS* from categorize-input.lisp, because those are most critical to the admissibility of forms. ACL2s always includes these (see acl2s.lib.session.MyInteractiveSessionConfig.getStartup(...)).
Actually, one can also specify state-global variables to track and restore with the super-history but not consider the logical state to have changes if they change. This affects the categorization of inputs and what things executed as immediates need to be copied above the line. These "tracked but not matched" state globals should include *RESTORABLE-TRANSIENT-GLOBALS* from categorize-input.lisp. ACL2s always includes these (see acl2s.lib.session.MyInteractiveSessionConfig.getStartup(...)).
Activation: The super-history is for "line"-oriented sessions. ACL2s allows sessions that are stand-alone and/or do not have an enforced "line," and those sessions do not use the super-history. See acl2s.lib.session.MyInteractiveSessionConfig.getStartup(...) and acl2s.plugin.editors.session.SessionDocument.getConfig().
Configuration: When using the super-history in ACL2s, the parameterization over a set of state globals to be tracked has been distilled into two boolean configuration parameters, which we can name TRACK_MONITORS and TRACK_PRESENTATION. See acl2s.plugin.prefs.InteractionPrefs for basic description and how the user can override these settings. By default, "introductory" modes track both monitor globals and presentation globals, so that there's a simple story for "the line." Experts might prefer they not be part of the super-history. See acl2s.lib.session.MyInteractiveSessionConfig.getStartup(...) for how the configuration translates to ACL2 code. In particular, the *MONITOR-SETTINGS-GLOBALS* and *PRESENTATION-SETTINGS-GLOBALS* constants in categorize-input.lisp indicate the global variables associated with TRACK_MONITORS and TRACK_PRESENTATION.
Hacks: To get super-history working correctly, we install two hacks (with redefun+rwrite). First, if we are in the top-level LD loop, we should use REVERT-SUPER-HISTORY-ON-ERROR instead of REVERT-WORLD-ON-ERROR. This is necessary because we assume that anything that has failed does not affect the super-history, because we never add above the line something that has failed. If we only revert the world, changes to critical state globals might persist after something that returned an error.
Second, whenever we complete a form read from *STANDARD-OI*, we need to push the current super-history onto the stack, using UPDATE-SUPER-HISTORY. Excess calls to UPDATE-SUPER-HISTORY should not affect correctness, but only waste space. For UNDOing, the length of the stack is recorded after each form. See references to acl2s.lib.session.IEnvInfo.getSuperDoneSize().
UBU and UBT: If an ACL2s user types a :U, :UBT, or :UBU immediate command, ACL2s translates that into appropriate line motion. :U just undoes the last form and :UBT and :UBU undo enough to undo "through" or "up to" a command descriptor. Code at the bottom of super-history.lisp translates those command descriptors into the appropriate super-history indices so that the plugin can perform the appropriate line motion. See acl2s.plugin.editors.session.SessionDocument.trySubmitImmediate(...).
graphics.lisp is the only book from acl2s-hooks that users should include specifically. See the user documentation for graphics development to understand graphics.lisp.
graphics-basis.lisp is included by graphics.lisp to access the low-level functionality for interacting with the ACL2s graphics system. This creates a new ACL2 stobj that captures interaction with the ACL2s graphics system. This offers a logical story for the interaction, but that is not really important. There are two functions that use this stobj: POP-GRAPHICS-EVENT and PUSH-GRAPHICS-OP. This communicates with the ACL2s plugin using specially formatted output on the standard-oi pipe. POP-GRAPHICS-EVENT blocks waiting for the next "event" from the plugin and PUSH-GRAPHICS-OP sends a graphics "operation" to the plugin.
At the moment, acl2s-lib does not have any recognition of the graphics stuff. acl2s-uilib is responsible for recognizing the graphics operations output by ACL2 and handing them off to acl2s-plugin, and for recognizing ACL2's requests for the next graphics events and requesting them from acl2s-plugin. This happens in acl2s.uilib.session.InteractiveSessionManager and communicates with acl2s-plugin through the interface acl2s.uilib_driver.IAcl2sGraphics. Only acl2s-plugin has a notion of the meaning of the graphics operations and events. See acl2s.plugin.graphics.Acl2sGraphics and all the classes in that package.
These files load an ACL2-customization file or warn about the presence of an ACL2-customization file, respectively. (See ACL2 documentation for explanation of ACL2-customization.) Depending on user preferences and perhaps on whether the session mode is introductory, one of these will be used after the mode is initialized. (See acl2s.lib.session.MyInteractiveSessionConfig.getStartup(...).) I choose to load after session initialization because I don't want a user complaining about failures in loading ACL2s stuff if they introduce an incompatibility in their ACL2-customization. Note that I supress ACL2's loading of customization files in acl2s.lib.session.MyBaseConfig.setupEnvironment(...).
ACL2-customization is never loaded for book certification, in accordance with ACL2's default policy, evident by "export ACL2-CUSTOMIZATION ?= NONE" in Makefile-generic.
Background: At one point, Matt Kaufmann sent an email complaining that ACL2s did not respect acl2-customization files. My view was that it might interfere with how my stuff gets loaded and pollute the "pristine" ACL2s environment, but I decided to code up a complicated solution, as discussed.
Some ACL2 code developed for ACL2s is now distributed with ACL2. Most importantly, this includes the "hacking" books in books/hacking. See the Readme.lsp file in that directory for basic information about each book.
REDEFUN+REWRITE: One of the most elaborate things used from the hacking books is REDEFUN+REWRITE, which allows redefinition of an ACL2 function based on "code rewriting" of the existing definition. This "code rewriting" has no real relationship to ACL2 rewrite rules because they have different goals. The goal is to specify modifications to functions in a way that tend to hold up to acceptable changes in the original function and complain appropriately in the case of potentially incompatible changes. Some documentation is in $ACL2/books/hacking/rewrite-code.lisp, but I explain some here by example, from super-history.lisp:
(progn+touchable :all
When redefining a system function that uses untouchables, we need to redefine in a context in which they are temporarily touchable.
(redefun+rewrite acl2::ld-read-eval-print
We are rewriting the function LD-READ-EVAL-PRINT, and because we haven't imported it into the current package, we have to specify the ACL2 package.
(:carpat (acl2::revert-world-on-error %form%)
:CARPAT specifies a pattern to search for that must be the car of a cons or at the top level of a function definition. :PAT is similar with no such restriction. Each "rewrite spec" should have one :CARPAT or :PAT. By convention, I surround variables with % signs (more detail coming). The reason for :CARPAT is to match probable function calls. If I use :pat (cons %a% %b%) that would match in (foo cons 1 2), because that is (foo . (cons 1 2)). :carpat (cons %a% %b%) does not match because (cons 1 2) is not the car of a cons nor at the top level.
:recvars %form%
:VARS and :RECVARS specify a singleton or list of symbols to treat as variables in the pattern. Variables match anything, including symbols, constants, and cons structures. Variables given in :RECVARS are "recursive," meaning what those variables match will be rewritten as well. (Note that this process is guaranteed to terminate if the pattern is not directly a recursive variable.
:mult 1
:MULT specifies an allowed number of times to use this code rewrite. If it is not used the given number of times, an error is raised. In fact, the reason we used a recursive variable in this rule is to assert that there is only one occurrence in the function, even within the matched %FORM%.
:repl (if (= 1 (@ ld-level))
(revert-super-history-on-error %form%)
(acl2::revert-world-on-error %form%))))
:REPL is the replacement for the given pattern. Occurrences of the variables are replaced with what they matched, possibly after recursive rewriting in the case of recursive variables.
(redefun+rewrite acl2::ld-read-eval-print :seq
Now we are rewriting the function LD-READ-EVAL-PRINT, but we are going to give two rules that should be performed in sequence (:SEQ, go deep before trying other possibilities). To combine rules to be matched simultaneously (go deep after trying other possibilities) use :SIMUL.
(:carpat %body%
This is a standard way to wrap code around the whole body. Just be sure you don't have any recursive variables.
:vars %body%
:repl (let ((old-std-oi-super-history (standard-oi state)))
%body%))
When :MULT is omitted, it is the same as *, which is shorthand for the range (0 . inf) or any number of rewrites. + is short for (1 . inf), one or more. In this case, there's no reason to assert a number of matches because there will always be one, at the top level.
(:carpat (acl2::ld-print-results %trans-ans% state)
:vars %trans-ans%
:mult 1
:repl (pprogn
(if (equal old-std-oi-super-history *standard-oi*)
(update-super-history state)
state)
(acl2::ld-print-results %trans-ans% state)))))
So after we put a LET at the top level, we put this code around a call to LD-PRINT-RESULTS.
Inline-book: At one point in ACL2s's history, there was a conflict between the amount of time spent certifying the system books and the separation of functionality into separate books. A lot of certification time was spent including books that were included in just one other book. To solve this problem I implemented some make-event magic that solves this problem by allowing one book to be inlined into another. This is now in $ACL2/books/make-event/inline-book.lisp.
Peter's essay on (not) moving more (or all) to ACL2 standard books: I have strongly resisted adding all of acl2s-hooks to the ACL2 standard books for reasons I will try to express here. My basic objection is that the parts of acl2s-hooks that I have not contributed to the standard books are more likely to change significantly based on updates to ACL2s than based on updates to ACL2. Consequently, I want to be able to distribute updates with each update to ACL2s.
One possible way around this would be a "snapshot" model, in which each ACL2 release includes the latest snapshot of the acl2s-hooks. In order to make updates with ACL2s, however, we would probably have the latest acl2s-hooks elsewhere on the user's system, because (1) updating all of ACL2 just for updates to the hooks would be overkill, (2) updating just part of a plugin in Eclipse is difficult, and (3) we wouldn't want to taint an ACL2 tree with updates anyway, since a set of standard books are part of the definition of an ACL2 version. But I think it's awkard to have an old copy of something lying around in a location where it might be used in interference with the new!
Consequently, I have taken the approach of migrating to the standard books only pieces that I feel have stabilized to the point that any updates that might be desired won't be critical to other updates to ACL2s.
The argument does not hold up as well for acl2s-modes (below), since it is, by design, independent of the rest of ACL2s. The only part of the argument that holds up there is the desire to release frequent updates and not have multiple, potentially competing copies on the user's system.
"Compatible Mode" is the only session mode that is built into the "acl2s" plugin for Eclipse. Other Eclipse plugins can add session modes via the acl2s.modedir extension point. The plugin "acl2s-modes" does this, to register the standard set of session modes for ACL2s. These are essentially independent from the rest of ACL2s, so they are implemented with separation of concerns. (See user documentation on "How modes are implemented.")
It is standard to use :load-compiled-file :comp when including these books, so that the user can benefit from compiled functions without recertification if switching to another underlying Common LISP for the same version of ACL2.
Each .lsp file for a mode contains the code inserted into the preamble of every book using the corresponding session mode. The distinctive comments are there so that a user opening an ACL2s .lisp file in a text editor will not be utterly confused not to see their code right away.
The lines starting with #+acl2s-startup are executed iff the code is read during the initialization of an interactive session in ACL2s. In some cases, this is to include functionality that is only needed for interactive sessions. Otherwise, it is used to store a good error message in the case of failure. (ACL2s prints whatever is stored in the state global FMT-ERROR-MSG if something fails during startup. See acl2s.lib.session.MyInteractiveSessionConfig.) (In developing ACL2s, I have learned that failing gracefully is key to making a usable tool: one that people can troubleshoot themselves. -Peter)
Though most of this is in the user documentation, this mode includes:
Like ACL2s mode, but includes these:
Like Intermediate mode, but do no automatic induction. J Moore wanted a mode that behaves this way, so that users have to explicitly direct inductions.
Like Intermediate mode, but with nothing related to soundness. Starts in :PROGRAM mode and with a default hint that kills any proof attempt. Not including features such as CCG makes the mode load more quickly.
TODO: by others?
This book is a repository of things that Pete and others simply want included in non-Compatible modes. This currently includes a definition of ALLP, CHECK, CHECK=, DEFUNT, and THEOREM.
This book uses hacks to make imposing certain restrictions on the theorem prover clean, simple, and pretty. In particular, without using hints, one can set an maximum depth on automatic inductions and/or completely disable parts of the waterfall.
Wart: The hack for adding an entry to the acl2-defaults-table has a large wart. The acl2-defaults-table entries at inclusion time must match those at certification time. In particular, the CCG book also adds to the acl2-defaults-table. Consequently, one cannot certify that book and this one in isolation and then include both of them. In general we might need three certification/inclusion trails: just CCG, just prover-restrictions, and both. It turns out all the modes that want prover restrictions also want CCG termination analysis, but not vice-versa. We certify ccg.lisp, but instead of certifying prover-restrictions.lisp, we certify prover-restrictions-and-ccg.lisp, which includes CCG and inlines the prover-restrictions.
Updates: With the version of ACL2 to follow 3.5, one should be able to implement these restrictions in a reasonable way using default/computed hints, using some combination of :no-thanks, :override, and :do-not-induct :otf. (I might be incorrect on some naming details.) For example, default hints are a terrible way to set up session modes when users consistently get "Thanks for the hint!" messages.
This books provides support for printing values in a codified, "evalable" way, as DrScheme does for student languages. See comments in the book for details on configuring it. It is used by evalable LD printing and TRACE*, below.
Because of suspected stability, this book is now (ACL2 >= 3.5) distributed with ACL2's standard books, in misc/. It needn't be distributed in acl2s-modes once support for ACL2 3.4 is dropped.
This hacks ACL2's read-eval-print-loop (LD) to print results in an "evalable" way. See comments in the book for details on configuring it.
Because of suspected stability, this book is now (ACL2 >= 3.5) distributed with ACL2's standard books, in hacking/. It needn't be distributed in acl2s-modes once support for ACL2 3.4 is dropped.
This is the beginner-friendly version of TRACE$. It uses evalable printing (if activated) and has other benefits, discussed in the user documentation.
Because of suspected stability, this book is now (ACL2 >= 3.5) distributed with ACL2's standard books, in misc/. It needn't be distributed in acl2s-modes once support for ACL2 3.4 is dropped.
To run sessions, an ACL2 installation is needed. Though some use the term "image" to refer to just the executable and auxilliary files that start an ACL2 session, I use "image" to refer to all the files needed to constitute, from the user's perpective, a full installation of ACL2. This includes .lisp and .cert files for the standard books, but does not need to include the ACL2 main sources, Makefiles, and generated .out files.
An acl2-image feature just includes an acl2-image plugin, which does not have any Java code but has all the files for an ACL2 image. (It also includes HTML documentation, zipped sources, and GCC if needed.) The "acl2s" feature does not depend on an "acl2-image" feature, however, because users are welcome to use their own build of ACL2, assuming it is an acceptable version.
The images distributed are, of course, platform dependent and, thus, need to be built for a specific platform. Under Eclipse 3.3, the Update Manager could pick an appropriate plugin based on the platform running Eclipse, but I could never get that to work reliably in Eclipse 3.4. Thus, the plugins and features are named based on the platform they are built for.
Currently, supported platforms are Linux/x86, Windows/x86, MacOSX/x86, and MacOSX/ppc. Apple sold its last PowerPC Macs in 2006, so PPC support could reasonably be dropped soon. 64-bit operating systems can complicate things (see below), but our preference is to have just a 32-bit version that also works on 64-bit operating systems.
Currently, supported underlying LISPs are GCL, SBCL, and OpenMCL (now Clozure/CCL). The only real reason for these limitations are so that "preinit" can neuter the debugger, though with SET-DEBUGGER-ENABLE defaulting to NIL, that's not as important.
Linux: Any version of GCL that works fine with ACL2 works fine with ACL2s, except that I seem to recall problems with 32-bit GCL on a 64-bit machine because GCC targets 64-bit code. This problem, and the general dependence on GCC, which is not always installed on "desktop" systems, makes GCL unattractive for distribution with ACL2s.
SBCL is currently my preference, because it has proven stable, automatically compiles definitions, has virtually no dependencies, and 64-bit Linuxes usually include enough 32-bit libraries to run 32-bit console programs, such as 32-bit SBCL.
I have not tried other LISPs very much under Linux.
Mac OS X: SBCL is currently my preference, because it has proven stable, automatically compiles definitions, has virtually no dependencies, and I don't recall any problems running 32-bit SBCL on 64-bit MacOSX. I'm not sure the same is true with 32-bit CCL (Clozure, formerly OpenMCL).
Windows: In my tests, SBCL for Windows is quite stable running ACL2. The problem is that (last I checked) it does not support interruption with Ctrl+C. This is not a big issue under Intermediate Mode, which limits automatic inductions, but is a deal-breaker for ACL2s or Compatible modes.
I have been using the GCL-based ACL2 distributed on the ACL2 web page for the Windows images. This requires a compatible version of GCC, so we distribute that along with it. (Details below.) I think reports of this 32-bit GCL working under 64-bit Windows have been conflicting.
Clozure might now work well under Windows. I don't know.
Background: Eclipse does not need to be "installed" on the user's system in the way that most software is installed to be available to multiple users. It is actually much easier to work with an Eclipse installation that is completely modifiable by the user.
This causes a problem for ACL2 images mostly because the certificate files for the standard books refer to their absolute path, and we don't want to require Eclipse users to put their Eclipse in a specific place. They should also be allowed to move it without it breaking. Consequently, to distribute ACL2 images as Eclipse features, we need a work-around for the dependence on absolute paths.
Basic solution: My solution is an ACL2 hack to update certificate files "on demand" for whatever path they are in, without full recertification. Thus, we can store what path the ACL2 is expecting to be in (implementation uses text file books/saved_dir), and if we start ACL2 with it in a different path, we call the code (implemented in fix-cert.lsp) to update the certificate files of the standard books. The context in which fix-cert.lsp is built or invoked is described in "building" and "run-acl2" details below.
Anatomy of fix-cert.lsp: fix-cert.lsp is constructed from three basic pieces: fix-cert-pre.lsp, *standard-book-list*, and fix-cert-post.lsp. Basically, fix-cert-pre has general code for updating certificate files. Then we define a constant *standard-book-list* as a list of strings that are all the :dir :system books. To play nicely with Makefiles, they should be listed in a valid certification order. Then fix-cert-post ensures the loaded code has been compiled, runs it on the list of standard books, and updates the text file containing the latest path.
Details of fix-cert-pre.lsp: In the next version, there should be a fix-cert.lisp distributed with the ACL2 system books that has the functionality needed. With a regression test in there also, it should be the responsibility of the ACL2 maintainers to keep this working.
Details of OLD fix-cert-pre.lsp (rev 126 and older): It should be easy to understand the wrappers around FIX-CERT-FN, where :dir should be something like :system. The outer ER-LET* in FIX-CERT-FN turns the symbolic directory into a path string. The MV-LET gets the full path to the book to "fix." CREATE-PKGS-FOR-CERT-FILE creates in the current session all the packages used by the target book--except that we define all such packages with no imports. This eliminates possible conflicts between packages and is OK in this context because all symbols in .cert files are printed based on their "canonical" package. Then I use ACL2's CHK-CERTIFICATE-FILE to load in the certificate as an object. The rest is a matter of doing some checks, translating that object and writing it back out with ACL2's MAKE-CERTIFICATE-FILE1. Using ACL2's certificate generation function ensures a valid checksum for the new certificate is produced, even though the certificate has, in a sense, been forged.
The checks, using CHK-NO-RELOC-IN-USER-BOOK-NAMES, are designed to abort in cases in which the user refered to a book with an absolute path. These checks should not be needed for the standard books, and ACL2 can actually generate include-books in certificates that look like they reference absolute paths in certificates, which make the checks too aggressive in some cases. Thus, the checks have been disabled in the definition of CHK-NO-RELOC-IN-USER-BOOK-NAMES. (For more detail, see acl2-unix-dist/fix-cert-notes.txt.)
The guts of the translating is in calls to RELOC-CMDS and RELOC-EXPR for the CMDS, PRE-ALIST, and POST-ALIST parts of the certificate. This basically replaces any strings starting with the old path to ones using the new path. It is theoretically possible for strings that do not refer to paths to match and be translated, resulting in unsoundness, but this is highly unlikely, especially in a controlled environment like the standard books.
There is still an outstanding issue regarding trust tags. See acl2-unix-dist/fix-cert-notes.txt. This issue would be fixed if no standard books included other standard books in their portcullises. Perhaps it would be good to have the acl2-books maintainers implement this. It would not take too much work. I recommend the (ld "pkgs.lsp") idiom for shared package definitions.
For these ACL2 images, we need to insert extra functionality before each startup of ACL2. This extra functionality is in a script called "run_acl2," which is what users or other programs should normally run to start an ACL2 session. For Unix-like systems, this is a SH/BASH shell script, and for Windows this is an EXE file compiled from C source code.
A design decision was made to put this functionality in a script other than "saved_acl2," and letting "saved_acl2" look and operate much like the usual ACL2 version, but with a warning. "saved_acl2" maintains compatibility with Makefiles, etc., but is only updated to use a new path when you run the new script, "run_acl2."
run_acl2 does these things (roughly):
Here's how it updates for the new path:
Then it starts ACL2, in a manner specific to the underlying Common LISP.
After you have built ACL2 from sources, using the desired underlying Common LISP, and certified all the system books, the "make-dist.sh" shell script can produce from that an "ACL2 Image" suitable for distribution with ACL2s. Packaging up the generated directory of files is described later in the Update Site information.
For Unix-like OSes, go into the acl2-unix-dist directory and run ./make-dist.sh acl2_build_dir target_dist_dir. Relevant files will be copied from acl2_build_dir to target_dist_dir, along with some stuff from acl2-unix-dist. We want the contents of the target_dist_dir to eventually end up replacing everything in the correct acl2-image plugin project directory-- everything except META-INF/, build.properties, and .project, which are the only items under version control.
For Windows, go into acl2-windows-dist in Cygwin. The make-dist.sh is nearly the same, but it might not totally work. I have been using the more up-to-date, more customized make-dist-win-gcl.sh to generate a GCL-based distribution in Windows. In theory, one should have a single make-dist.sh updated to work with Unix or Windows, and attention might need to be paid since there might now be a better LISP to use in Windows than GCL. (CCL? SBCL?)
One interesting piece of make-dist is building an exec-files.lst file. This is a list of all the files that (might) need to be made executable on the user's system. Eclipse installs the ACL2 image from a JAR file, which is just a ZIP file, meaning it does not include permission metadata. We work around this by including the exec-files.lst file, which by its existence indicates that the files listed in it might need to be made executable. We check for that file and, if needed, perform the chmod and remove the file. See acl2s.plugin.prefs.Acl2Prefs.getAcl2ImageDir().
One complication of make-dist is that care must be taken to preserve--to the extent possible--write times on files relating to books. We also set permissions appropriately, because in addition to the JAR files downloadable by Eclipse, there are TAR.GZ of the ACL2 images available for download. (See Update Site information.)
Common LISPs like to compile code and then load it in dynamically in new executable code segments, and this upsets an optional security mechanism called Data Execution Prevention (DEP) in recent versions of Windows. One work-around is to disable DEP entirely or for user applications. (A Google search can easily reveal how.) Another solution is to tell Windows to run the application in a compatibility mode with DEP disabled. This requires building a .sdb file using the Microsoft Application Compatibility Toolkit and installing that file on client machines.
Here's how I have generated proper .sdb files in the past, using version 5.0 of the toolkit:
For building an ACL2 Image for windows, make sure that the DEP-fix.sdb file and install-sdb-files.exe is in the directory in which the image is being built. install-sdb-files.exe is a script-like C program that uses Windows' sdbinst to install all .sdb files in the current directory. With this setup, we can instruct users who run into trouble because of DEP to run install-sdb-files.exe in their acl2-image directory to fix it. TODO: put this on the user documentation page.
In case it is not obvious, a new .sdb file needs to generated for any new version of saved_acl2.exe.
In response to an email message from a user who ran into a situation in which the write times of the compiled files were not after the .lisp files, I wrote a little Java utility to "touch" all of the compiled files under the current directory. I didn't write it in ACL2 because I didn't find a good portable way to "touch" a file in ACL2/LISP. As a Java JAR file, GUI users can double-click it and be finished. Command line users just change to the books directory and "java -jar touch_compiled.jar".
It has not been distributed with ACL2 images before Version 3.5, but the make-dist script has been updated to include the touch-compiled.jar file in future versions. It is just the class acl2s.lib.certify.TouchCompiledFiles, built in Eclipse by right-clicking acl2s/touch_compiled.jardesc and selecting "Create JAR" or "Open JAR Packager..."
Almost all ACL2s development can be done using the Eclipse SDK, which includes the Plugin Development Environment. To get it, start at http://download.eclipse.org/eclipse/downloads/. You should probably use the latest stable version, but as of July 2009, I have only used versions 3.4.x of Eclipse.
When you checkout the acl2s "trunk" from SVN, you get a lot of directories and some miscellaneous files. You should use this root directory as an Eclipse workspace. Many of the directories are Eclipse "projects" and should be "imported" into the workspace as such. If I do ls */.project, that tells me which directories are projects. Basically, there is a project for every standard plug-in and feature, a project for the update site, and some projects for experimental/testing purposes.
The acl2-image.blah projects for the image plugins do not need much attention in Eclipse., so I typically keep them "closed" to save memory. Also note that I do not commit most of their contents to subversion because it is huge and should be easy to recreate from an ACL2 build.
"acl2s-update" is an "Update Site" project. Eclipse 3.3 used something called "Update Manager" to install/upgrade components. It was pretty nice and worked pretty well. Eclipse 3.4 introduced a replacement, which I believe is called "P2" and it is terrible, buggy, or both. (See p2_complaints in trunk root.) P2 recognizes 3.3-style Update Sites--which Eclipse SDK actually knows how to develop--so that's what I run with ACL2s.
Building ACL2s feature: The key file for the site is site.xml. Double-clicking gives you a rich editor with some important functionality. This is where you want to build the "acl2s" feature, including its constituent "acl2s," "acl2s-hooks," and "acl2s-modes" plugins. Basically, you highlight the latest version and click Build. Note that once you release a version, you probably don't want to rebuild it, since users will not get the updates if they attempt to update. (In rare cases of "unimportant" updates, it is ok.) Important build note: To keep this from being treated as a P2 site, you have to remove a couple .xml files that are generated whenever you do a Build. (content.xml and artifacts.xml I believe.) (If you don't, the site looks like crap to users when they install/update.)
When you bump up the version number (by modifying it in the acl2s-feature project), you need to "Add Feature..." the latest version to the site. Versions you don't want people to use anymore should be (right-click) "Remove"d. You might have to manually delete the old files out of features/ and plugins/. These are where building puts the JAR files for the features and the plugins they include.
Building acl2-image features/plugins: Do not build acl2-images with the "Build" button. We use a script for that: "./build_imagestuff". The main purpose of this script is to build the JAR files in such a way that all other files will be extracted before the compiled files (.o or .fasl). This way, the compiled files should have a later write time, as ACL2 requires. Note that JAR files do not include modification time information, as tar files do.
The script also builds versions that can be downloaded and extracted off the web page under update/images. It recycles the JAR as a .zip for Windows and builds .tar.gz for Unix-like platforms. These are put in the acl2s-update/images directory.
Other notes: pkgs is a symlink to the prebuilt Eclipse+ACL2s+ACL2 packages, so that they can be found on the web page under update/pkgs. Since these are rather big and easy to rebuild, I generally let them live in a location that is not even backed up. Similarly, I do not commit contents of plugins/, features/, or images/ to the repository. They can be reconstructed with similar ease.
The documentation in acl2s-doc is on the web page. To make it easy to update version numbers, etc. on the web page, it is generated from a source file with some escapes that I replace using sed. See the Makefile. You should update version numbers in the Makefile and "make" for new releases. Also, you should edit src/index.html not index.html.
game.jar is for the Boolean logic game applet in game.html and built from game.jardesc in the acl2s Eclipse project.
acl2s-modes, acl2s-hooks, and acl2-images come with source code, with the exception of the underlying Common LISP. The acl2s plugin does not. Nevertheless, all the source code should be packaged up in acl2s-src, available on the web page as src/. In particular, I put C code and such in misc/, LISPs in lisp/, ACL2 in acl2/, our ACL2 extensions (hooks and modes) in acl2-extensions/ and Java plugin source in plugins/. There are scripts in plugins/ and acl2-extensions/ to build files with the source code. As a protection, they only build if there is no file for the current version. You should only build each version once, on release.
acl2s-eclipse-pkgs/ directory has a script and some files for building prepackaged Eclipse+ACL2s+ACL2. For each release, one needs to update build.sh with version numbers for everything and possibly the directories where things are stored. (TODO: Modify to extract most of the version numbers automatically.)
The basic idea is that we are going to take an Eclipse "platform" build (which does not include Java Development Environment and all that stuff) and add to it the appropriate ACL2 and ACL2s features and plugins. In fact, we start with the tar files not gzipped, so that we can just add files to the archive.
This works with Eclipse, because if we put features and/or plugins in the right place (features/ and plugins/), Eclipse will recognize that they are "installed". Thus, the user extracts one ZIP or tar.gz file of Eclipse with an ACL2 Image and the ACL2s plugins already "installed."
A lot of the magic in the script is in ordering files of an ACL2 Image in the archive. Recall that the write times of compiled files need to be after the respective .lisp files. For the Windows ZIP file, we have to order them in the archive to make that happen. The tar.gz files should preserve that information, but the program that extracts the tar.gz might not. Thus, it's best to order them appropriately in the archive as well.
There is another piece added to each archive, and that is in acl2s-eclipse-pkgs/eclipse/. It is configuration information that puts the ACL2s update site in the list of sites that is already set up. This makes it extra easy for users who download the prepackaged stuff to update.
The working copy of the acl2s-update site is what you get to with the http://acl2s.peterd.org/acl2s/update-testing/ URL. That is not committed to the web page until you do "./sync_www" from the trunk root of the repository. (If developing from another machine, modify and use "./rsync_acl2s_naxos_up".) That sync publishes the documentation, the source code, and the icons as well, but you need to be sure they are already built with your changes!
Using Eclipse in a multi-user setting is a little complicated, and ACL2s makes it a little more complicated.
Multi-user Eclipse: Eclipse is happiest when it is able to write to all of its files, so that things can be upgraded and configured easily. If I recall correctly, Eclipse will work around this if it is unable to write to the installation directory, by setting up a directory in the user's home--but only if you have never run that installation as a user that can write to the installation directory! If I recall correctly, it seems to expect to be able to write to the installation directory if it was ever able to write to the installation directory.
Multi-user ACL2s: Unfortunately, ACL2s is, in a way, worse about wanting to write to its own files, and there does not seem to be a simple fix for that. However, one can easily get ACL2s into a state in which it no longer needs to write to its own files, as long as users don't upgrade or try to move Eclipse to a different path. In particular, an acl2-image will need to update its .cert files the first time it is used in a particular path. Otherwise, no files in an acl2-image plugin need to be written to. Also, the "ACL2s system books" in acl2s-hooks and acl2s-modes need to be recertified the first time they are used (with a particular build of ACL2). Otherwise, no files in those plugins need to be written to. Files in the acl2s plugin never need to be written to.
Multi-user Eclipse+ACL2s: Now we have a dilemma, because we need to run ACL2s to certify the system books and start a session as a user who can modify the files, but we aren't allowed to start Eclipse as a user who can modify the files. The NEU computer labs do not really have the multi-user Eclipse problem because they use SoftGrid (see below), but others might not. The solution? You can perform these tasks outside of Eclipse. (By the way, you can effectively install Eclipse plugins without running Eclipse by unpacking them in the right place. See pre-packaged stuff below.) Execute run_acl2 in the acl2-image-blahblah plugin directory to update the .cert files. In the acl2s-hooks and acl2s-modes plugin directories, use the acl2-image to certify the required books, TODO: support needed; at least a script, but something more portable would be better
SoftGrid: Regardless, NEU CCIS computer labs use something called SoftGrid that does some magic to run "single-user" applications in a mutli-user setting. My understanding is that the user starts with a known good installation of Eclipse, and the SoftGrid system keeps track of the modifications made to that user's copy of Eclipse. Users can use it as if they have their own copy, even upgrading pieces if they so choose, but most of the structure is still shared among users. However, there is something a little mysterious about accessing files in SoftGrid. I think we had problems with the ACL2 image residing on the SoftGrid, and we used an alternate setup for the ACL2 image...
Alternate ACL2 Image Access: It is relatively simple to let the ACL2 Image reside outside of the Eclipse install. Recall "Finding ACL2 on the user's system" in the user documentation. One can extract the appropriate ACL2 image (from the update/images directory, without using Eclipse) to some shared location, and the environment variable ACL2_HOME can be preset for all users to that location. Remember to have a priviledged user execute run_acl2 once with it in the path from which it will be accessed. This is the setup in the CCIS computer labs, where ACL2 is in N:\arch-windows\acl2-3.4.