File: Readme.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (163 lines) | stat: -rw-r--r-- 7,915 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
<HEAD><TITLE>The ACL2 Books Directory</TITLE></HEAD>

<BODY TEXT="#000000">
<BODY BGCOLOR="#FFFFFF">

<H1>The ACL2 Books Directory</H1>
<P>
The word ``book'' has two senses to the ACL2 user.  One is the normal one: a
sequence of printed paper pages bound together between covers.  There are
such books about ACL2.  Click <A
HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html">here</A>
for more information.
<P>
The other sense is a technical one: an ACL2 ``book'' is a file of
definitions, theorems and other commands used to extend ACL2's reasoning
abilities.  Commands add ``rules'' to ACL2's data base.  When a book is
``certified,'' ACL2 checks that all the commands in it can be successfully
processed.  A book can be ``included'' into an ACL2 session to extend the
data base.  This is the standard way users exchange useful sets of theorems.
See the online documentation topic BOOKS for details.
<P>
The standard distribution of ACL2 comes with many books.  They are stored on
this directory.  This is a guide to the available books.  We include
instructions on how to certify the books in this directory at the <A
HREF="#CertificationInstructions">end</A> of this note.
<P>
Some of the links below are to files.  Others are to directories.  When
you visit a directory, look at its <CODE>README</CODE> file.  Most of
these books were written by ACL2 users other than the authors of ACL2.
Authorship is acknowledged in the individual files.
<UL>
<LI><A HREF="Makefile">Makefile</A>: a Unix file for recertifying all the 
books in this directory.
<LI><A HREF="Makefile-generic">Makefile-generic</A>: a Unix file exploited by
<CODE>Makefile</CODE>.
<LI><A HREF="Makefile-subdirs">Makefile-subdirs</A>: a Unix file exploited by
<CODE>Makefile</CODE>.
<LI><A HREF="README">README</A>: a text file directing you to this file.
<LI><A HREF="README.html">README.html</A>: this file.
<LI><A HREF="arithmetic">arithmetic</A>: books about arithmetic.  The book
<CODE>books/arithmetic/top-with-meta.lisp</CODE> is the most commonly used
ACL2 arithmetic book.  However, arithmetic is an extraordinarily rich
topic and none of our books do it justice.  If you develop an improved
arithmetic book, let us know!
<LI><A HREF="arithmetic-2">arithmetic-2</A>: books about arithmetic contributed by Robert Krug (older)
<LI><A HREF="arithmetic-3">arithmetic-3</A>: books about arithmetic contributed by Robert Krug (newer)
<LI><A HREF="bdd">bdd</A>: books that exercise ACL2's BDD mechanism.

<LI><A HREF="certify-numbers.lisp">certify-numbers.lisp</A>:  used to
certify the <CODE>cowles</CODE> and <CODE>arithmetic</CODE> books when
not using make, e.g., for example, when using a Macintosh.

<LI><A HREF="concurrent-programs">concurrent-programs</A>: contributions by
Sandip Ray (see </code>Readme.lsp</code> files in subdirectories)
<LI><A HREF="cowles">cowles</A>: support for arithmetic books
<LI><A HREF="data-structures">data-structures</A>: books for common data
structures, with utilities; see also subdirectory <a
href="data-structures/memories">memories</a>
<LI><A HREF="defexec">defexec</A>: fast execution with mbe and defexec
<LI><A HREF="finite-set-theory">finite-set-theory</A>: finite sets in ACL2
<LI><A HREF="ihs">ihs</A>: ``integer hardware specification'', integer
arithmetic appropriate for hardware modeling
<LI><A HREF="make-event">make-event</A>: illustrations of
<code>make-event</code>, which implements the idea of macros that can take state
<LI><A HREF="meta">meta</A>: metafunctions for arithmetic
<LI><A HREF="misc">misc</A>:  a grab-bag of useful books and
utilities
<LI><A HREF="nonstd">nonstd</A>:  books in support of reasoning about the real
numbers in ACL2 using non-standard analysis.  If you want this directory, you will need to
<a
href="nonstd.tar.gz">download
the gzipped tar file</a> to your <code>acl2-sources/books/</code> directory,
and then gunzip and extract it there.
<LI><A HREF="ordinals">ordinals</A>: books about ordinals
<LI><A HREF="powerlists">powerlists</A>: a data-structure suited to the analysis of recursive,
data-parallel algorithms.
<LI><A HREF="proofstyles">proofstyles</A>: logical equivalence of two proof styles for
verifying programs using operational semantics, namely
inductive invariants and clock functions
<LI><A HREF="rtl">rtl</A>: floating-point arithmetic support, used for example
in proofs about AMD rtl
<LI><A HREF="symbolic">symbolic</A>: generic proofs of partial and total
correctness of sequential programs based on assertional reasoning
<LI><A HREF="textbook">textbook</A>: solutions to the exercises
in <I><A
HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html">Computer-Aided
Reasoning: An Approach</A></I>
<LI><A HREF="unicode">unicode</A>: help for reading input from files
<LI><A HREF="workshops">workshops</A>:  Books in support of ACL2 workshops, as
listed just below.  If you want this directory, you will need to
<a
href="http://www.cs.utexas.edu/users/moore/acl2/v3-0/distrib/acl2-sources/books/workshops.tar.gz">download
the gzipped tar file</a> to your <code>acl2-sources/books/</code> directory,
and then gunzip and extract it there.
<UL>
<LI><A HREF="workshops/1999">workshops/1999</A>:  books from ACL2 Workshop 1999, supporting and described
in <I><A
HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-books/acs/index.html">Computer-Aided
Reasoning: ACL2 Case Studies</A></I>, including full scripts for each case
study and answers to all the exercises
<LI><A HREF="workshops/2000">workshops/2000</A>:  books and papers from ACL2 Workshop 2000
<LI><A HREF="workshops/2002">workshops/2002</A>:  books and papers from ACL2 Workshop 2002
<LI><A HREF="workshops/2003">workshops/2003</A>:  books and papers from ACL2 Workshop 2003
<LI><A HREF="workshops/2004">workshops/2004</A>:  books and papers from ACL2 Workshop 2004
<LI><A HREF="workshops/2006">workshops/2006</A>:  books and papers from ACL2 Workshop 2006
</UL>
</UL>
<P>
If you seek a book you suspect someone might have created but which is not
here, join the ACL2 mailing list and ask the community.
<P>
If you develop a book you think will be useful to the community, please submit
it following the <a
href="http://www.cs.utexas.edu/users/moore/acl2/books/index.html">instructions
for contributing books to ACL2</a>.
<P>

<H2><A NAME="CertificationInstructions">Certification Instructions</A></H2>

Many of these books are easily imagined to be of general value to ACL2 users,
while others are more specialized.  Although this subdivision is a bit
arbitrary, we refer to books in the former category as "basic" books.  By
default, the <CODE>make</CODE> process certifies only the basic books.  It may
take several hours to certify all the books, but only a couple of hours to
certify only the "basic" books.

<P>

All of the instructions below assume that you are standing in subdirectory
<CODE>books</CODE> of the ACL2 distribution.

<P>
<B>EXAMPLES:</B>
<P>

To certify the <B>basic</B> books, assuming that `<CODE>acl2</CODE>' invokes
ACL2, execute:
<PRE>
make
</PRE>
To certify <B>all</B> books, assuming that `<CODE>acl2</CODE>' invokes ACL2,
execute the following after you download <code><a
href="http://www.cs.utexas.edu/users/moore/acl2/v3-0/distrib/acl2-sources/books/workshops.tar.gz">
workshops.tar.gz</a></code> to your <code>acl2-sources/books/</code> directory,
and then gunzip and extract it there.
<PRE>
make all-plus
</PRE>
To certify the <B>basic</B> books, assuming that `<CODE>my_acl2</CODE>' invokes
ACL2, execute:
<PRE>
make ACL2=my_acl2
</PRE>
To certify <B>all</B> books using an image with absolute pathname
<CODE>/u/bin/allegro_acl2</CODE> on a Sparc, execute the following.  Note that
pathnames of images must be absolute pathnames (except that commands observable
via the Unix path are OK).
<PRE>
make all-plus ACL2=/u/bin/allegro_acl2
</PRE>
<BR><BR><BR><BR><BR><BR>
</BODY>
</HTML>