Developers-guide-background
Some Implementation Background
When background is found to be lacking in this topic, it might be acquired
by querying the acl2-devel mailing list. In that case it would probably be
good to extend this chapter by adding the background that had been
lacking.
Source files
ACL2 has many source files. The definitive list of
source files is the value of the constant *acl2-files* found in source
file acl2.lisp. This list is consistent with the list associated
with the variable "sources" in GNUmakefile, with the exception of
generated file doc.lisp (which is discussed later in this Guide; see
developers-guide-build). Perhaps surprisingly, acl2.lisp is not
in either list! That's due to a traditional ambiguity in the use of the term
``source file'' for ACL2. The files in the list *acl2-files* are all
written in ACL2 (with the exception of relatively little raw Lisp code, as
discussed in the section on ``Readtime Conditionals'' below). A few other
files support the infrastructure surrounding the ACL2 system. These may be
found in the definition of variable "sources_extra" in
GNUmakefile; acl2.lisp is one of those files.
We may talk of ``earlier'' and ``later'' source files. Here we reference
their order in *acl2-files*, which is essentially the order in which they
are processed via ld when building an ACL2 executable. Note however
that files *-raw.lisp are not intended for processing by ld
during the build, but rather, are simply loaded directly into Common Lisp,
perhaps after being compiled.
The names of the source files are somewhat suggestive
of their contents. However, over time this correspondence has weakened, in
large part because of the requirement that a function must be defined before
it is used. For example, function find-rules-of-rune was moved in
git commit 5647bd402e from defthm.lisp to an earlier file,
rewrite.lisp, in support of a new function,
backchain-limit-enforcers, which in turn was introduced in support of an
existing function in rewrite.lisp
(tilde-@-failure-reason-phrase1) that reports failures in the break-rewrite loop.
Source file axioms.lisp
The source file axioms.lisp is the place for defining most logic-mode functions that form the core of the ACL2 programming language, and
also for some basic axioms and theorems about these functions as well as the
built-in primitives like car and unary-/ that have no explicit
definition. The theorems are stated as defthm events, while
the axioms are stated as defaxiom events. The axioms are intended to
completely specify the ground-zero theory. However, it is less clear
when to include a defthm event into axioms.lisp, rather than simply
putting that theorem into a book.
The section on ``Build-time proofs'' in the topic, developers-guide-build, has a discussion of executing ``make proofs'' to
admit events, including those in axioms.lisp. Some defthm events
are critical for this purpose, for example, for proving termination or
verifying guards. Others are simply very basic: so useful that it seems a
pity to relegate them to books, rather than to include them in the build.
Moreover, the specific form of some axioms and theorems is chosen to be useful
for reasoning; for example, here is a rather critical :elim rule
in addition to being an important axiom.
(defaxiom car-cdr-elim
(implies (consp x)
(equal (cons (car x) (cdr x)) x))
:rule-classes :elim)
It is good to be careful when considering the addition of defthm
events to axioms.lisp. If defthm events are to be added in order to
support termination or guard verification when doing ``make
proofs'', you can consider making the events local so that they
don't make it into the build. But you might leave some non-local if they seem
to be extremely useful, for example:
(defthm fold-consts-in-+
(implies (and (syntaxp (quotep x))
(syntaxp (quotep y)))
(equal (+ x (+ y z))
(+ (+ x y) z))))
There is potential controversy here. One could argue that such theorems
belong in books, not in the source code. This can be argued either way:
putting in the source code is good because ACL2 can do obviously-expected
things at start-up, and is bad because it's inelegant and narrows user
choices. These days, we tend to add defthm events to axioms.lisp
only sparingly, without removing any. One could argue endlessly about this
controversy, but there are probably many more fruitful ways to spend limited
development resources!
The ACL2 state and logical world
The ACL2 state is represented in the implementation as
a symbol, which is the value of constant *the-live-state*.
Sometimes we call this the ``live state'', to
distinguish it from its logical value, which is a list of fields. See state for relevant background.
It may seem impossible for a fixed symbol to represent
a changeable state. But let us consider for example what happens when we
update a state global variable (see f-put-global) in raw Lisp.
In the following example (where we elide code for the case of wormholes) there
are two cases. The interesting case is the first one, in which the state is
the live state. We see below that there is an associated global (special)
variable, in a package obtained by prefixing the string "ACL2_GLOBAL_"
to the front of the symbol's package-name: ACL2_GLOBAL_ACL2::XYZ. The code below updates that
global.
? (pprint (macroexpand '(f-put-global 'xyz (+ 3 4) state)))
(LET ((#:G128770 (+ 3 4)) (#:G128771 STATE))
(COND ((LIVE-STATE-P #:G128771)
(COND (*WORMHOLEP* ...))
(LET ()
(DECLARE (SPECIAL ACL2_GLOBAL_ACL2::XYZ))
(SETQ ACL2_GLOBAL_ACL2::XYZ #:G128770)
#:G128771))
(T (PUT-GLOBAL 'XYZ #:G128770 #:G128771))))
?
To read a state global from the live state, we simply read its associated
global variable.
? (pprint (macroexpand '(f-get-global 'xyz state)))
(LET ((#:G128772 STATE))
(DECLARE (SPECIAL ACL2_GLOBAL_ACL2::XYZ))
(COND ((LIVE-STATE-P #:G128772) ACL2_GLOBAL_ACL2::XYZ)
(T (GET-GLOBAL 'XYZ #:G128772))))
?
Note that the ACL2 state can be viewed as a special, built-in case of a
stobj. Indeed, we may also speak of ``live
stobjs'', to distinguish them from their logical, list-based
representations, and a stobj, st, is represented in the implementation as
*the-live-st*. These ``live'' constants are illustrated below.
ACL2 !>(defstobj st fld)
Summary
Form: ( DEFSTOBJ ST ...)
Rules: NIL
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ST
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
? *the-live-st*
#<SIMPLE-VECTOR 1>
? *the-live-state*
ACL2_INVISIBLE::|The Live State Itself|
?
One of the logical fields of the state is the global-table, which is
an association list mapping symbols, namely state global variables (sometimes
called ``state globals''), to values. See also programming-with-state.
One particular state global, the symbol current-acl2-world, is mapped to
the current logical world, often just called ``the world''. Here is
the logical definition of the function (w state) that returns this world;
note that it calls the macro f-get-global, which, as explained above,
generates a read of a Lisp global.
Function: w
(defun w (state)
(declare (xargs :guard (state-p state)))
(f-get-global 'current-acl2-world
state))
The current logical world, in turn, is a list of triples of the form
(name property . value). The function getprop may be used to
access the value for a given name and property. For example, suppose that we
submit the event (defun f (x) (cons x x)). This actually pushes several
triples on the world, one of which is the so-called unnormalized body
of f, accessible via getprop as follows.
ACL2 !>(getprop 'f 'unnormalized-body nil 'current-acl2-world (w state))
(CONS X X)
ACL2 !>
It is extremely common for the last three arguments of getprop to be
as displayed above, so the macro getpropc is often used instead.
ACL2 !>(getpropc 'f 'unnormalized-body)
(CONS X X)
ACL2 !>
Also see walkabout for a tool that can be extremely helpful for
examining the world.
Terms, translate, and untranslate
For relevant background on the notion of term in ACL2, see term. The ACL2 source code traffics in what that documentation topic calls
``translated terms''. In any discussion at the implementation level,
including this guide and source code comments, we just
say ``term'' to refer to a translated term. The source code traffics almost
entirely in terms, though user input is in the form of what the
documentation for term calls an ``untranslated term''. The ACL2 functions translate and untranslate map
from untranslated terms to terms and vice-versa, respectively. These
both take the world as a formal parameter, because they need to consult
the world: for example, translate consults the world to determine, for a
call (f t1 t2 ...), whether f is a function symbol, a macro, or (in
the error case) neither of these; and untranslate consults the world for
more subtle reasons such as converting a call of return-last to
something more readable.
The definition of the function untranslate1, which is the workhorse
for untranslate, is instructive for how ACL2 processes terms. It has the following form.
(defun untranslate1 (term iff-flg untrans-tbl preprocess-fn wrld)
(let ((term (if preprocess-fn ... term)))
(cond ((variablep term) term)
((fquotep term)
(cond (<basically, not a cons or symbol>
(cadr term))
(t term)))
((flambda-applicationp term)
<Turn the lambda application into a LET.>)
((eq (ffn-symb term) 'if)
<Many special cases, e.g.,
(if x1 'nil 't) negates untranslation of x1>
...))))
This sort of structure is typical: handle the variable case, then the case
of (quote _), then the case of a lambda application, and finally one or
more cases for the call of a function symbol. If you peruse the source code
you will see handy term utilities. Please strive for consistency by studying
some of those (e.g., search the source code for "variablep" or
"quotep"). For example, don't build a new term with (cons fn
args); use cons-term or fcons-term instead of
cons.
We defer to a later chapter (see developers-guide-utilities) a
discussion of macros that are commonly used in the ACL2 implementation, with
one exception: defrec. We cover that macro here because it is so
crucial for understanding some topics covered below.
See defrec for user-level documentation on defrec. This macro
provides a cheap way to lay out a record structure using cons (since the
Common Lisp macro defstruct is not supported by ACL2, which does not have
structures). Sometimes it is worthwhile to think a bit about expected reads
and writes of the fields, to help lay them out efficiently. For example,
consider the definition of an important record for the prover,
prove-spec-var (with comments omitted here):
(defrec prove-spec-var
((rewrite-constant induction-hyp-terms . induction-concl-terms)
(tag-tree hint-settings . tau-completion-alist)
(pool . gag-state)
user-supplied-term displayed-goal orig-hints . otf-flg)
t)
Notice above and in the following generated definition that the field,
orig-hints, is buried deep inside this structure.
ACL2 !>:trans (access prove-spec-var some-pspv :orig-hints)
((LAMBDA (ORIG-HINTS)
(CAR (CDR (CDR (CDR (CDR (CDR ORIG-HINTS)))))))
SOME-PSPV)
=> *
ACL2 !>
An Emacs tags-search for ``:orig-hints'' shows that this field is
used only during initialization of the prover (excluding ACL2(p)), not within
the waterfall, let alone the rewriter; of course, this is hardly surprising.
So it seems fine to push this field way back in the record definition. On the
other hand, the rewrite-constant field is more rapidly accessible as the
caar, which is reasonable since it is accessed quite frequently within
the waterfall.
One can often learn about a record by reading its field names, seeing how
they are used in the source code (with a tags-search), or reading code
comments inserted into the defrec form that defines it or near that
definition. You could try learning more now about the prove-spec-var and
rewrite-constant, which are quite important in the prover code.
Commands and events
DEMO: USING WALKABOUT TO EXPLORE THE WORLD
Among the triples in the world are so-called command
landmarks and event landmarks, which are put there at the
conclusion of a command or event, respectively. What are
commands and events, and what's the difference between them?
Let's start with commands. The (user-level) documentation for commands says that they are ``forms you type at the top-level, but the word
`command' usually refers to a top-level form whose evaluation produces a new
logical world.'' At the implementation level, a command is a form read
and evaluated by ld. If you follow the source code starting with
ld, you'll see that it reads and evaluates forms with the function
ld-loop, which in turn calls ld-read-eval-print on each form. That
function, in turn, calls ld-read-command to read the next form and then
calls a version of trans-eval, trans-eval-default-warning, to
evaluate it. (See also the section on ``Evaluators'' in the chapter, developers-guide-utilities; also see the chapter, developers-guide-evaluation.) When there is no error, the function
maybe-add-command-landmark is called. It checks whether the world has
changed, and if so it pushes a new triple on the new world, a so-called
command landmark, provided the new world doesn't already have a command
landmark as the topmost triple. Let's use the walkabout utility to
see what a command landmark might look like.
ACL2 !>(with-output :off :all (defun foo (x) x)) ; avoid noise just below
FOO
ACL2 !>(walkabout (w state) state)
Commands:
0, 1, 2, ..., nx, bk, pp, (pp n), (pp lev len), =, (= symb), and q.
((COMMAND-LANDMARK GLOBAL-VALUE 7357 ...)
(EVENT-LANDMARK GLOBAL-VALUE 8625 ...)
(FOO ABSOLUTE-EVENT-NUMBER . 8625)
...)
:1
(COMMAND-LANDMARK GLOBAL-VALUE 7357 ...)
:pp
(COMMAND-LANDMARK GLOBAL-VALUE 7357
(:LOGIC WITH-OUTPUT :OFF
:ALL (DEFUN FOO (X) X))
"/share/projects/")
:
The triple just above is, as with every triple in the world, of the form
(sym prop . val). We thus interpret the triple above to say that the
current command-landmark has a global-value property of the form
(7357 (:logic . <form>) <dir> . nil). The definition of the record
structure command-tuple (which is easy to find with the Emacs command,
meta-.) uses the defrec macro, discussed above. For now we
explain the fields in our example as follows; see the Essay on Command Tuples
and ensuing definitions for more information.
- the absolute command number is 7357.
- The defun-mode is :logic.
- The form is (with-output :off :all (defun foo (x) x)).
- The cbd is "/share/projects/".
- The last-make-event-expansion field is nil.
We turn now from commands to events.
There are primitive events that modify the world such as a call of defun, defthm, and table. See events and especially
see embedded-event-form, which explain that events may go in calls of
encapsulate and progn, which themselves are also (compound)
events, and events may also go in books. Several other utilities are
events in the sense that they are allowed in compound events and books, but
they are really just wrappers of sorts for actual events. Here is a list of event macros, taken from a comment in the
definition of function chk-embedded-event-form, which is the recognizer
for (embeddable) events.
- local
- skip-proofs
- with-cbd
- with-guard-checking-event
- with-output
- with-prover-step-limit
- with-prover-time-limit
- make-event
Of course, make-event is a complex sort of wrapper, in that it
serves to generate an event, its expansion.
Continuing the demo of walkabout started above (when explaining
commands), we see an event-landmark immediately below the
command-landmark.
:nx
(EVENT-LANDMARK GLOBAL-VALUE 8625 ...)
:pp
(EVENT-LANDMARK GLOBAL-VALUE 8625 ((DEFUN) FOO . :IDEAL)
DEFUN FOO (X)
X)
:
Let's take this opportunity to explore how to make sense of ACL2 data
structures. If we use the Emacs command meta-x tags-apropos on
"event-landmark" we find the function add-event-landmark; then
using the meta-. command on add-event-landmark, we find its
definition and we see a call of make-event-tuple. That function has
comments that explain the fields; perhaps more illuminating, accessors for
event-tuple fields are defined immediately below the definition of
make-event-tuple. We can apply these accessors to deconstruct the value,
val, in the triple above, (event-landmark global-value . val).
Regarding the local-p field of an event-tuple: if an event E is
evaluated in a local context, then the corresponding event-tuple is
(local . x) where x is the event-tuple for E.
ACL2 !>(let ((val (cddr '(EVENT-LANDMARK GLOBAL-VALUE 8625 ((DEFUN) FOO . :IDEAL)
DEFUN FOO (X)
X))))
(list :local-p (access-event-tuple-local-p val)
:number (access-event-tuple-number val)
:depth (access-event-tuple-depth val)
:type (access-event-tuple-type val)
:skipp (access-event-tuple-skipped-proofs-p val)
:namex (access-event-tuple-namex val)
:form (access-event-tuple-form val)
:symcls (access-event-tuple-symbol-class val)))
(:LOCAL-P NIL
:NUMBER 8625
:DEPTH 0
:TYPE DEFUN
:SKIPP NIL
:NAMEX FOO
:FORM (DEFUN FOO (X) X)
:SYMCLS :IDEAL)
ACL2 !>
We conclude our discussion of commands and events with a few
observations.
- Commands can be undone, using ubt and related utilities. Events
are not undone (except when they are also commands); only commands are
undone.
- :Puff is applied to command-descriptors, so naturally
it expands commands, not events.
- Only events can go into books and calls of progn or encapsulate, not arbitrary commands.
Exploring the source code with an example: prover flow
An important skill for ACL2 code development and maintenance is the ability
to explore the source code to gain necessary background. This is really an
art, developed with experience. There has been a lot of attention to
documenting the source code — as of mid-March 2018, about 30% of the
source file lines (that is, from *.lisp files not including the generated
documentation file doc.lisp) consisted entirely of a comment line, and of
course other lines contained comments as well. Here we show the raw data.
ginger:/projects/acl2/acl2/saved% wc -l *.lisp | grep total
373606 total
ginger:/projects/acl2/acl2/saved% wc -l doc.lisp
121865 doc.lisp
ginger:/projects/acl2/acl2/saved% grep '^[ ]*;' *.lisp | wc -l
76588
ginger:/projects/acl2/acl2/saved% grep '^[ ]*;' doc.lisp | wc -l
1545
ginger:/projects/acl2/acl2/saved%
Unfortunately, 30+% comments is not sufficient! In a perfect world, more
ACL2 functions would have extensive documentation, with clear pointers to
necessary background including high-level algorithm discussion. This Guide is
intended to help to fill the gap, but can only do so partially. The missing
additional ingredient to absorbing source code — as practiced for years
by ACL2 developers as of this writing in March 2018 — is the ability to
explore the sources. Ideally this is a skill that can be learned by
practicing.
As a simple example, we show how to explore the source code to get a sense
of the flow of the theorem prover. This is very far from getting a sense of
the ACL2 system in general, which supports much more than the prover (think of
book certification, make-event, invariant-risk, and on and
on).
Let's start with thm:
DEMO: EXPLORE HOW THM ULTIMATELY CALLS THE REWRITER. But unlike the
discussion below, I'll go bottom-up. This may give us some idea of how the
prover is structured. One result may be found in the documentation section,
developers-guide-background-extra.
Macro: thm
(defmacro thm (&whole event-form
term &key instructions hints otf-flg)
(cons
'with-output
(cons
':off
(cons
'summary
(cons
':stack
(cons
':push
(cons
(cons
'make-event
(cons
(cons
'er-progn
(cons
(cons
'with-output
(cons
':stack
(cons
':pop
(cons
(cons
'thm-fn
(cons
(cons 'quote (cons term 'nil))
(cons
'state
(cons
(cons 'quote (cons instructions 'nil))
(cons
(cons 'quote (cons hints 'nil))
(cons (cons 'quote (cons otf-flg 'nil))
(cons (cons 'quote (cons event-form 'nil))
'nil)))))))
'nil))))
'((value '(value-triple :invisible)))))
'(:expansion? (value-triple :invisible)
:on-behalf-of :quiet!
:save-event-data t)))
'nil)))))))
Thm-fn calls prove, which calls prove-loop and so on, as is
easy to discover using the Emacs command, meta-. . We thus work our way
to the waterfall.
thm-fn
prove
prove-loop
prove-loop0
prove-loop1
prove-loop2
waterfall
At this point things get more complicated. Waterfall calls
waterfall1-lst@par, which should be thought of as waterfall1-lst, as
discussed below where we talk about ACL2(p). We see that waterfall1-lst
is part of a rather complex mutual-recursion. But a key function
called in that mutual-recursion is waterfall-step, which is shown as
calls of waterfall-step@par. Knowing about waterfall-step is one of
those pieces of background knowledge to learn that makes it easier over time
to peruse the ACL2 sources. In the body of that function is a call of
waterfall-step1, which provides a clue about the main flow of the prover:
the key subroutine of a function foo often has the name foo1, or
perhaps foo-1, foo-aux, or foo-rec, or more generally,
foo<something>. The function waterfall-step1 has a nice structure
showing how it leads to calls of individual waterfall processing functions, in
particular, the simplifier via the function simplify-clause. We can
explore the definition of simplify-clause in a similar way, finding
simplify-clause1, which has these key subroutines.
remove-trivial-equivalences
forward-chain-top
setup-simplify-clause-pot-lst
process-equational-polys
rewrite-clause
The flow suggests that the first four of these functions are called to set
things up for the call to rewrite-clause. That function can be similarly
explored, in particular to find key subroutines that include the
following.
built-in-clausep1
rewrite-clause-type-alist
rewrite-atm
clausify
rewrite-clause-lst
The function rewrite-atm does yet a bit more processing, using
known-whether-nil, before calling rewrite. Feel free to explore
rewrite, but beware, as it's quite complicated! Indeed, the usual
activity of an ACL2 maintainer is not to explore for the sake of general
background, as we have been doing above, but rather to explore for the sake of
more specific understanding before making desired modifications or
additions.
Build-time checks
There are several checks done near the end of an ACL2 build, as performed
by (subfunctions of) the function, check-acl2-initialization. There is
not much that we need to say here, because if one of those tests fails, then
the error message should make it clear how to proceed.
Raw Lisp and readtime conditionals
ACL2 is built on top of Common Lisp. Some knowledge of that programming
language is occasionally necessary. The definitive reference is the Common
Lisp Hyperspec, which can be found easily with a web search.
Every ACL2 source file is either loaded directly into Common Lisp as part
of the ACL2 build, or is first compiled into a compiled file before loading
that compiled file. (Files acl2.lisp and acl2-init.lisp are never
subjected to file compilation, as noted in a comment near the top of each
file.) Thus, ACL2 macros including defun, defthm, table, defconst, local, and encapsulate must be suitable for Common Lisp evaluation. This is
arranged differently for different macros, as illustrated by the following
examples.
DEMO: RATHER THAN GO THROUGH WHAT'S BELOW, I'LL JUST EXPLORE DEFUN,
DEFTHM, LOCAL, and QUIT, AND USE THEM TO EXPLAIN *features* AND SPECIFICALLY
acl2-loop-only.
First consider defun. We have only the following definition of
defun in the ACL2 source code.
#+acl2-loop-only
(defmacro defun (&whole event-form &rest def)
; Warning: See the Important Boot-Strapping Invariants before modifying!
(list 'defun-fn
(list 'quote def)
'state
(list 'quote event-form)
#+:non-standard-analysis ; std-p
nil))
The notation ``#+acl2-loop-only'' is called a readtime
conditional. In this case, it says that the definition of defun
immediately following that notion is ignored by the reader unless the symbol
:acl2-loop-only is a member of the Lisp variable, *features*.
Normally, and during loading and (when it occurs) compilation of ACL2 source
files, :acl2-loop-only is not a member of *features*, so the
definition above is ignored — as is appropriate, since defun is
already defined in Common Lisp. The function initialize-acl2 pushes the
symbol :acl2-loop-only onto *features* before beginning to ld
the ACL2 source files; thus, as ACL2 processes its own source files, the
definition above is read (not ignored) and evaluated; you can evaluate :pe
defun in the top-level loop to see the definition above.
Next consider defthm. This time there are two definitions. One is
much like the definition above of defun:
#+acl2-loop-only
(defmacro defthm (&whole event-form
name term
&key (rule-classes '(:REWRITE))
instructions
hints
otf-flg)
; Warning: See the Important Boot-Strapping Invariants before modifying!
(list 'defthm-fn
(list 'quote name)
(list 'quote term)
'state
(list 'quote rule-classes)
(list 'quote instructions)
(list 'quote hints)
(list 'quote otf-flg)
(list 'quote event-form)
#+:non-standard-analysis ; std-p
nil))
The other definition occurs in a raw Lisp context, as follows.
#-acl2-loop-only
(progn
...
(defmacro defthm (&rest args)
(declare (ignore args))
nil)
...)
Thus, the Common Lisp loader or compiler will see this definition of
defthm, but the ld of the ACL2 source files will not. In summary:
defthm is defined in terms of defthm-fn in the ACL2 loop, but it is
defined simply to return nil in raw Lisp.
Interesting cases are local and encapsulate. These have
rather complex definitions in the ACL2 loop, but let's see
what happens during macroexpansion in raw Lisp.
? (pprint
(macroexpand '(encapsulate (((f *) => *))
(local (defun f (x) x))
(defun g (x) (f x))
(local (defthm consp-g
(implies (consp x) (consp (g x))))))))
(PROGN (DEFUN F (X1) (THROW-OR-ATTACH F (X1)))
(LOCAL (DEFUN F (X) X))
(DEFUN G (X) (F X))
(LOCAL (DEFTHM CONSP-G (IMPLIES (CONSP X) (CONSP (G X))))))
? (macroexpand '(LOCAL (DEFUN F (X) X)))
NIL
T
? (macroexpand '(LOCAL (DEFTHM CONSP-G (IMPLIES (CONSP X) (CONSP (G X))))))
NIL
T
?
Evidently, encapsulate defines its signature functions simply to cause
errors, actually like this:
ACL2 Error in TOP-LEVEL: ACL2 cannot ev the call of non-executable
function F on argument list:
(3)
It is also apparent that calls of local in raw Lisp expand simply to
nil.
To understand such behavior, let's look at the definitions of local
and encapsulate, eliding comments and some code for brevity. The elided
code in the first definition of encapsulate below, which is for raw Lisp,
defines the functions in the signature to cause errors when called.
#-acl2-loop-only
(progn
...
(defmacro encapsulate (signatures &rest lst)
`(progn ,@(mapcar <...elided code...> signatures)
,@lst))
...
(defmacro local (x)
(declare (ignore x))
nil)
...)
#+acl2-loop-only
(defmacro local (x)
(list 'if
'(equal (ld-skip-proofsp state) 'include-book)
'(mv nil nil state)
(list 'if
'(equal (ld-skip-proofsp state) 'initialize-acl2)
'(mv nil nil state)
(list 'state-global-let*
'((in-local-flg t))
(list 'when-logic "LOCAL" x)))))
#+acl2-loop-only
(defmacro encapsulate (&whole event-form signatures &rest cmd-lst)
(list 'encapsulate-fn
(list 'quote signatures)
(list 'quote cmd-lst)
'state
(list 'quote event-form)))
We see that in raw Lisp, encapsulate generates a suitable progn
and local is a no-op.
You may find it instructive to look at the #-acl2-loop-only and
#+acl2-loop-only definitions of other event macros.
Implementation-specific code
As of this writing, six Common Lisp implementations support ACL2: Allegro
Common Lisp (ACL), Clozure CL (CCL), CMU Common Lisp (CMUCL), GNU Common
Lisp (GCL), LispWorks, and Steel Bank Common Lisp (SBCL). (Note: As of
Sept. 2018 there remains a problem with CMUCL that was reported several months
ago, which the implementor has indicated that he intends to try to fix.) Some
ACL2 raw-Lisp code is implementation-specific, that is, depends on which of
these six Common Lisp implementations is the host lisp. See for example the
definitions of exit-lisp and getenv$-raw. Here is an elided version
of the definition of exit-lisp. Notice the readtime conditional used for
each of the six supported Lisp implementations and also some that are no
longer supported, like CLISP. (Note: Normally we see ``gcl'' for GCL but
sometimes, as below, we see the somewhat archaic (but still acceptable)
``akcl''.)
(defun exit-lisp (&optional (status '0 status-p))
<<code elided>>
#+clisp
(if status-p (user::exit status) (user::exit))
#+lispworks ; Version 4.2.0; older versions have used bye
(if status-p (lispworks:quit :status status) (lispworks:quit))
#+akcl
(if status-p (si::bye status) (si::bye))
#+lucid
(lisp::exit) ; don't know how to handle status, but don't support lucid
#+ccl
(if status-p (ccl::quit status) (ccl::quit))
#+cmu
<<code elided>>
#+allegro
(user::exit status :no-unwind t)
#+(and mcl (not ccl))
(cl-user::quit) ; mcl support is deprecated, so we don't worry about status
#+sbcl
<<code elided>>
(progn status-p status))
ACL2 ``Experimental Versions''
Two dissertations have produced modifications of ACL2.
- ACL2(r), courtesy of Ruben Gamboa, extends the rational number data type
to include irrational numbers. It is built on a foundation of non-standard
analysis, which is a logical theory (really, more than one) that makes sense
of Leibniz's notion of ``infinitesimal'' in place of foundations based on
limits.
- ACL2(p), courtesy of David Rager, supports both parallel evaluation in
general and parallelization of the ACL2 waterfall.
Code that is to be read only when building ACL2(r) has the readtime
conditional #+:non-standard-analysis, where the leading colon is actually
optional but is typically used by convention. Code that is to be read only
when building ACL2(p) has the readtime conditional #+acl2-par. As of
this writing, the maintenance of these systems has typically been performed by
Kaufmann and Moore when reasonably feasible, but sometimes with assistance
from Gamboa and Rager, especially when there is a major change.
Note that ACL2(r) changes the logic — for example, the formula
(not (equal (* x x) 2)) is a theorem of ACL2 but is disprovable in
ACL2(r) — but ACL2(p) does not change the logic. Another difference is
that ACL2(r) was intended, as a design decision, to be sound; by contrast,
ACL2(p) was intended to be sound in practice but with a small risk that an
unsound result could be obtained.
There is a somewhat elaborate mechanism for incorporating ACL2(p) source
code into the ACL2 sources. One part involves the use of feature
:acl2-par: that is, the use of #+acl2-par to prefix code to be read
only when building ACL2(p) and of #-acl2-par to prefix code to be read
only when building ACL2. But there is also support for function and macro
names with suffix "@PAR". When considering ACL2 and not ACL2(p), these
should be read simply by removing that suffix: for example, defun@par is
to be read as defun, er@par is to be read as er, and so on.
For information about how to make sense of the "@PAR" suffix when
reading the sources as ACL2(p) sources, see the Essay on Parallelism,
Parallelism Warts, Parallelism Blemishes, Parallelism No-fixes, Parallelism
Hazards, and #+ACL2-PAR notes. Several definitions near the end of
axioms.lisp, below mention of that essay, implement the handling of
"@PAR" suffixes.
At one time, the addition of hash-cons, function memoization, and
fast-alists (see hons-and-memoization) was considered experimental, and
resulted in a system called ACL2(h) with a corresponding readtime conditional
of #+hons. That system, which was originally built on top of ACL2 by Bob
Boyer and Warren Hunt and was updated by Jared Davis and Sol Swords, with
contributions by Matt Kaufmann and J Moore, was ultimately updated and
incorporated into ACL2 by Kaufmann and Moore after an extensive code review.
Since Kaufmann and Moore now stand behind the resulting system and are
maintaining it, and with assent from its contributors, what was formerly
ACL2(h) is now just ACL2.
NEXT SECTION: developers-guide-extending-knowledge
Subtopics
- Developers-guide-background-extra
- Some Implementation Background Extra Information
