|
|
|---|
|
|
|
|---|
ACL2 Sedan User Guide
This guide showcases the important parts of the ACL2 Sedan user experience. We assume you already have a running ACL2s session; if not check out the ACL2s-tutorial. The ACL2 tutorial (ACL2::ACL2-tutorial) is a fine place to learn about the ACL2 language, logic and theorem proving system. For in-depth documentation about ACL2 itself refer to ACL2::ACL2.
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 "ACL2s"
| Mode | Description |
|---|---|
| ACL2s |
This mode is full-featured and places no restrictions on the theorem prover. This is the recommended mode for a standard ACL2s user. |
| Compatible |
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 the How/what ACL2 functionality is modified for ACLs section of the ACL2s-implementation-notes. |
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 the How modes are implemented section of the ACL2s-implementation-notes.
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
| UI Action | Icon | Description |
|---|---|---|
| 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
| |
| "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 ACL2::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 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. | ||
| 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 |
|
This will use cert.pl to certify the current book so that it can be quickly included from another file. See ACL2::certificate for more information. Shortcut: 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," session mode includes 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 ccg.
Data definitions are an essential part of crafting programs and
modeling systems. Whereas most programming languages provide rich
mechanisms for defining datatypes, ACL2 only really provides a
limited collection of built-in types and
This state of affairs presented us with a challenge when we started teaching undergraduates how to model, specify and reason about computation, because even freshmen students have a type-centric view of the world.
We introduced the defdata framework in ACL2s
in order to provide a convenient, intuitive way to specify data
definitions. A version of
See defdata for defdata's documentation. In particular, a readable and example-oriented description of defdata framework appears in the ACL2 2014 Workshop paper linked at the bottom of that topic.
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" have testing enabled by default.