ACL2s 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 go to Get Started. The ACL2 tutorial is a fine place to learn about the ACL2 language, logic and theorem proving system. For in-depth documentation about the ACL2 itself refer to the manual.

Cheat Sheet

A cheat sheet is available with a summary of key bindings and command types: HTML or PDF.

Customization

Workspace Layout

Getting your workspace laid out in a convenient way is important to using ACL2s efficiently. Here are some pointers:

  • Editor split: At this time, source code and sessions are in editors--different editors. To see both at one time, you need to split up your editor area. (Each workbench window has one rectangular "editor area" in which all the open editors are tabbed and/or tiled.) Click the title area of an editor you would like to split away from the others and drag it to any side of the others. As you drag, a gray outline of the proposed layout is shown. Observe that you can also drag titles back together, and you can relocate views around the editor area analogously.
  • Open, close, many, one: Through the "Window" menu, you can open more than one workbench window, each of which has one rectangular editor area and can have only one of any view open. Also through the "Window" menu, you can open another editor to the same file; all editors for the same file keep their content in sync with each other. Also through the "Window" menu, you can reopen any views that may have accidentally been closed.
  • Fast views: If you don't want to dedicate long-term real estate to views such as the Project Explorer, Outline, Proof Tree, and Console, you can minimize them to make them available quickly. If you click the icon for the minimized view--rather than the restore icon--it pops up as a "fast view" which is minimized again after you click outside it.

Preferences

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:

  • Editor font: Open the preferences dialog and go to General | Appearance | Colors and Fonts. Under "Basic," the "Text Font" is that used by the ACL2s editors. Click "Change..." to change it.
  • Editor colors: To make the editor text darker in general, go in the preferences dialog to General | Appearance and select the "Current theme" "High Contrast (ACL2s)". This is good for use on a projector, for example. To manipulate the colors in detail, go to Colors and Fonts and open the ACL2s group. Note: You will have to close and re-open editors for these color changes to take effect.

Session

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.

Session Modes for ACL2 development

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"

Introductory modes

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:

Mode Description
Bare Bones
(introductory)

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.

Programming
(introductory)

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.

A note for experienced ACL2 users: Primarily, this mode uses program mode and guard-checking :none.

Recursion & Induction
(introductory)

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 non-standard theorem event also disables any generated rules by default (like defthmd). Induction and theory extension are disabled *not* to discourage use, but to force the user to give some guidance to ACL2, with hints. Automatic generalization and irrelevance elimination are also disabled for proofs in this mode--to encourage writing appropriate lemmas.

Here's an example script for Recursion & Induction mode:


(defun app (x y)
  (if (consp x)
    (cons (car x) (app (cdr x) y))
    y))

(defun rev (x)
  (if (consp x)
    (app (rev (cdr x)) (cons (car x) nil))
    nil))

(theorem rev-app-single 
  (equal (rev (app l (list v)))
         (cons v (rev l)))
  :hints (("Goal" :induct (rev l))))

(theorem rev-rev
  (implies (true-listp x)
    (equal (rev (rev x)) x))
  :hints (("Goal" :induct (rev x)
                  :in-theory (enable rev-app-single))))

Here's the general form of theorem:


(theorem <name>
  <formula>
  [:hints (("Goal" [:induct <term>]
                   [:in-theory (enable <name1>
		                       ...
				       <nameK>)]))])
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 (:doc defdata) and automated Counterexample Generation (:doc cgen).

Standard/Industrial modes

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

Mode Description
ACL2s

This mode is full-featured. It is like the Recursion& Induction mode, but with 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 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.

Input Command Classifications

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:

Class Description
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.
VALUE

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.

Advanced Note: some VALUE forms have transient side effects, but they have no logical consequence (e.g. CW and WORMHOLE).

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).
UNDO
(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.
REDO
(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.

BAD

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:

  • wrong number of parameters to a function/macro
  • use of an undefined function/macro
  • first element of an invocation list is not a symbol or lambda expression
  • mismatch between expected and actual "mv shape"

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".
ACTION
(potentially dangerous!)
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.
RAW
(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.

Descriptions of UI Actions with key bindings

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 Command+Shift. For example, Interrupt is still Ctrl+Break (if you have a Break key), but switching editors is Command+Shift+o.

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 ( 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.
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.

CCG termination analysis

Background

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.

Settings

CCG is configured by calling set-termination-method with a single parameter, which must be one of these:

  • :ccg - CCG analysis only (no measure-based proof attempt)
  • :measure - no CCG analysis (measure-based proofs only)

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.

More Documentation

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.

Data Definitions

Background

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 cons.

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 defdata has appeared in ACL2s since at least August 2009 (in version 0.9.7), and we have been extending and improving it since then.

Documentation

A readable and example-oriented description of the defdata framework appears in the ACL2 2014 Workshop paper Data Definitions in ACL2 Sedan. Furthur documentation is also available by submitting :doc defdata inside an ACL2s session.

Counterexample Generation

Background

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.

Documentation

For documentation on usage and settings please refer to :doc cgen from inside a session. See in particular :doc test?.

ACL2 Book Development

Introduction

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

Usually the only things that would go before the begin-book form are package definitions (defpkg), but these aren't worth learning about until you know you need them.

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.

Implementation and compatibility with ACL2

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 save it.

Tracing function execution

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:

Tracing 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)
(2 1) ACL2 >

The output outlined in yellow is the tracing output. This indicates that during the execution of (rev '(1 2)), app was first called with parameters nil and the list (2). 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 '(2).

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 app was called recursively. The "2" means the recursive depth is two. We then see that that call (level 2) returns (1) and the outer call of app (level 1) returns (2 1).

The final (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)".

More Tracing Details

One can trace multiple functions simultaneously with (trace* fn1 fn2) or with multiple calls to trace*.

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)
which means exactly what it says.