ACL2s: "The ACL2 Sedan" for Eclipse

Outline

• Introduction/Motivation
• Requirements/Platforms
• Installation and setup
  • of Java
  • of Eclipse
  • of ACL2s plugin & ACL2 image
  • of ACL2 outside of Eclipse (optional)
  • of Prepackaged Eclipse+ACL2s+ACL2
• Beginning Tutorial
• Guide to usage
  • Cheat sheet for ACL2s
  • Customization of Eclipse/ACL2s
  • Modes for ACL2 development
  • Classifications of ACL2 input
  • Descriptions of user interface actions, with key bindings
  • CCG: improved termination analysis
  • Data Definitions: specify data definitions
  • Random Testing: print counter-examples/witnesses in proofs
  • Book development
  • Tracing function execution in ACL2s
  • Graphics application support in ACL2s
• FAQs
  • about Eclipse
  • about ACL2
  • about Java
  • about ACL2s
• Implementation notes for ACL2 hackers
  • Source code for ACL2s
  • Finding ACL2 on the user's system
  • Wrapping the ACL2 process
  • Hooks: How/what ACL2 functionality is modified for ACL2s
  • How undo and redo are implemented
  • How modes are implemented
• Contact info

ACL2 is a powerful system for integrated modeling, simulation, and inductive reasoning (see What is ACL2?). Under expert control, it has been used to verify some of the most complex theorems to have undergone mechanical verification. In addition to its maturity and stability, these qualifications make it a good platform for learning about industrial-strength theorem proving. Unfortunately, ACL2 has a steep learning curve and with its traditional tool support is analogous to a racecar: it is powerful, but it take expertise to operate properly.

We want to make tool support for the ACL2 platform that is more analogous to a family sedan; hence, the "ACL2s" or "ACL2 Sedan" name. With just a little training, a new user should be able to drive slowly on paved streets without worrying about oversteer, tire temperature, or even engine RPMs.

Pushing aside the analogies, ACL2s includes powerful features that provide users with more automation and support for specifying conjectures and proving theorems. This includes CCG termination analysis and random testing. In addition, ACL2s is "safer" by constructing and enforcing abstractions based on what is meaningful interaction with ACL2. For example, unlike the traditional ACL2 development environment (the command-line theorem prover and Emacs), pressing Return at the command prompt in ACL2s does not send any input to ACL2 until a single, well-formed input expression is completed. Unlike Emacs, ACL2s stops automatically sending input to ACL2 if something fails. Undoing in ACL2s is simple and natural; in other ACL2 environments, however, one has to figure out for oneself the command to undo to a particular point, while watching for critical commands that evade the traditional undo mechanism.

We have implemented our tool as a plugin for the Eclipse development environment (see What is Eclipse?). In addition, the plugin requires some extra functionality from ACL2 that is not included in the main distribution. This functionality is largely hidden from the user and shouldn't alter ACL2's behavior for all practical purposes. To be sure, though, users can certify their work in a clean ACL2 session (see Book development).

ACL2s is not completely mature in its capabilities, but industrial and academic users alike should find it stable enough, intuitive enough, and capable enough to meet their needs. Ideally, the tool will become even more intuitive, self-teaching, etc. in the future.

To run Eclipse and our plugin, you need a "J2SE 5.0" (minimum) runtime environment (such as Sun's "JRE 5.0") or SDK (such as Sun's "JDK 5.0"). For Linux and Windows, see Sun's J2SE download site. For Mac OS X, see the Mac OS X Java support page, though Eclipse reportedly does not run under 64-bit Java SE 6 for Mac OS. Any downloads will be specific to your platform and will come with installation instructions.

See our FAQ section on Java if you want some clarification on the requirements.

Note: At this point, you can may elect to skip to Prepackaged Eclipse+ACL2s for easier, basic installation on supported platforms.

Our plugin is currently developed for Eclipse versions 3.5, but versions 3.3.x and upward are still supported with some minor inconveniences. See the Eclipse Project download page for the latest downloads, but Release Build 3.5 is a known compatible version. Basically, if you think you might want to do Java development in Eclipse, splurge for the full "Eclipse SDK", which will be a file named eclipse-SDK-3.5-<your platform here>. If you're only going to use Eclipse for ACL2, the minimal version is the "Platform Runtime Binary", with the file named eclipse-platform-3.5-<your platform here>. Be sure you choose between x86, x86_64, and PPC architectures correctly! And note that x86_64 depends on your operating system and JVM being 64-bit.

IMPORTANT: Windows 7 Users and other 64bit Windows Users need to install 64bit Java and choose Windows(X86_64) Eclipse Platform to download.

Install

If Java is installed properly, Eclipse installation is simple on all platforms. Simply decompress (unzip or untar/gz) to the directory where you want Eclipse. Make sure this directory has no spaces in its path, avoid 'My Documents', 'Program Files' which are common on Windows. Preferably use C:\Users\yourName\tools\eclipse. The other caveat is that you should do this as the user who will be running Eclipse. See Can I do a multi-user install of Eclipse? for more info.

To get started, run the "eclipse" executable. This could involve either browsing to it and double-clicking the icon or running it from a command line. If Eclipse can't find your Java VM, see How do I run Eclipse--with the right options? below.

Ubuntu 9.10(Koala) users: If you have trouble with buttons in Eclipse, read about this fix.

The first time you run Eclipse, it will prompt you for a "workspace" location. This is where Eclipse will save your configuration and layout and is the default location for projects and their associated files. The default should be fine--unless you are using Windows and the default is on a network share path. (ACL2 does not understand network share paths.) In that case you should "Map network drive" in Windows and use a path on that drive.

If you get a welcome window, you can click the "Go to workbench" icon to get to the Eclipse "workbench".

In Eclipse version >= 3.5, (click here for old Eclipse 3.4 updater instructions)

• Help | Install New Software..
• Click the "Add..." button near top right and enter Name: ACL2 Sedan and enter Location:

  http://acl2s.ccs.neu.edu/acl2s/update

• This should reveal an "ACL2 Images" and an "ACL2s Components" category.
• Under "ACL2s Components," be sure to select "ACL2s" (0.9.9.3).
• If you don't have your own installation of ACL2, you should expand "ACL2 Images" and select ONLY ONE of the ACL2 Images there, the one that fits your platform and architecture.
• After making your selection, click "Install..."
• Double-check that you aren't installing more than one "ACL2 Image". (Apparently, Eclipse 3.4+ will happily install things that are marked as incompatible with your system, while Eclipse 3.3 would not.)
• Read and accept the license agreement and click "Next" and/or "Finish" until it's installed.
• Restart Eclipse as recommended.

Once you've restarted Eclipse, test that the plugin is loaded by typing Ctrl+N (+N on Mac) in Eclipse to bring up the dialog for selecting a wizard for creating a new file. There should be an ACL2s category with a wizard for "ACL2s/Lisp file". Select that and click "Next >." If the wizard comes up, you are good. If you get an error when trying to open the ACL2s/Lisp wizard, you might be using a version of Java that is too old (see How do I run Eclipse--with the right options? and How do I tell what Java version Eclipse is running under? below, remembering that the Java version needs to be >= 1.5.0). If there is no ACL2s category, Eclipse is not loading the ACL2s plugin, which probably means it was not installed properly or you haven't restarted Eclipse.

If you already have ACL2 Version 3.6 to 3.6.1, based on GNU Common LISP (GCL), Steel Bank Common Lisp (SBCL), or ClozureCL/OpenMCL, then you can use that with the current version of ACL2s without installing the "ACL2 Image" in Eclipse. In this case, refer to how the plugin locates/runs ACL2. You can also build ACL2 yourself, but the "ACL2 Image" we distribute for supported platforms is prebuilt with standard books precertified. (To use these in Eclipse, install from the update site; otherwise, you can get them from here.) We even have mechanisms to automatically adapt the .cert files to whatever absolute path it's installed into. Our images are based on SBCL for Unix-clone platforms and on CCL for windows. (We would have uniformly liked to use SBCL, because its fast and reliable, but SBCL for Windows lacks interruption--an important feature.)

Prepackaged Eclipse+ACL2s+ACL2

For quick and easy install on supported platforms you can simply unpack a prepackaged Eclipse install tree that includes the ACL2s Plugin and ACL2 Image out-of-the-box. You should be able to "Unpack and Go (on to the tutorial)". See http://acl2s.ccs.neu.edu/acl2s/update/pkgs/ for the list of available packages. Choose based on your operating system and architecture.

Some notes:

• macosx-ppc is for G3/G4-based Macs, such as the old Powerbooks and iBooks.
• macosx-x86 is for Intel-based Macs, such as MacBooks and MacBook Pros.
• linux-x86 is likely to work only on 32-bit Linux. The 32-bit Eclipse depends on 32-bit GTK libraries, which are not typically available on 64-bit (amd64) Linuxes.
• linux-x86_64 will work only on 64-bit Linux. On linux, if you have trouble starting Eclipse, especially if you're using Ubuntu, read about these possible fixes.
• win32-x86 is for 32bit versions of Windows XP and later, and will not work for 64-bit versions of Windows. So even if you have a x86_64 processor, if you are running a 32bit OS, then use this image.
• win64-x86_64 is for 64bit versions of Windows XP and later, and will not work with 32-bit versions of Windows.

To familiarize yourself with some Eclipse vocabulary and navigating the workbench, we recommend going through the "Basic Tutorial" section of the Workbench User Guide.

Create a project: Select File | New | Project... and select Project from the group General. Give a name to the project that will contain your ACL2 developments and click Finish.

Open the "ACL2 Development" perspective: Select Window | Open Perspective | ACL2 Development. You could have instead clicked on the icon in the top-right corner. The new perspective will change the layout of your workbench.

Create a new Lisp file for getting the feel of Eclipse and our plugin. Select File | New | ACL2s/Lisp file. The "Directory" should already indicate the project you just created. If not, browse to the project you just created. Pick a file name like "test.lisp" or leave the default. Use "ACL2s" for the mode and click Finish.

You can now type some ACL2 code in the editor. Type in this definition to get the feel of the auto-indenting, paren-matching, and syntax-based coloring:

; Computes the nth fibonacci number (maybe?)
(defun fib (n)
  (if (and (integerp n) (< n 2))
    (+ (fib (- n 1)) (fib (- n 2)))
    1))

Moving on

Upon creating the new file, an editor has now opened in the editor area of the workbench. Around the editor area are views, such as the Navigator view to the left and Outline view to the right. From their title areas, these can be dragged around, tiled, minimized, etc. You probably also noticed that "(defun fib (n)" showed up in the Outline view, which you can use to navigate the top-level forms of your file.

In the Navigator view, which is a tree view of projects and files, expand your project to reveal a few files:

• .project - a file used by Eclipse to store project-specific settings.
• test.lisp or whatever you called it. This will contain ACL2 code your write.
• test.lisp.a2s - a file created automatically when you opened test.lisp. This file will store the history of ACL2 sessions you open to develop test.lisp.

Open test.lisp.a2s by double-clicking it in the Navigator. Alternatively, hit Ctrl+Shift+o (Mac: +Shift+o) in the editor for test.lisp. This is the key sequence for switching between corresponding .lisp and .lisp.a2s editors, opening the other if necessary. You should now be in an editor that has a little message "No session running" at the top and won't let you type anything. This editor is read-only when no session is running.

Start a session for testing our code in test.lisp by clicking the icon in the toolbar.

After this bookkeeping, you should be able to click the "restart session" icon on the toolbar and have ACL2 start up, resulting in the "ACL2 >" prompt.

Type an "immediate command" for ACL2, such as (* 21 2) in the session editor (.a2s editor). Notice that the editor is read-only except for the part after the last prompt. Hitting Enter (Return) at the end of this editor will submit the typed form to ACL2. Actually, it will only submit syntactically valid commands to ACL2, so if one tries to trick it by hitting Enter after just (* 21, the editor just goes to the next line.

Try submitting other types of input to ACL2. (* 21 2) was classified by the plugin as "VALUE" input, because it's just computation that returns a value. Another example is a "QUERY" such as :pe strip-cars, which prints out information about the current history or "world", in this case the definition of the function "strip-cars". (defun succ (x) (1+ x)) is an "EVENT" because it (potentially) changes the history. See Command Classifications in the guide for more detail. For "EVENT" inputs, ACL2s pops up a dialog asking what to do about the fact that we did something logically relevant from the command line rather than from our source code. Read the dialog and for now choose "Insert".

Try submitting something with an error such as (succ 1 2)--an error because the arity of the succ function we just defined is 1. The red (maroon, I guess) output indicates the command was not successful. ACL2 is back in the state it was in before you submitted the form that caused the error.

Line action

Switch back to the .lisp editor where you will discover the (defun succ (x) (1+ x)) form we submitted in the session editor has been "inserted" above what we had typed previously! Also, that form is "above the line" and read-only. This is part of the intrinsic linkage between somename.lisp and somename.lisp.a2s: the forms "above the line" in the .lisp editor are those used to get the ACL2 session in the .lisp.a2s editor in its current state. To maintain this invariant, we have to do one of two things in the case of executing something history-relevant in the session editor: insert it at the line in the lisp editor or undo it. These are the options the "Relevant input at command line" dialog gave us. Note that "QUERY"s and "VALUE"s do not modify the history, so we don't need to insert those above the line.

Try moving the line past the definition we gave for fib by pressing the "advance todo" button on the toolbar ( or Ctrl+Shift+I on PC or +Shift+I on Mac). Watch carefully and you will see the definition for fib flash green. Because it did not turn from green to gray, our definition of fib was rejected by ACL2. Also, if the "Proof Tree" view is open (probably left), it might show some information about a failed termination proof that caused ACL2 to reject the definition.

Here is some more detail on the meaning of the green and gray highlighting:

The plugin models two "lines" in a .lisp file: the "completed line" and the "todo line". These "lines" are only visible as the boundary between regions with different highlighting. The "completed line" is at the last point of gray (or blue) highlighting. The "todo line" is at the last point of any highlighting: gray, blue or green.

Above the "completed line" is the (potentially empty) "completed region," which has forms that ACL2 has--get this--completed. Between the two lines are forms that we want ACL2 to work on completing (hence "todo"). This (potentially empty) region, the "todo region", has green highlighting. We can call the rest of the buffer the "working region", which is the freely editable part.

So what was the meaning of the flash of green highlighting? Clicking "advance todo" moved the "todo line" from between (defun succ ...) and (defun fib ...) to after (defun fib ...). With at least one form in the "todo region", the session started processing the first (and only) one. If you look at the session output, you see that the attempt to admit our fib function failed. The attempt to prove termination failed. If the next "todo" form fails, the plugin moves the todo line back to the point of the completed line, "cancelling" the todo operations and prompting the user to fix the rejected form.

Fix our fib definition: the previous one had parameters to the < comparson swapped. ACL2 admits this one:

; Computes the nth fibonacci number
(defun fib (n)
  (if (and (integerp n) (< 2 n))
    (+ (fib (- n 1)) (fib (- n 2)))
    1))

If you want to add some configuration input to be loaded with each interactive session, use an acl2-customization file. This can include your own configuration to be done after the session mode is loaded and configured. This should not include events, which should be specified or explicitly loaded in the source code. In fact, we do not load the acl2-customization for certification. Also note that ACL2s does not respect the environment variable for acl2-customization. Also note that acl2-customization is only loaded in some modes (see below), unless overridden in the preferences.

In addition to removing prover restrictions present in introductory modes, these modes are more friendly to customization. By default, ACL2s will only load acl2-customization files in non-introductory modes. (There is a preference controlling this.)

Additional advanced note: Another feature of all these modes except "Compatible" is doing destructor elimination before laying down a checkpoint. Thus, the checkpoint summary will show the formula after destructor elimination. The downside is that the variable names may appear cryptic and unfamiliar, but the upside is that you get some generalization for free, usually resulting in smaller formulas.

Notes about how these modes are implemented are described in How modes are implemented.

Descriptions of UI Actions

The keyboard bindings for these actions are user modifiable through Eclipse's preferences, which is under the Window menu or the Eclipse menu depending on platform. The settings are under General > Keys, and show up beside their location in the application menus (under ACL2 or Navigate).

Mac OS X Note: The keybindings below are for PC users. The Mac equivalents (if available) are the same except that Ctrl+Shift is replaced by +Shift. For example, Interrupt is still Ctrl+Break (if you have a Break key), but switching editors is +Shift+o.

Navigation (appear under "Navigate" menu)
"Go To" | "Corresponding ..."		This switches which editor has keyboard focus. If you are in a .lisp file, it switches to the corresponding .a2s editor, opening it if necessary. Vice-versa if starting from an .a2s editor. The keyboard shortcut is Ctrl+Shift+o (since it is related to emacs' C-x o).
"Go To" | "Matching Character"		If the character behind the caret (cursor) is matched to another (such as ( and ), or " and "), then this action moves the cursor just beyond the match. Invoking this action twice in a row should have no net effect except in the case of going from a , to its matching `, which could potentially have many commas matching to it. The keyboard shortcut is Ctrl+Shift+P (as in Eclipse's Java Development Environment).
"Down/Up to Next/Previous Session Input" (.a2s only)		These allow the user to navigate through the session history by moving to the beginning of the next/previous command in the history. If, for example, one is at the bottom of a failed proof attempt, one can navigate to the beginning of the command that initiated it with Ctrl+Shift+Up. "Next" is bound to Ctrl+Shift+Down. One can go to the end of any buffer with Ctrl+End (Eclipse binding).
"Down/Up to Next/Previous Checkpoint/Input" (.a2s only)		These grant the user finer-grained navigation through the session history than the above by also visiting checkpoints in proof attempts. For a description of checkpoints, see :DOC THE-METHOD. "Next" is bound to Ctrl+Shift+Right and "Previous" is bound to Ctrl+Shift+Left. Thus, to go to the first checkpoint of the previous form's output, type Ctrl+Shift+Up, Ctrl+Shift+Right.
"Next/Previous/Last Command in History" (.a2s only)		The .a2s editor keeps a history of acl2 forms that have been submitted as "immediates" (typed in the .a2s editor). One can navigate through this history in much the same way one can navigate through a shell history, or a history of ACL2 commands (assuming readline support). Previous: Ctrl+Shift+, (comma); Next: Ctrl+Shift+. (period); Last/Current: Ctrl+Shift+/ (slash). Actually, two orthogonal histories are maintained. One for immediates submitted as command forms and one for miscellaneous input, such as input to the proof checker. The command history for each is available only when the session has prompted for that type of input.
Session-related
Submit Immediate		When ACL2 is running and waiting for input, one can type input forms directly into the .a2s buffer. We call these "immediates." Whenever Enter (sometimes called Return) is typed at the end of the .a2s buffer, we check to see if some prefix of the typed input is a valid, complete input form. If so, the Enter is interpreted as submitting the form. If not, the Enter is inserted, as in a traditional editor. Ctrl+Enter ignores the location of the caret and will submit the first complete, valid input form if there is one. If the form submitted is relevant to the logical history, (i.e. not a QUERY or VALUE), the user will be queried on whether to insert it at the "completed" line point in the corresponding .lisp file or to immediately undo it. This is to maintain the invariant that the forms above the "completed" line in the .lisp file comprise the logical history of the session.
"Clean Session"		Opens a dialog box with options to clear the session history, the typed command history, and others. Clearing the session history will stop the associated ACL2 session (if running) and move the "completed" line in the corresponding Lisp file to the top. Forgetting REDO information is useful for including updated versions of the same book. Note that some of these actions are not readily reversible, if at all, so use them cautiously. Shortcut: Alt+Delete.
"(Re)start Session"		Starts a fresh, new ACL2 session, with its output going to the current or corresponding .a2s editor. If an ACL2 session was already running in that editor, it is stopped/killed. Depending on user preferences, the dump of previous sessions may or may not be cleared. Shortcut: Alt+Home. In the corresponding Lisp file, the "completed" line is moved to the top. The "todo" line is left where it is, meaning forms that were done or still left "todo" in a previous session will start being read and loaded automatically. To avoid this, use "Stop session" (optional, but takes ACL2 interaction out of the operation) and "Undo/cancel all forms" before "(Re)start Session".
"Stop Session"		If ACL2 is running in this (or the corresponding) .a2s editor, stop it cleanly or kill it. Regardless of the state it was in before, ACL2 is *not* running in this editor after "Stop Session" is pressed. Shortcut: Alt+End In the corresponding Lisp file, the completed line is reset and the todo line is left where it is.
"Interrupt Session"		If ACL2 is processing a command form, this will break it back out to the top-level prompt. This is most commonly used to interrupt the execution of some evaluation that will take too long, or to abort what seems to be a divergent proof attempt. As a nod to times passed, we bind this to Ctrl+Break. "Interrupt Session" often has the same effect as "Cancel all 'todo' forms," because if the form being processed by ACL2 is the next "todo" form, either action will both interrupt ACL2 and (because an interrupted form is not successful) move the "todo" line back to the "done" line.
Line-related
"Undo/cancel all forms"		This moves both the "completed" line and the "todo" line to the top of the .lisp file. ACL2 need not be running, but if it is, this will cause anything currently executing to be interrupted, and all completed forms to be undone in LIFO (last-in, first-out) order. (No default shortcut) The large double arrows in the icon are intended to portray moving the line all the way to the top.
"Undo/cancel last form"		If there are any "todo" forms, the last will be cancelled. If it was currently being executed by ACL2, it will be interrupted. If there were no "todo" forms, both lines will be moved up one form, and if that form was relevant to the logical history, it will be undone in the ACL2 session. ACL2 need not be running to use this action. Shortcut: Ctrl+Shift+M This has changed from 0.9.6 to accomodate for GNOME users. To restore this binding to Ctrl+Shift+U, go to Window->Preferences->General->Keys and change the "Retreat Line" action's binding. The small arrow in the icon is intended to indicate the undoing of a single form.
"Cancel all "todo" forms"		The "todo" line is moved to be even with the "completed" line. If the next "todo" form was being processed by ACL2, it is interrupted. (No default shortcut) The large arrow next to green text in the icon is intended to indicate the undoing of all "todo" forms.
"Advance todo line"		The "todo" line is advanced by one command form. This will often cause ACL2 to start processing "todo" forms. Many forms are completed by ACL2 so quickly, that there is but a flicker before the "completed" line is moved as well. ACL2 need not be running to use this action, but it won't trigger ACL2 to start. Shortcut: Ctrl+Shift+I The small down arrow in the icon is intended to indicate the advancement of the line by a single form.
"Move todo up/down past cursor" (.lisp only)		If the "todo" line is above the cursor, it is advanced until it reaches (or passes) the cursor. If the "todo" line is below the cursor, it is retreated until it passes the cursor. Note that invoking this action repeatedly in the same spot will have a sort of "toggle" action on the form under or immediately after the cursor. Shortcut: Ctrl+Shift+Enter The up and down arrows in the icon are intended to indicate moving the line in either direction to get to the current spot. This is the only line action valid in "No Line" mode, in which it has a special (but obvious) meaning: it submits the command form under or following the cursor to the associated session (if exists, running, and ready) and advances the cursor past the submitted form.
Misc
Auto-complete (content-assist)		In the .lisp editor, you may press Ctrl+Space to auto-complete your function/macro names, parameter names, let bindings or defconsts. The functions and constants defined in ground theory ACL2 are also auto-completed. If a session is open, then any defined function, macro or defconst in the world will also be auto-completed.
Indent code		In either the .lisp editor or the immediate area of the .a2s editor, the Tab key indents lines spanned by the current selection (or just the line containing the caret) according to some built-in rules. Not all lines will have their indention changed by this operation, such as lines whose first non-whitespace characters are ";;;".
Select s-exp		In either the .lisp editor or the immediate area of the .a2s editor, Ctrl+Shift+Space selects (highlights) s-expressions, to help with cutting and pasting mostly. If nothing is highlighted, the smallest s-exp "under" (and to the right) of the cursor is selected. Sometimes a single token that is not itself an s-exp (such as ")") is highlighted. Hitting Ctrl+Shift+Space with something already selected selects the next larger s-exp that contains the selected region. Thus, hitting this sequence repeatedly selects larger and larger s-expressions until an entire top-level form is selected. Using this sequence to select a symbol causes all lines with occurrences of that same symbol to be marked. Selecting a non-symbol clears the markings. This is helpful for finding definitions and uses of functions and variables.
Certify as book		See book development. Alt+C
Recertify ACL2s system books		This should only be needed if an ACL2 session fails to start up and asks you to do this. This could happen, for example, if you change the version of ACL2 you are using with ACL2s.

Our CCG termination analysis is highly customizable and includes many features not mentioned here. For detailed documentation please refer to :doc ccg.

For detailed documentation please refer to :doc data-definitions.

For documentation on usage and settings please refer to :doc random-testing.

An ACL2/ACL2s book is a reusable collection of definitions and other events (embedded event forms, actually). A valid book can be certified to demonstrate its validity and/or to prepare it for inclusion elsewhere.

To develop a .lisp file as a book in ACL2s, either create the file using the ACL2s/Lisp file wizard selecting "Create with book code", or put this at the top/beginning:

(begin-book t :ttags :all)
(in-package "ACL2")

After the begin-book and in-package come the definitions and other events for your book. As one is developing a book, it is very helpful to use the line action discussed above for interactive development. One difference is that everything starting from the begin-book form that is in the "completed" region will be highlighted blue as long as it is valid for use in a book (see EMBEDDED-EVENT-FORM). Any tangent from book-valid forms will begin gray highlight. Such tangents should eventually be undone and removed before certification.

To ensure your book is valid/certifiable, save your changes and choose "Certify as book" from the menu or toolbar (). An Eclipse console will dump the output of the certification process and indicate success or failure when finished.

More detail

In ACL2s, a (begin-book ...) form in a .lisp file has special significance, indicating the .lisp file is intended to define a book. Our approach might seem strange at first, but it really works pretty well with the seemingly obscure requirements ACL2 has for books. This and the next subsection get into the details and the justification.

The preamble is everything that comes before the begin-book. This defines what ACL2 authors call the certification world for the book, which become the book's portcullis. The simplest explanation for the preamble/portcullis is that it is where any defpkg events should go, because these are not allowed inside books (because Common Lisps vary in their ability to compile files that define packages).

The begin-book form itself takes the syntax of ACL2's certify-book except begin-book doesn't take the "book-name" or "k" parameters. In fact, here are the parameter and guard specifications for ACL2s's begin-book:

(defmacro begin-book (&optional (compile-flg 't)
                      &key (defaxioms-okp 'nil)
                           (skip-proofs-okp 'nil)
                           (ttags 'nil)
                           (save-expansion 'nil))
  (declare (xargs :guard (and (booleanp compile-flg)
                              (booleanp defaxioms-okp)
                              (booleanp skip-proofs-okp)
                              (member-eq save-expansion '(t nil :save)))))
  ...)

So the parameters to begin-book indicate the parameters that should be given to certify-book for certification of the containing .lisp file as a book. One can look up the meaning of the compile-flg, defaxioms-okp, skip-proofs-okp, and save-expansion arguments from ACL2's documentation for certify-book. But the ttags argument is important in ACL2s:

ACL2s session modes other than "Compatible" mode utilize ACL2 extensions that ACL2 cannot verify are sound or even safe. These modes include books for ACL2s that define trust tags or ttags in order to tweak ACL2 in non-standard ways. In order to certify a book that depends on the use of trust tags, including books defined in a mode other than "Compatible", an appropriate :ttags argument must be given to begin-book. We recommend the all-encompassing :all argument to :ttags, which roughly says, "I recognize this book could depend on some non-standard stuff, and I don't want to bother specifying the details. Just go ahead." See the docs for ttags-seen and certify-book for more information on how to be more specific.

The contents or body of a book is everything after the begin-book form as long as it conforms to ACL2's requirements for book contents. Basically, the first form must be (in-package "blah") where blah names a built-in package (such as ACL2 or ACL2-USER) or a package defined in the preamble. (The wizard for "New ACL2s/Lisp file" can generate appropriate "book code" that defines a package in the standard way, begins the book, and enters the defined package.) After the (in-package "blah") form are embedded event forms using blah as the default package. In ACL2s, embedded event forms have the input classification EVENT or EVENT/VALUE.

Book code in the completed region is formatted specially. The preamble looks like any other non-book .lisp file, and so uses gray highlighting. The begin-book form begins the part that distinguishes this .lisp file as a book, and so begins blue highlighting. The blue highlighting continues either until the end of the current "completed" region, or until the end of the last form that was valid as the contents of a book. This visually tells the user whether and where the book contents have became polluted with code disallowed in books.

We call anything after a valid book body a tangent, which is given gray highlight in the completed region. A tangent might be intentional; the user might want to try things in ACL2 without the restrictions imposed by book development and later undo his work and clean it up for use as book code. Any .lisp file with a tangent (that hasn't been commented out) will not certify, and we cannot forsee any case in which ACL2s would falsely report a form as tangential.

The tracing is active as long as the trace* form is in the completed region of your source code. It is true that tracing has no impact on ACL2's logical world, but tracing does depend on ACL2's logical world. So at least for now, we consider trace* to be "relevant". Calls to trace* are classified as COMMAND, which means they are not allows in books.

It is ill-advised to trace functions built into ACL2. Such functions are likely to be used by ACL2 itself, so you are likely to get mounds of output that originates from the operation of ACL2 itself before you get the output you are looking for. One can effectively trace one's own uses of a built-in function by writing a simple proxy function that directly calls the desired function, replacing your uses of the built-in function, and tracing the proxy. For example:

(defun my-butlast (lst n)
  (butlast lst n))

(trace* my-butlast)

If one attempts to use tracing in "Compatible" mode, you might get this output:

1> !! Warning: guard-checking is not :none, so trace    !!
   !!   output could be misleading or appear incorrect. !!
   !!   (see :DOC set-guard-checking)                   !!
   (REV '(1 2))
  2> (APP NIL '(2))
  <2 (APP NIL '(2))
   = '(2)
  2> (APP '(2) '(1))
  <2 (APP '(2) '(1))
   = '(2 1)
<1 (REV '(1 2))
 = '(2 1)

ACL2s supports development of simple graphical applications, inspired by some teachpacks in DrScheme and DrACuLa. We intend this to be a motivational pedagogical tool, so that students can prove theorems about something they can literally see in action and play with.

A basic API is available by including a book from the ACL2s system books,

(include-book "graphics" :dir :acl2s :ttags :all)

Advanced note: Although this is an ACL2 book, the graphical capabilities are provided by the ACL2s plugin to Eclipse, so you won't be able to use graphical applications outside of ACL2s, but you can certainly reason about them in ACL2 without ACL2s. In fact, if an astute ACL2 user decomposes this book, he/she will find logical underpinnings that enable reasoning not only about pieces of a graphical system, but about the reactive behavior of the overall system. But this "public" book is designed only for reasoning about the pieces in isolation.

In the following API, a "configuration" is an abstraction of the current state of the graphical world, and this abstraction is whatever the user of the API wants it to be. The user can register a function to construct a "presentation" from this "configuration", which will be used to re-present the graphical world after each event/update.

At present, the graphics are limited to a single window with a square canvas and a textual status line at the bottom. Events are limited to timer events, mouse clicks, and key presses that correspond to printable characters. (Sorry, arrow keys.)

The API includes some EVENTs for registering event handler routines & data:

The API also includes some functions for constructing/modifying "presentations".

Unlike what one might expect, X and Y coordinates (and widths and heights) are given as ratios (rationals from 0 to 1) of the entire canvas. This allows one to specify what the presentation should look like supposing it is not composed of discrete pixels. Working directly with pixels would allow one to make the displayed result as "pretty" as one wants, but this library is intended to discourage such tweaking in favor of focusing on the "concept" of the presentation.

Colors are specified in several ways, including all of the ways to specify a color as a string in HTML. Some examples include "#A080FF", "blue", :gray, 'violet and '(255 0 127).

Image paths are strings and interpreted by Java in the expected, OS-dependent way, except that forward slashes are always permitted as a directory separator character (for portability). Paths can be absolute or relative to the directory containing the .lisp file, such as "abc.png", "../images/foo.jpg", or "/home/me/pics/me.jpg" (unix/mac specific); relative is preferred for easy packaging of images with your source code. The image files themselves can be PNG (recommended for drawings/text), JPG (recommended for photos/scenes), and possibly others. PNG transparency is supported.

Here are the functions:

Finally, to run your graphics program, execute (big-bang), which should open a new window, etc.

Here is an example .lisp file that has the graphical skeleton of an Othello/Reversi game. It shows the board and you can switch a spot between white, black, and empty by clicking it. The logic of the game (what's legal, whose turn it is, what should happen in response to certain actions, etc.) is not included.

Here is the source code download directory, which contains source code for ACL2, for distributed Common Lisps, and for the ACL2s Eclipse plugin. The "ACL2s hooks" and "ACL2s modes" parts already includes source code, and are available from the update site plugins directory.

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.

Wrapping the ACL2 process

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:

• preinit.lsp - disables raw Lisp debugger, which must be disabled because we can't tell for sure when/what kind of input it is expecting. This file often includes other version-specific tweaks and fixes. (This file is loaded by raw Lisp.)
• acl2s.lisp - the main "hooks" book, which includes the "hacking" books now distributed with ACL2 and the rest these hooks books:
• canonical-print.lisp - functions for printing things... in a canonical way! (for reading by the acl2s plugin)
• acl2s-book-support.lisp - installs the BEGIN-BOOK function (see book development), which is the interactive stand-in for certify-book.
• categorize-input.lisp - functions for (you guessed it...) categorizing inputs to ACL2. Note that categorizing inputs is an example of the plugin executing commands in ACL2 that are unseen to the user.
• super-history.lisp - implements the "super-history" mechanism of UNDOing and REDOing. See "How undo and redo are implemented".
• protection-hooks.lisp - implements a protection mechanism by which only those with knowledge of a secret number (the plugin) can invoke certain actions, such as UNDOing, REDOing, quitting, or breaking into raw Lisp. Only a hash of the secret number is stored in the ACL2 runtime. You could defeat the protection with your own trust tag, but I challenge you defeat it without using trust tags!
• interaction-hooks.lisp - this redefines internal ACL2 functions to provide metadata output that is sucked up (hidden) by the plugin and used to inform it about interaction. Most importantly, extra environment information is sent with the prompt, a special marker is sent in the case of a form being successful, and a special marker is sent whenever ACL2 is about to read another object from *standard-oi*. The plugin is now also given all of the package definitions so that they can be used in determining whether abstract syntax is the same in checking whether REDO is allowed.
• markup-hooks.lisp - the markups in this book are not critical to intelligent interaction with ACL2, but add some extra helpful info, such as the position of checkpoints in the output. Along these lines, somewhere in startup stuff we remove destructor elimination as a checkpoint-causing processor, since destructor elimination cannot reduce theorems to non-theorems (confirmed by Matt Kaufmann).

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. ;)

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":

<?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:

• book_dev - whether book development/certification should be allowed in this mode (default true)
• extra_imports - any extra symbols that are suggested to be imported into packages defined under this mode, aside from the ACL2 standard set
• init_file - the file with the forms to execute at startup to initialize the mode. These should not refer to the current directory (instead use :dir :whatever). If book_dev is true, the forms should follow the guidelines for a .acl2 file, or commands that are okay prior to certify-book. We recommend the whatever-mode.lsp naming convention.

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.

Up to version 0.96, the main developer has been Peter Dillinger, advised by Pete Manolios. Since then, the main developer has been Harsh R Chamarthi, advised by Pete Manolios. CCG termination analysis is by Pete Manolios and Daron Vroon.