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.
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
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 Recursion& Induction 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.
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.
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
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.
A readable and example-oriented description of
defdata framework appears in the ACL2 2014 Workshop
paper Data Definitions in
ACL2 Sedan. Furthur documentation is also available by
:doc defdata inside an ACL2s session.
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
cgen from inside a session. See in particular
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) (in-package "ACL2")
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))
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
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)