ACL2s: "The ACL2 Sedan"
Current version 126.96.36.199 (with ACL2 version 6.0.0)
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.
Any platform that can run Eclipse, Java >= 1.5 and <= 1.6, and ACL2 will support our system, but we specifically support these platforms (making installation easier):
Linux on x86 (32 or 64 bit) - Any reasonably recent version of virtually any distribution will work.
Windows on x86 (32 or 64 bit) - All versions Windows 2000 and newer should work.
Mac OS X on x86 (32 or 64 bit) - We require J2SE 5.0 or 6.0, which requires OS X >= 10.4.
|IMPORTANT: ACL2 images we provide depend on the platform and OS. So the image for 64bit Windows will *not* work on a 32bit Windows machine and vice-versa. Please choose your platform correctly. Refer to Is my OS 32 bit or 64 bit? in the FAQ.|
The minimal install of all components will consume about 300MB of disk space. Full install of all will be around 500MB.
Because Eclipse is exceptionally modular, written to be easy to hook into and extend, and it runs in Java, it is slower than one might expect, especially on Windows or Mac OS. It is quite usable on my old laptop running Linux (900mhz + 256MB of RAM), but I would not recommend running it on anything much slower. I would also caution against running Eclipse over a network filesystem, unless it is very fast and reliable.
For quick and easy install on supported platforms you can simply unpack/unzip a prepackaged Eclipse install tree that includes all of ACL2 Sedan and works out of the box. Make sure you unpack it to a path which has no spaces and where you have write permissions (for example /Users/peterd/tools). The other caveat is that you should do this as the user who will be running Eclipse. See http://acl2s.ccs.neu.edu/acl2s/update/pkgs/ for the list of available packages. Choose based on your operating system and architecture (Important: If you dont know wether your OS is 32 or 64 bit, check the faq). Once you have unpacked, go into the unpacked folder, double-click on Eclipse icon or type ./eclipse in the command line and go on to the tutorial.
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 or too new (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 and <= 1.6.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. Check out the faq for troubleshooting the problem.
Updating your old setup to the latest ACL2s version is easy:
In your working Eclipse, from the menu on the top, select Help | Check for Updates .... If there is a newer version available, a window will pop up with the latest versions of ACL2s and Eclipse, unselect the Eclipse, but keep the ACL2s checkbox selected and press Yes/Next. Once the update finishes, it will ask you to restart and delete some old files, say Yes. On restart, you might need to repeat through some bookkeeping (fixing .cert files and acl2s system book recertification).
Assuming you have Eclipse running with our plugin (as described above), we will now guide you through the process of creating a new ACL2s/Lisp file, typing definitions into that file, opening up an associated ACL2 session, sending definitions to the session, querying the session, etc.
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".
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))
Upon creating the new file, an editor has now opened in the editor areaof 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:
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.
The first time you start a session, there is some bookkeeping that ACL2s must take care of. This will happen automatically (except for a couple confirmation dialogs), but the process could take several minutes (5-10).
First, the ACL2 Image for Eclipse will need to fix .cert files for the absolute path of Eclipse on your computer. If you move Eclipse, this step will automatically be repeated. Be patient and let it finish this one-time bookkeeping task, it might take around 5 minutes.
Second, the ACL2s "system books", our visible and invisible extensions to ACL2, need to be certified and compiled by ACL2. This step could be required again if you change your ACL2 version or when you update ACL2s to a new version.
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
form to ACL2. Actually, it will only submit syntactically valid
commands to ACL2, so if one tries to trick it by hitting Enter
(* 21, the editor just goes to the next
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 successor (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
(successor 1 2)--an error because the arity of the successor
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.
Switch back to the .lisp editor where you will discover the
(defun successor (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 successor ...) and
(defun fib ...)
(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
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.
fib definition: the previous one had parameters to
< comparson swapped. ACL2 admits this one:
Now clicking "advance todo" should result in the definition flashing green while it is in the todo region and turning gray after being accepted. (current end of tutorial)
; Computes the nth fibonacci number (defun fib (n) (if (and (integerp n) (< 2 n)) (+ (fib (- n 1)) (fib (- n 2))) 1))
Getting your workspace laid out in a convenient way is important to using ACL2s efficiently. Here are some pointers:
Some ACL2s options are available for setup under Window | Preferences... | ACL2s, but these are easy to find and should be self-documenting. Here I'll point out ACL2s settings burried (necessarily) elsewhere and other Eclipse-wide settings that affect ACL2s:
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.
Lisp files developed in our tool are configured to be in one of several modes, choosable from the menu ACL2 | Set ACL2 session mode. Modes cannot be changed while ACL2 is running, so selection must be made while no associated session is running.
The current mode is displayed in the content description line of the lisp editor, just below the file name tab. The mode is also displayed as part of the startup output of a session, as below:
======================================================================== Executing /home/peterd/acl2s.exe Starting ACL2 in mode "Recursion and Induction"
These modes are intended for those learning ACL2. They all modify ACL2 to print results in a way that is itself "evalable":
ACL2 >VALUE (cons 'a (cons 'b nil)) (LIST 'A 'B) ACL2 >VALUE (cons 1 (cons 2 3)) (CONS 1 (CONS 2 3)) ACL2 >
Here are the introductory modes:
Bare Bones is a mode that is used to teach the semantics of ACL2 using a minimal subset of built-in functions. The mode introduces ACL2 as a programming language with contracts (a "typed" ACL2) to the students, using a "minimal" subset of primitive functions. For example, in the case of the Booleans, all that is built-in are the constants t and nil and the functions if and equal. Everything else is built on top of that.
This mode is designed around exploring ACL2 as a programming language of untyped, total functions. The only caveat is that definitions in "Programming" mode are not checked for termination. Consequently, logically invalid, non-terminating definitions are possible, but this freedom should be familiar to programmers. "Programming" mode also removes some restrictions and warnings about "silly" definitions, and any attempts at proof fail.
|Recursion & Induction|
This mode is intended to be the next step for students comfortable with
ACL2 programming and writing proofs by hand. The primary feature of this
mode is that it only performs induction with explicit hints. Its
Here's an example script for Recursion & Induction mode:
Here's the general form of
where things in [ ] are optional, etc. etc.
R&I mode also includes CCG termination analysis and, for cases in which
that fails, is configured to use lexicographic ordering for termination
proofs. It also supports specifying data-definitions and random-testing (to show
counterexamples and witnesses to proof conjectures in proof output).
Random testing is enabled by default. The following commands turns it off:
This mode is like the R&I mode (above) except that the prover is allowed
to perform one level of induction automatically.
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.)
This mode is full-featured. It is like the Intermediate mode, but with no restrictions on the theorem prover.
This is the recommended mode for a standard ACL2s user.
In this mode, ACL2 is almost indistinguishable from what you would get from executing it directly. This mode is recommended for those developing definitions and theorems to be used by ACL2 outside of ACL2s.
Admissibility in this mode, however, does not *guarantee* admissibility in ACL2 proper (and vice-versa). For more details, see How/what ACL2 functionality is modified for ACLs. Also see book development for certification with ACL2 proper inside of ACL2s/Eclipse.
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.
Each input form submitted to ACL2 from the plugin is placed into one of the following categories based on its purpose and potential effect. Basically, if you use RAW or ACTION input, we cannot guarantee that the plugin will behave in a consistent way with respect to UNDOing, etc., but the rest should behave as expected. We present them in decreasing order of commonness or importance to the user:
|EVENT||These correspond to ACL2 embedded event forms, which are those forms that can appear in books. Calls to defun, defmacro, and defthm are examples of embedded event forms and EVENTs.|
Such forms are simple computations which return a value when (and if) they terminate. No VALUE form can alter ACL2's state and, therefore, never affects undoing or redoing.
A precise definition is that if ACL2 permits (cons <form> nil), then <form> is a VALUE.
|QUERY||These are calls to some built-in ACL2 functions that report information about the current state but are known not to modify state. Examples include (pe 'append) and (pbt 0).|
(internal initiation only)
|Various UI actions which have to do with "undoing" or "moving the line up" can initiate the execution of an UNDO in the session. An ordinary user need not concern him/herself with how this works (How undo and redo are implemented), but should keep in mind that UNDOing an ACTION or RAW form may not have the desired effect.|
(internal initiation only)
This is the counterpart of UNDO. It is used when resubmitting something with the same abstract syntax and in the same environment as something that was previously undone.
REDO enables one to (for example) edit comments above the line, by retreating the line far enough to edit what one wants to change, and then moving the "todo" line back to where it was. If only comments were changed, the session will accept the forms as REDOs, which happen almost instantaneously.
If the input is a parseable ACL2 object but is an ill-formed expression according to the current history, we call it "BAD" input. Examples of violations that would cause input to be staticly ill-formed are:
|COMMAND||There are many forms that are illegal in books but we are able to undo the effect of. If we recognize a form as such, we call it a COMMAND-- except for special cases IN-PACKAGE and BEGIN-BOOK. The best example of a command is ":set-guard-checking :none".|
|This is the "catch-all" categorization for forms that may have effects that we don't know how to properly undo or might even break or hang the ACL2 session. Users who use STOBJs or other STATE beyond the logical WORLD will need to use ACTIONs heavily, but these are advanced uses of ACL2.|
|IN-PACKAGE||This COMMAND gets its own category because of its role in book development. See also :DOC in-package.|
|BEGIN-BOOK||This COMMAND gets its own category because of its role in book development with our plugin. This form is not part of ACL2 proper (yet!).|
|EVENT/VALUE||These are a special type of embedded event form (value-triples) that have no logical consequence--except that they could halt progress by generating a hard lisp error.|
(potentially very dangerous!)
|Most users of ACL2 are familiar with breaking into "raw lisp" by typing ":q" at the top-level prompt. This is not supported in our plugin, but "raw mode" is supported. Most forms submitted under this mode are classified as RAW because they have no well-defined meaning from the ACL2 view of things. With raw mode, the user can easily break many things, and it's only supported for the benefit of experts.|
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+/
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.
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.|
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".
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.
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.
|"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.
DISABLED TEMPORARILY 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.
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 ";;;".
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.
The "ACL2s," "Intermediate," and "Recursion & Induction" session modes include improved termination analysis for ACL2 based on research by Pete Manolios and Daron Vroon. The analysis is based on "context calling graphs," so we refer to it as CCG termination analysis for short.
Beginners can think of CCG termination analysis of as a black-box analysis. We say "black-box" because beginning users need not concern themselves with the details of how CCG analysis works. Of course, any termination analysis is necessarily incomplete and eventually users may come across terminating functions that CCG analysis cannot prove terminating. When that happens, CCG analysis will construct a function that is as simple as possible, includes a subset of the looping behavior of the submitted function, and which CCG analysis cannot prove terminating. This function, along with several suggestions of how to help CCG analysis prove termination, will be presented to the user.
CCG is configured by calling set-termination-method with a single parameter, which must be one of these:
Regardless of this or other settings, ACL2's built-in method will be used if an explicit measure is specified.
For advanced debugging purposes, :set-ccg-verbose t causes the analysis to show what it is doing. This generates lots of output, however.
Finally, "Compatible" mode does not include CCG, and "Programming" mode does not need CCG. CCG is independent of the rest of ACL2s in the sense that it is implemented as an ACL2 book in the acl2s-modes plugin.
Our CCG termination analysis is highly customizable and includes many features not mentioned here. For detailed documentation please refer to :doc ccg from inside a session.
The Data-Definition framework provides a convenient way of specifying data-definitions. It supports records and enumeration, list, union, product, and custom types. The user specifies data-definitions using the macro defdata.
For detailed documentation please refer to :doc data-definitions from inside an ACL2s session or its web version.
Counterexample generation framework seamlessly integrates (random) testing and the full power of the theorem prover (ACL2) to provide an automatic bug-finding capability that often finds counterexamples to false conjectures. This feature is especially effective when used in conjunction with the data definition framework. The counterexamples allow users to quickly fix specification errors and to learn the valuable skill of designing correct specifications. This feature is enabled by default and requires no special syntax so that users get the benefit of automated testing without any effort on their part. The data definition framework supports the counterexample generation framework in an important way . For example, we guarantee that random testing will automatically generate examples that satisfy any hypotheses restricting the (defdata) type of a variable. The ACL2 2011 workshop paper Integrating Testing and Interactive Theorem Proving goes into the details of this feature, but is a very easy read. The reader is encouraged to go through it.
All modes except "Compatible" and "Programming" have testing enabled by default. This feature is independent of the rest of ACL2s in the sense that it is implemented as an ACL2 book in the acl2s-modes plugin.
For documentation on usage and settings please refer to :doc testing from inside a session or its web version. See in particular :doc test?.
The counterexample generation and data definition framework was implemented by Harsh Raju Chamarthi, Peter Dillinger, Matt Kaufmann and Pete Manolios.
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:
Usually the only things that would go before the
(begin-book t :ttags :all)
begin-bookform are package definitions (defpkg), but these aren't worth learning about until you know you need them.
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
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.
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
simplest explanation for the preamble/portcullis is that it is where
should go, because
these are not allowed inside books (because Common Lisps vary in their
ability to compile files that define packages).
begin-book form itself takes the syntax of ACL2's
begin-book doesn't take the "book-name" or "k" parameters. In
fact, here are the parameter and guard specifications for ACL2s's
(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
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
") 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
") form are
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.
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.
One of the goals of ACL2s is to maintain a high degree of compatibility with existing ACL2 development patterns/infrastructure while hiding some of the nasty details from ACL2s-only users. Compatibility of ACL2s book development with existing patterns/infrastructure utilizes the fact that the text in the ACL2s .lisp editor is not exactly what is saved on disk. In particular, when book code is present, the preamble and the begin-book form are saved in a specially-formatted comment. Thus, when ACL2 reads the .lisp file, the first (uncommented) thing it sees is the in-package.
Our "preamble" roughly corresponds to what ACL2 users would put in a .acl2 file. We have a java subroutine/program that can extract the specially-formatted preamble+begin-book from a .lisp file and put it into a .acl2 file with the begin-book call translated to a corresponding certify-book call. This subroutine is used to generate a .acl2 file when the ACL2s users asks to "Certify as book" but the functionality can also be accessed as a stand-alone program. The class is acl2s.lib.certify.MaybeExtractPreamble in acl2s-lib (acl2s-lib.jar in the plugin directory). This program plays nice with old codebases in that it will not overwrite an existing .acl2 file unless there is an ACL2s preamble in the corresponding .lisp file.
Right now, however, there's no automatic way to import an existing book AND
its "preamble" into an ACL2s-ready .lisp file. You can, however, open the
.lisp file with ACL2s, which from the ACL2s perspective has no book code
yet, insert the preamble and
begin-book form at the top, and
ACL2s offers a "beautified" version of ACL2's tracing capability, which is inspired by Common Lisp tracing capabilities. Perhaps the capability is most easily demonstrated with an example:
(defun app (x y) (if (endp x) y (cons (car x) (app (cdr x) y)))) (defun rev (x) (if (endp x) nil (app (rev (cdr x)) (cons (car x) nil)))) (trace* app) (rev '(1 2))
The last input produces the following output:
ACL2 >VALUE (rev '(1 2))
1> (APP NIL '(2)) <1 (APP NIL '(2)) = '(2) 1> (APP '(2) '(1)) 2> (APP NIL '(1)) <2 (APP NIL '(1)) = '(1) <1 (APP '(2) '(1)) = '(2 1)
The output outlined in yellow is the tracing output. This indicates that
during the execution of
(rev '(1 2)),
first called with parameters
nil and the list
Note that arguments are quoted as needed so that one could copy and paste
the call that is displayed, as in
(APP NIL '(2)). The second
and third line of tracing output indicate that the same call returned the list
(2). Like parameters, the return value
is quoted, so that what is displayed is a theorem, in this case that
(APP NIL '(2)) equals
The next time
app is called in the execution of
(rev '(1 2)) is, as the output indicates, as
(APP '(2) '(1)). The next line,
2> (APP NIL '(1))" indicates that
called recursively. The "2" means the recursive depth is two. We then
see that that call (level 2) returns
(1) and the outer call
app (level 1) returns
(2 1) outlined with purple is the usual printed
output of evaluating
(rev '(1 2)). This comes from the
"PRINT" part of "READ-EVAL-PRINT (LOOP)".
One can trace multiple functions simultaneously with
(trace* fn1 fn2
) or with
multiple calls to
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
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:
which means exactly what it says.
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:
||This registers the value of v as the initial "configuration". How this corresponds to what is shown on screen is determined by the next setting.|
This registers the named function f as the translation from
"configurations" to "presentations". After each update to the
graphics "configuration", this function will be called with
[first argument] that configuration and [second argument] an
empty presentation. The return value is treated as the graphics
presentation to show. This is built using API presentation
modification routines described in the next list.
This event overwrites any previous setting for the configuration presenter. Initially, this is the identity function, which means the graphics "configuration" is treated as the "presentation".
||This registers the named function f as a "timer handler". Once started, our system invokes this function every delay-ms milliseconds with the current "configuration" and uses the return value as the updated "configuration". As the name implies, you can register multiple timers with their own (or the same) handler.|
|(add-key-handler f)||This registers the named function f as a "key handler". When a character is typed into the graphics window, we invoke each registered key handler with [first argument] the ACL2/Lisp character that was typed and [second argument] the current "configuration". We use the return value as the updated "configuration". Note that keys that do not correspond to Lisp characters, such as arrow keys, are not currently supported.|
|(add-click-handler f)||This registers the named function f as a "click handler". When the user clicks in the graphics window, we invoke each registered key handler with [first argument] the number of the button clicked (1=left 2=middle 3=right), [second argument] the X position of the click (a rational proportion, 0=left-most 1=right-most), [third argument] the Y position of the click (a rational proportion, 0=top-most 1=bottom-most), and [fourth argument] the current "configuration". The return value is used as the updated "configuration".|
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:
||This returns a modified version of presentation in which the status bar text is set to the string str.|
|This returns a modified version of presentation in which a line has been drawn from (x1,y1) to (x2,y2) in the given color.|
|This returns a modified version of presentation in which the outline of an oval extending right from x with width w and down from y with height h is drawn in the given color.|
|This returns a modified version of presentation in which the outline of an oval centered at (x, y) with width w and height h is drawn in the given color.|
|This returns a modified version of presentation in which the oval extending right from x with width w and down from y with height h is filled with the given color.|
|This returns a modified version of presentation in which the oval centered at (x, y) with width w and height h is filled with the given color.|
|This returns a modified version of presentation in which the outline of a rectangle extending right from x with width w and down from y with height h is drawn in the given color.|
|This returns a modified version of presentation in which the rectangle extending right from x with width w and down from y with height h is filled with the given color.|
|This returns a modified version of presentation in which the image file given by the string path has been placed with its top-left corner at position (x, y) and scaled to extend by width w and height h.|
|This returns a modified version of presentation in which the image file given by the string path has been centered at position x, y. Conceptually, you should think of this function as placing an image of negligible/unimportant size at a point in space. Unlike put-image, this will draw the image at its native size, but to stay "conceptual", we recommend "put-image" if resulting image size is large or important.|
|This returns a modified version of presentation in which the text of the string text has been drawn with height h in color color, centered at position x, y. If h is zero, a default readable size is used.|
|This returns a modified version of presentation in which the text of the string text has been drawn with height h in color color with its top-left corener at position x, y. If h is zero, a default readable size is used.|
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.
|Q:||Is my OS 32 bit or 64 bit?|
|A:||For Linux, if you see "x86_64" or "amd64" in the output of shell command `uname -a`, you have a 64bit OS, otherwise a 32 bit one. For other operating systems, please visit their respective FAQ pages: Windows and MacOSX.|
|Q:||What is Eclipse?|
|A:||Eclipse is a highly modularized, extensible, free development environment for a variety of programming languages. See www.eclipse.org. Eclipse is written in Java and has an especially well developed development environment for Java.|
|Q:||Where do I learn about all this Eclipse lingo?|
|A:||See the "Basic Tutorial" section of the Workbench User Guide.|
|Q:||How do I run Eclipse--with the right options?|
|A:||See the "Running Eclipse" section of the 3.5 Release Notes. To view details about how a currently-running Eclipse was invoked, go to Help | About Eclipse SDK and click "Configuration Details".|
|Q:||How do I tell what Java version Eclipse is running under, and if its 64bit?|
|A:||Inside Eclipse, go to Help | About Eclipse SDK and click "Installation Details". Under "Configuration" tab are the "eclipse.commands" property and the "java.runtime.*" properties, you will find the relevant information. You can also find out under "-arch" your machine architecture, for example, "X86_64" will indicate that you are running a 64bit Eclipse. "java.vm.name" will tell you if the Java being used is a 64bit JVM.|
|Q:||Where is Eclipse documentation?|
|Q:||Can I do a multi-user install of Eclipse?|
It is tricky to support a multi-user install of Eclipse. The key seems to be not running Eclipse at all in a way that would allow modification of the files in that eclipse installation. Once it has written some configuration stuff to the installation directory, it bombs if you can't write to that directory anymore.
This is why I discourage this unless you're truly in an environment that's going to have many Eclipse users. As awkward as it sounds, just install Eclipse such that the user who will be running it can modify all of its files, and life will be easier.
|Q:||What is ACL2?|
|A:||ACL2 is a programming language, logic, and theorem prover/checker based on Common Lisp. See the ACL2 home page for more information.|
|Q:||What is CAR?|
|A:||CAR is an abbreviation we sometimes use to refer to this
Computer-Aided Reasoning: An Approach.See J Moore's page about the book for description and affordable ordering information.
|Q:||What is an ACL2 book?|
|A:||Basically, an ACL2 book is a bunch of ACL2 definitions (functions, theorems, proof rules, etc.) that can be easily imported into other ACL2 work. See :DOC books and our guide to book development in ACL2s for more information.|
|Q:||Can I use the ACL2 image downloaded by Eclipse outside of Eclipse?|
|A:||Absolutely! From the ACL2 perspective, it has everything you would have building ACL2 yourself. Simply run eclipse/plugins/acl2_image.something/run_acl2.|
|Q:||Do I already have Java? What version?|
|A:||The simple answer is to type "java -version" at your operating system's command prompt/console/shell. You might still have Java if the command is rejected. See How do I run Eclipse--with the right options? and Is there a difference between Java SDK 1.5.0 and 5.0? for more info.|
|Q:||Do I need the Java SDK or is the JRE fine?|
|A:||The SDK is nice to have if you plan on ever doing any Java development. Otherwise, the (smaller) JRE is fine.|
|Q:||Is there a difference between Java SDK 1.5.0 and 5.0?|
|A:||No. "5.0" is the version number adjusted for marketing-hype. See "Version 1.5.0 or 5.0?" on Sun's site. Similarily, there is no difference between Java version "6.0" and JDK/JRE 1.6.0.|
|Q:||What is Netbeans?|
|A:||Netbeans is a Java development environment that feels much like Eclipse but is more Java-specific. You do not need it.|
|Q:||Can I use a version of Java older than "5.0" and newer than "6.0"?|
|A:||Eclipse will run on Java runtimes as old as 1.4.2, but our plugin uses 1.5 language constructs and APIs. You are likely to encounter problems if you use a Java runtime that is older than "5.0" or newer than "6.0".|
|Q:||Why won't ACL2s let me do <blah> in a session?|
In order for the plugin to follow what's going on in ACL2, we must impose some small limitations. One, for example, is that it will not let you break into raw Lisp. For those interested in this dangerous, low-level form of interaction, however, raw mode is supported (because it uses ACL2's reader).
Another subtle limitation is that--aside from wormholes--ld will only let you read from *standard-oi* at ld level 1. The reason has to do with undoing and also ld-error-action. Another example is that good-bye and other exit commands are disabled to the user, to encourage use of the user interface operation "Stop session" instead.
For more details, see How/what ACL2 functionality is modified for ACL2s.
|Q:||Can I use ACL2s extensions to ACL2 in an Emacs development environment?|
Yes! Assuming you have ACL2s installed as an eclipse plugin in /Users/sarah/tools/eclipse, here are instructions on how to run an ACL2s mode session in Emacs. Name the above directory my_eclipse.
|Q:||I am having trouble installing/running ACL2s, what should I do?|
ACL2s is open-source software, and comes with ABSOLUTELY NO WARRANTY. Copyright 2008 Georgia Tech Research Corporation and Northeastern University.
All parts are available under the Eclipse Public License v1.0 with a GPL exception, and the "acl2s-hooks" and "acl2s-modes" parts are dual-licensed under the GNU General Public License v2.0 as well.
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.
Email Harsh Raju Chamarthi() and Pete Manolios() with bugs and other questions.
Up to version 0.97, the main developer has been Peter Dillinger, advised by Pete Manolios. Since then, ACL2s is maintained by Harsh Raju Chamarthi, advised by Pete Manolios. CCG termination analysis is by Pete Manolios and Daron Vroon.