← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/doc/relnotes.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/doc/relnotes.lisp
45
45
;
46
46
;  - Book release notes are typically very disorganized.  This shouldn't be
47
47
;    considered a bug until we are very close to a release.
48
 
;
49
 
;  - The following URL is very useful for updating the comments here:
50
 
;       http://code.google.com/p/acl2-books/source/list
 
48
 
 
49
(defxdoc note-7-0-books
 
50
  :parents (note-7-0)
 
51
  :short "Release notes for the ACL2 Community Books for ACL2 7.0 (January
 
52
2015)"
 
53
 
 
54
; Current through 2014-12-29, modulo a couple of bozos
 
55
 
 
56
  :long "<p>The following is a brief summary of changes made to the @(see
 
57
community-books) between the releases of ACL2 6.5 and 7.0.</p>
 
58
 
 
59
<p>The <a
 
60
href='https://github.com/acl2/acl2/wiki/Release-version-numbers'>acl2-books
 
61
Wiki page on Release Version Numbers</a> gives the Git/SVN revision numbers
 
62
corresponding to releases.  See also @(see note-7-0) for the changes made to
 
63
ACL2 itself.  For additional details, you may also see the raw <a
 
64
href='https://github.com/acl2/acl2/commits/master'>commit log</a>.</p>
 
65
 
 
66
<h2>Organizational, Build System, and Name Changes</h2>
 
67
 
 
68
 
 
69
<h3>Source Code Moved</h3>
 
70
 
 
71
<p>The ACL2 Community Books and ACL2 System source code repositories have been
 
72
merged into one repository and are now available at</p>
 
73
 
 
74
<box><p><a
 
75
href=\"https://github.com/acl2/acl2\">https://github.com/acl2/acl2</a></p></box>
 
76
 
 
77
<p>See the @('Readme.md') file found there for more details.  See also the
 
78
@(see git-quick-start) guide if you are interested in contributing.</p>
 
79
 
 
80
 
 
81
 
 
82
<h3>Deleted Stubs</h3>
 
83
 
 
84
<p>When we move a book, we often add a <b>stub</b> book in its previous
 
85
location to help you transition your @(see include-book) commands.  The @(see
 
86
cert.pl) build system prints warnings when a stub book is being included.</p>
 
87
 
 
88
<p>Stub books have a lifespan of one release.  The following books were stubs
 
89
in ACL2 6.5, so we've deleted them.</p>
 
90
 
 
91
@({
 
92
     Previous Location                New Location
 
93
   ---------------------------------------------------------------
 
94
     str/*                            std/strings/*
 
95
 
 
96
     xdoc/portcullis                  std/portcullis
 
97
     std/osets/portcullis             std/portcullis
 
98
     std/bitsets/portcullis           std/portcullis
 
99
     std/strings/portcullis           std/portcullis
 
100
 
 
101
     coi/osets/instance               std/osets/instance
 
102
     coi/osets/computed-hints         std/osets/computed-hints
 
103
 
 
104
     centaur/bitops/sign-extend       centaur/bitops/fast-logext
 
105
 
 
106
   ---------------------------------------------------------------
 
107
})
 
108
 
 
109
 
 
110
<h3>Build System Changes</h3>
 
111
 
 
112
<p>The @('arithmetic-2') library is no longer built by default when running an
 
113
ordinary @('make').  All books that previously depended on @('arithmetic-2')
 
114
have been transitioned to use @('arithmetic-3') instead.  If your own work
 
115
depends on @('arithmetic-2'), you can still build these books, e.g., by running
 
116
@('make arithmetic-2') in the @('books') directory.</p>
 
117
 
 
118
<p>Many minor tweaks and cleanups have been made to the build system
 
119
itself.</p>
 
120
 
 
121
<ul>
 
122
 
 
123
<li>@('cert.pl') now has better support for @(see
 
124
provisional-certification).</li>
 
125
 
 
126
<li>The @(see cert_param) mechanism, which is used by @(see cert.pl) to
 
127
indicate that books have special requirements, is now documented.</li>
 
128
 
 
129
<li>New @('cert_param') directives have been added to avoid certifying certain
 
130
books on incompatible Lisps.</li>
 
131
 
 
132
<li>@(see cert.pl) now better avoids overflowing the maximum number of
 
133
arguments to shell commands on some platforms when certifying large numbers of
 
134
books.</li>
 
135
 
 
136
<li>The new @(':ignore-certs') feature of @(see include-book) is now used in
 
137
special two-pass books like @('std/strings/defs-program.lisp'), and should help
 
138
to make building these books more reliable.</li>
 
139
 
 
140
<li>Hundreds of old Makefiles from the @(see books-certification-classic) era
 
141
have been eliminated.  Some obsolete GCL-specific directives have also been
 
142
eliminated.</li>
 
143
 
 
144
<li>Installing @(see quicklisp) now works from behind a proxy.  See <i>Using a
 
145
Proxy</i> in @(see books-certification) for details.</li>
 
146
 
 
147
<li>The implementation of ``@('make everything')'' has been cleaned up.  In
 
148
particular, it no longer sets @('USE_QUICKLISP=1') since this is not
 
149
appropriate for some Lisps.</li>
 
150
 
 
151
<li>The @('make clean') command now does a better job of cleaning up generated
 
152
files.</li>
 
153
 
 
154
</ul>
 
155
 
 
156
<p>Numerous books have been patched up for better portability across Lisps and
 
157
integration with ACL2(p).  For instance: In many cases, previous calls of @(see
 
158
without-waterfall-parallelism) are no longer necessary, largely due to
 
159
thread-safe memoization; several @(see oslib) functions have been extended to
 
160
work on additional Lisps; many books with raw Lisp code now use @(see
 
161
include-raw) for more portable compilation behavior across Lisps.</p>
 
162
 
 
163
<p>Various other utilities have been made more reliable.</p>
 
164
 
 
165
<ul>
 
166
 
 
167
<li>For Emacs @('TAGS') users, the @('etags.sh') script has been improved to
 
168
permit whitespace before definitions.</li>
 
169
 
 
170
<li>For ACL2 packaging mechanisms, the @('fix-cert') utility has been improved
 
171
and now includes scripts for moving ACL2 distributions.</li>
 
172
 
 
173
</ul>
 
174
 
 
175
<p>Supporting scripts for the <a href='http://jenkins-ci.org/'>Jenkins</a>
 
176
continuous integration server can now be found in the @('build/jenkins')
 
177
directory.  These scripts have received significant attention and can now
 
178
support multi-configuration builds for checking ACL2 books compatibility with
 
179
many host Lisps.</p>
 
180
 
 
181
 
 
182
<h3>Name Conflict Resolution</h3>
 
183
 
 
184
<p>Progress has been made toward resolving name clashes in order to be able to
 
185
include more books together.  This work involves renaming certain lemmas and
 
186
may require updates to your books.</p>
 
187
 
 
188
<p>Arithmetic-2</p>
 
189
 
 
190
<ul>
 
191
<li>@('floor-mod-elim') no longer forces its hypothesis.</li>
 
192
</ul>
 
193
 
 
194
<p>Arithmetic-5</p>
 
195
<ul>
 
196
<li>@('floor-=-x/y') now has additional corollaries.</li>
 
197
</ul>
 
198
 
 
199
<p>IHS</p>
 
200
<ul>
 
201
<li>@('floor-mod-elim') no longer forces its hypothesis.</li>
 
202
<li>@('floor-=-x/y') now has additional corollaries.</li>
 
203
<li>@('justify-floor-recursion') has been renamed to @('floor-recursion').</li>
 
204
<li>@('cancel-floor-+') has been renamed to @('cancel-floor-+-basic').</li>
 
205
<li>@('cancel-mod-+') has been renamed to @('cancel-mod-+-basic').</li>
 
206
<li>@('rationalp-mod') no longer requires @('(rationalp x)').</li>
 
207
</ul>
 
208
 
 
209
<p>COI/osets</p>
 
210
 
 
211
<ul>
 
212
 
 
213
<li>Many @('coi/osets') books are now just small wrappers around @('std/osets')
 
214
books.</li>
 
215
 
 
216
<li>COI's @('double-containment') rule has been renamed to
 
217
@('double-containment-expensive').</li>
 
218
 
 
219
</ul>
 
220
 
 
221
 
 
222
<h3>Licensing Changes</h3>
 
223
 
 
224
<p>Robert Krug's @('arithmetic-3') library of is now available under a
 
225
BSD-3-Clause style license instead of the GNU General Public License.</p>
 
226
 
 
227
<p>Several books contributed by David Rager, which were formerly released under
 
228
the GNU General Public License or a BSD-3-Clause style license, are now instead
 
229
released under a (more permissive) MIT/X11-style license.</p>
 
230
 
 
231
<p>Several books contributed by Oracle, which were formerly released under the
 
232
GNU General Public License, are now instead released under an MIT/X11-style
 
233
license.</p>
 
234
 
 
235
<p>The @(see ubdds) library and a few \"miscellaneous\" books have also been
 
236
transitioned from the GNU General Public License to a 3-clause BSD style
 
237
license.</p>
 
238
 
 
239
<p>Several books in the @('coi') library, which previously lacked explicit
 
240
license information, now have explicit MIT/X11-style licenses.</p>
 
241
 
 
242
 
 
243
<h2>New Libraries and Documentation</h2>
 
244
 
 
245
<p>The ACL2+Books manual has a great deal of new and improved content and many
 
246
topics have been reorganized to provide a more coherent hierarchy.  Notably,
 
247
all documentation in the legacy <i>defdoc</i> format has been rewritten into
 
248
the @(see xdoc) format.  Some highlights:</p>
 
249
 
 
250
<ul>
 
251
<li>The @(see ihs) documentation has been considerably updated.</li>
 
252
<li>The @(see defsort) macro is now documented.</li>
 
253
<li>The @(see sneaky) documentation has been considerably expanded.</li>
 
254
<li>Topics like @(see lists), @(see strings), @(see alists), etc., now
 
255
group together some related @(see programming) functions.</li>
 
256
</ul>
 
257
 
 
258
<p>The ACL2 @(see Sidekick) is an experimental and very preliminary graphical
 
259
add-on to ACL2.  It currently features a session viewer, theory linter, a
 
260
horribly primitive interface to the @(see proof-checker), and a slick
 
261
<i>Lookup</i> feature that can show you documentation and other information
 
262
about various symbols.</p>
 
263
 
 
264
<p>The new @('system/toothbrush') directory provides a way to create
 
265
applications with ACL2 that have a much smaller memory footprint than an
 
266
ordinary ACL2 @(see save-exec) image.  See the @('README') file in this
 
267
directory for more information.</p>
 
268
 
 
269
<p>The new @(see depgraph::depgraph) library now contains a few algorithms for
 
270
working with dependency graphs.  It provides @(see depgraph::toposort), a
 
271
topological sort, @(see depgraph::invert), an edge-inversion algorithm, and
 
272
@(see depgraph::transdeps), which can compute the transitive dependencies for a
 
273
set of nodes.  This functionality was formerly part of @(see VL) but has now
 
274
been made more general and extracted.</p>
 
275
 
 
276
<p>The new @('projects/codewalker/') directory contains Codewalker, a utility
 
277
for exploring code in any programming language specified by an ACL2 model to
 
278
discover certain properties of the code.  Demos of Codewalker are also in that
 
279
directory.</p>
 
280
 
 
281
<p>The new directory @('projects/hybrid-systems/') is a
 
282
specification/verification project by Shant Harutuntian using ACL2(r) (see
 
283
@(see real)), in support of his 2007 Ph.D. dissertation, with a few recent
 
284
updates (because of ACL2 changes) made by Cuong Chau.</p>
 
285
 
 
286
<p>There are also several new small tools and books.</p>
 
287
 
 
288
<ul>
 
289
 
 
290
<li>(CCL Only) The new @(see spacewalk) tool can be used to get a report about
 
291
heap memory usage.  It may be useful for identifying unusually large functions
 
292
and constants in your ACL2 session.</li>
 
293
 
 
294
<li>The new @(see simp) tool can be used to ask ACL2 to simplify terms under
 
295
certain hypotheses.</li>
 
296
 
 
297
<li>The new tool @('misc/check-fn-inst') can be used to check the constraints
 
298
to a functional instantiation.</li>
 
299
 
 
300
<li>The new tool, @(see def-saved-obligs), can be used to save proof
 
301
obligations for an event as independent defthms.</li>
 
302
 
 
303
<li>The new tool, @('system/dead-source-code.lisp'), may be useful
 
304
for finding dead code in the ACL2 sources.</li>
 
305
 
 
306
<li>The new books @('system/cantor-pairing-bijective.lisp') and
 
307
@('system/hl-nat-combine-onto.lisp') contain proofs of bijectivity and
 
308
surjectivity (one-one/onto and onto, respectively) of cantor-pairing
 
309
functions.</li>
 
310
 
 
311
</ul>
 
312
 
 
313
<h2>Changes to Major Libraries</h2>
 
314
 
 
315
<h3>XDOC Changes</h3>
 
316
 
 
317
<p>The web-based XDOC viewer has been improved.  It now uses newer versions of
 
318
the JQuery and Typeahead libraries.  Some bugs with the typeahead (jump to) box
 
319
have been fixed and it has been extended to show more results.  The jump-to box
 
320
has been extended with a @('Alt+/') hotkey (or perhaps some other key
 
321
combination like @('Ctrl+/'), depending on your browser).  Middle clicking on
 
322
XDOC links should now properly open them in new tabs and the fonts have been
 
323
updated.  Some ugly quotes are now replaced by ``smart'' replacements.</p>
 
324
 
 
325
<p>Significant work has been done to try to make XDOC content accessible to
 
326
search engines such as Google.  A new PHP script largely replaces previous
 
327
failed efforts to generate \"static\" HTML files, site maps, and so forth.</p>
 
328
 
 
329
<p>XDOC now supports \"resource directories\" for incorporating images, PDF
 
330
files, and other kinds of resources.  See @(see xdoc::add-resource-directory)
 
331
for details.</p>
 
332
 
 
333
<p>XDOC now features @(see xdoc::katex-integration) for writing LaTeX-like
 
334
formulas like @($ \\left( \\sum_{i=0}^{n} \\sqrt{f(i)} \\right) <
 
335
\\frac{n^2}{k} $) within your documentation.  Note that ACL2's new @(see
 
336
fancy-string-reader) can be used to make escaping simpler, and this may be
 
337
especially useful when trying to write LaTeX-like formulas, where the escaping
 
338
of @('\\') characters can be irritating.</p>
 
339
 
 
340
<p>There are also many other minor changes:</p>
 
341
 
 
342
<ul>
 
343
 
 
344
<li>The @(see defpointer) macro has been integrated into XDOC itself.  (It was
 
345
formerly only part of the ACL2 system documentation.)</li>
 
346
 
 
347
<li>@(see defsection) and @(see define) now permit plain strings to be included
 
348
among the list of events.  These strings are incorporated into the resulting
 
349
documentation as running commentary.</li>
 
350
 
 
351
<li>The @(see defxdoc), @(see defsection), and @(see define) macros now all
 
352
evaluate the arguments to @(':short') and @(':long') instead of quoting them.
 
353
This may make it more convenient to write macros that produce documentation
 
354
from boilerplate templates, e.g., you can now directly write things like
 
355
@(':short (cat ...)').</li>
 
356
 
 
357
<li>Tweaked @(see defsection) so that you can give @(':extension (foo)')
 
358
instead of just @(':extension foo.')</li>
 
359
 
 
360
<li>Better error handling on @(see xdoc::xdoc-extend) and @(see
 
361
xdoc::xdoc-prepend).</li>
 
362
 
 
363
</ul>
 
364
 
 
365
 
 
366
 
 
367
<h3>@(see STD) Library Changes</h3>
 
368
 
 
369
 
 
370
<h5>@(see std/basic)</h5>
 
371
 
 
372
<p>Added @(see tuplep) and @(see impossible).</p>
 
373
 
 
374
 
 
375
<h5>@(see std/lists)</h5>
 
376
 
 
377
<p>Cleaned up rules about take in @(see std/lists/take).</p>
 
378
 
 
379
<p>@(see replicate) is now an alias for @(see repeat) and is compatible with
 
380
the definition of @('repeat') in the COI libraries, fixing a longstanding
 
381
incompatibility.</p>
 
382
 
 
383
<p>The @(see all-equalp) function has been added.</p>
 
384
 
 
385
<p>Several lemmas about @(see intersection$), @(see intersectp), and @(see
 
386
set-difference$) have been extracted from @(see vl) and moved into
 
387
@('std/lists').  See for instance @(see std/lists/intersection$),
 
388
@(see std/lists/intersectp), and @(see std/lists/set-difference).</p>
 
389
 
 
390
 
 
391
 
 
392
 
 
393
<h5>@(see std/util)</h5>
 
394
 
 
395
<p>The @(see b*) binders for @(see std::defaggregate)s now also bind the
 
396
variable, fixing a longstanding issue.  Also, the syntax @('((prodname name))')
 
397
is now permitted as an abbreviation for @('((prodname name) name)').  (This is
 
398
often useful when destructuring a function's arguments).</p>
 
399
 
 
400
<p>The @(see b*) binders for @(see std::defaggregate) (and also @(see
 
401
fty::defprod)) are now extensible and can translate bindings like @('x.foo')
 
402
into calls of user-defined functions.  See the description of <i>Extra Binder
 
403
Names</i> in the documentation of @(see std::defaggregate) for details.</p>
 
404
 
 
405
<p>The @(see std::deflist), @(see std::defalist), @(see std::defprojection),
 
406
and @(see std::defmapappend) macros are now \"pluggable\" and can be extended
 
407
with additional theorems; see for instance the new book
 
408
@('std/lists/abstract.lisp').</p>
 
409
 
 
410
<p>The new books @('std/util/deflist-base') and @('std/util/defalist-base')
 
411
offer lighter-weight alternative to @('std/util/deflist') and
 
412
@('std/util/defalist').</p>
 
413
 
 
414
<p>The @(see std::defrule) book now has fewer dependencies.</p>
 
415
 
 
416
<p>Documentation for @(see std::deflist) has been improved.  @('Deflist') now
 
417
uses @(see define) so that you get a signature block in the resulting
 
418
documentation.  The documentation for automatically generated deflist events is
 
419
now put in a more sensible order and split off into a @('foolistp-basics')
 
420
section underneath of @('foolistp'), to reduce the prominence of this
 
421
\"boilerplate\" documentation.  Deflist can now also create documentation even
 
422
in the @('already-definedp') case.</p>
 
423
 
 
424
<p>Fixed an obscure bug with @(see define)'s return-specifiers that could
 
425
affect non-executable functions that involve stobjs.</p>
 
426
 
 
427
<p>The @(see define) macro now interprets @(':inline nil') as \"make this a
 
428
<see topic='@(url defun-notinline)'>$notinline</see> function\" instead of
 
429
\"make this a regular function instead of an <see topic='@(url
 
430
defun-inline)'>inline</see> one.\"</p>
 
431
 
 
432
<p>The @(see define), @(see defines), and also the @(see fty::deffixequiv)
 
433
macros now have improved, more advanced default hints set for inductive proofs
 
434
in return specs and @('deffixequiv(-mutual)') forms.</p>
 
435
 
 
436
 
 
437
<h5>@(see std/strings)</h5>
 
438
 
 
439
<p>Certification time has been improved.</p>
 
440
 
 
441
<p>The @('fast-cat') book (see @(see str::cat)) now uses @(see include-raw) to
 
442
avoid possible issues on various Lisps.</p>
 
443
 
 
444
<h5>@(see std/io)</h5>
 
445
 
 
446
<p>Added @(see read-file-as-string) function.</p>
 
447
 
 
448
<h5>@(see std/alists)</h5>
 
449
 
 
450
<p>There are some new functions: @(see fal-find-any) and @(see
 
451
fal-all-boundp).</p>
 
452
 
 
453
<p>Moved @(see worth-hashing) into @('std/alists') from
 
454
@('misc/hons-help').</p>
 
455
 
 
456
<h5>@(see std/typed-lists)</h5>
 
457
 
 
458
<p>Move @(see cons-listp) and @(see cons-list-listp) out of VL and into
 
459
@('std/typed-lists').</p>
 
460
 
 
461
 
 
462
 
 
463
<h3>Defdata (Data Definition Framework)</h3>
 
464
 
 
465
<p> @('Defdata') has undergone significant improvements.  Automated theorem
 
466
proving support has been increased by a tight integration with @(csee
 
467
Tau-system).  A significant new capability is the support for parametric
 
468
polymorphism via @('sig') rules. There have been many improvements in its
 
469
engineering too.</p>
 
470
 
 
471
<h5>Tau Integration</h5>
 
472
<p>
 
473
Defdata analyzes the predicate definition of every new type and, if
 
474
possible, produces a set of Tau rules that completely characterize
 
475
the type. Defdata thus provides the following guarantee: If Tau is
 
476
complete over the type reasoning theory, then adding a type to the
 
477
current theory via @('defdata') preserves completeness.
 
478
</p>
 
479
 
 
480
<h5>Parametric Polymorphism</h5>
 
481
<p>
 
482
Defdata provides a new macro @('sig') which can be used to define
 
483
signatures of polymorphic functions
 
484
such as <tt>append</tt>, <tt>remove1</tt>, <tt>put-assoc</tt> etc:
 
485
</p>
 
486
@({
 
487
  (sig append ((listof :a) (listof :a)) => (listof :a))
 
488
  (sig remove1-equal (all (listof :a)) => (listof :a))
 
489
  (sig put-assoc-equal (:a :b (alistof :a :b)) => (alistof :a :b))
 
490
})
 
491
 
 
492
<p>
 
493
Defdata automatically instantiates these generic theorems 
 
494
(type signatures) for previously defined types and as new types are defined
 
495
after the @('sig') forms. Defdata, thus implements parametric polymorphism, by
 
496
providing the following invariants:</p>
 
497
 
 
498
<ul>
 
499
<li> Every new defdata type is instantiated for every polymorphic
 
500
     signature (specified via sig) that matches (one of its argument
 
501
     types).</li>
 
502
<li> Every new polymorphic signature is appropriately instantiated for
 
503
     all defdata types of the right shape in the current world. </li>
 
504
</ul>
 
505
 
 
506
<p> Dependent type hypotheses are supported by @('sig') -- e.g. the
 
507
polymorphic signature of <tt>nth</tt> is specified as follows.  </p>
 
508
 
 
509
@({
 
510
  (sig nth (nat (listof :a)) => :a
 
511
       :satisfies (< x1 (len x2)))
 
512
})
 
513
 
 
514
<h5>Other Theory Reasoning</h5>
 
515
 
 
516
<p>Theory support for Records (structs) and Maps has been tuned to be more
 
517
robust. Destructor Elimination is now available for records.</p>
 
518
 
 
519
<h5>Advanced Usage</h5>
 
520
<p>
 
521
@('Defdata') has been re-engineered to have a plug-in like
 
522
architecture. The following macros provide ways to extend the Defdata
 
523
language and its semantics.</p>
 
524
<dl>
 
525
<dd> @('register-type') -- Register a name as a defdata type (with its associated metadata).</dd>
 
526
<dd> @('register-data-constructor') -- Register a data constructor (for product types).</dd>
 
527
<dd> @('register-user-combinator') -- Add user-defined syntactic sugar to the defdata language. 
 
528
e.g. <i>alistof</i> was added with minimal coding overhead using this facility (See defdata/alistof.lisp).</dd>
 
529
<dd> @('defdata-attach') -- Replaces/subsumes) defdata-testing; it can be used to change or add defdata type metadata. </dd>
 
530
</dl>
 
531
 
 
532
 
 
533
<h3>Defsort</h3>
 
534
 
 
535
<p>The interface to @(see defsort) has been extended, and it can now reuse
 
536
existing list recognizers.</p>
 
537
 
 
538
<p>Defsort can now (optionally) prove that the new sorting function is
 
539
equivalent to an insertion sort.</p>
 
540
 
 
541
<p>Defsort now allows extra arguments, e.g., to parameterize the sort.</p>
 
542
 
 
543
 
 
544
 
 
545
<h3>Tools</h3>
 
546
 
 
547
<p>The @(see include-raw) utility has been made more robust.  It now checks the
 
548
write-date of compiled files, to avoid including stale files.</p>
 
549
 
 
550
<p>The utilities @(see profile-acl2) and @(see profile-all) now work in the
 
551
ACL2 loop, and are documented.</p>
 
552
 
 
553
<p>The @('watch') utility works again.  Thanks to Bob Boyer for providing
 
554
fixes.  To use this utility:</p>
 
555
 
 
556
@({
 
557
   (include-book \"centaur/memoize/old/watch\" :dir :system :ttags :all)
 
558
   :q
 
559
   (watch)
 
560
   (lp)
 
561
   ; Now in Emacs, bring into a buffer the file reported by (watch), whose
 
562
   ; name is of the form watch-output-temp-n.lsp.  Then execute ACL2 forms.
 
563
})
 
564
 
 
565
<p>The @(see untranslate-patterns) tool is now compatible with @(see define)'s
 
566
@(see untranslate-preprocess) hook.</p>
 
567
 
 
568
 
 
569
<h3>OSLIB</h3>
 
570
 
 
571
<p>OSLIB has been reorganized to try to make it somewhat more coherent.  Most
 
572
files in oslib are now split up into, e.g., argv-logic.lisp (no raw code or
 
573
ttags) and argv.lisp (actual implementation).</p>
 
574
 
 
575
<p>OSLIB has new functions including @(see oslib::dirname), @(see
 
576
oslib::basename), @(see oslib::copy), and @(see oslib::catpaths).</p>
 
577
 
 
578
<p>The @(see oslib::ls), @(see oslib::ls-files), and @(see oslib::ls-subdirs)
 
579
functions have been improved to return better error information, and made more
 
580
portable across Lisps.</p>
 
581
 
 
582
<h3>Tau</h3>
 
583
 
 
584
<p>The book @('tau/bounders/elementary-bounders') has been improved by adding
 
585
guards, thanks to Dmitry Nadezhin.</p>
 
586
 
 
587
<h2>Changes to Centaur Libraries</h2>
 
588
 
 
589
<h3>@(see bitops)</h3>
 
590
 
 
591
<p>The new @(see bitops/part-install) macro can be used to set particular bits of an
 
592
integer to a value.  It is somewhat similar to utilities like @(see wrb) from
 
593
the IHS library, but its interface is perhaps more intuitive.</p>
 
594
 
 
595
<p>The new @(see bitops/fast-rotate) macros provide optimized versions of @(see
 
596
rotate-left) and @(see rotate-right).</p>
 
597
 
 
598
<p>The new @(see bitops/logbitp-bounds) book provides a few lemmas relating
 
599
@(see logbitp) to @(see expt).</p>
 
600
 
 
601
 
 
602
<h3>@(see fty::fty)</h3>
 
603
 
 
604
<p>The @(see std::deflist) and @(see fty::deflist) books are now integrated, so
 
605
that @('fty::deflist') can provide the ordinary @('std::deflist') theorems.
 
606
The @('fty::deflist') and @('fty::defalist') macros now provide at least @(see
 
607
append) theorems by default.</p>
 
608
 
 
609
<p>The documentation-generating macros have been enhanced.</p>
 
610
 
 
611
<p>The @(see fty::deftypes) macro now uses more aggressive theory management to
 
612
speed up certification, and also has more comprehensive error checking.</p>
 
613
 
 
614
<p>The @(see fty::deffixtype) macro has better error checking.</p>
 
615
 
 
616
<p>The cases macros introduced by @(see fty::deftypes) now support an
 
617
@(':otherwise') case.</p>
 
618
 
 
619
<p>The @(see fty::deftypes) @('make-') macros now disallow duplicated
 
620
keywords.</p>
 
621
 
 
622
<p>The @(see fty::deflist) and @(see fty::defalist) macros can now tolerate
 
623
already-defined predicates.</p>
 
624
 
 
625
<p>The @(see fty::basetypes) book has been filled out a bit, e.g., it now includes
 
626
@(see maybe-natp).</p>
 
627
 
 
628
<p>By default, @(see fty::deffixtype) now verifies the guards on the equivalence
 
629
relations it introduces.</p>
 
630
 
 
631
<h3>@(see Quicklisp)</h3>
 
632
 
 
633
<p>Quicklisp can now read proxy information from the @('HTTP_PROXY_WITH_PORT')
 
634
environment variable.  See also the \"Using a proxy\" page in @(see
 
635
books-certification).  BOZO move that into Quicklisp?  Blah, all this stuff
 
636
always ends up duplicated everywhere.</p>
 
637
 
 
638
<p>Quicklisp now includes books for loading the @('uiop') library and a more
 
639
sensible @('cl-fad') book.  These libraries may be useful for doing file system
 
640
things.  The CCL-only restrictions on @('bordeaux-threads') and
 
641
@('hunchentoot') have been dropped since these libraries seem to be working
 
642
fine on modern SBCL distributions.  A book for the @('html-template') library
 
643
has also been added.</p>
 
644
 
 
645
<p>The Quicklisp build should be more robust.  It now checks for existing
 
646
Quicklisp installations and produce a sensible error message instead of dying
 
647
horribly.</p>
 
648
 
 
649
 
 
650
<h3>Other</h3>
 
651
 
 
652
<p>The @(see getopt) library now has a basic test suite.</p>
 
653
 
 
654
<p>The @('centaur/misc/sharedlibs') code for relocating shared libraries has
 
655
been extended with a test/demo script.  The sharedlibs functions no longer
 
656
cause errors when used on non-CCL Lisps (they simply print a message,
 
657
instead.)</p>
 
658
 
 
659
<p>The @(see template-subst) tool has been expanded with some additional
 
660
functions.</p>
 
661
 
 
662
<p>The @(see profile-all) and @(see profile-acl2) functions can now be used
 
663
from within the ACL2 loop instead of only from raw Lisp.</p>
 
664
 
 
665
<p>The @(see flag::def-doublevar-induction) macro has been extended and improved.</p>
 
666
 
 
667
<p>For @(see esim), there is a new tool for @(see stv) decomposition theorems,
 
668
@('oracle/stv-decomp-theory-expander.lisp'), and a demo of using this tool in
 
669
@('centaur/regression/composed-stv.lisp').  The documentation tables for STVs
 
670
should now look nicer in the printer-friendly xdoc view.</p>
 
671
 
 
672
<p>In the @(see 4v) library, there are a few new @(see *sexpr-rewrites*).</p>
 
673
 
 
674
<p>Minor bug-fix to avoid complaint in an @(see aignet) @('bind-free')
 
675
routine.</p>
 
676
 
 
677
<p>Added @(see satlink::gather-benchmarks), a plugin for collecting DIMACS
 
678
files that SATLINK sends to the SAT solver. You could use this to gather
 
679
benchmarks for evaluating SAT solvers or for the SAT solving competitions.</p>
 
680
 
 
681
<p>In @(see gl), fixed a bug in @('trace-gl-interp').</p>
 
682
 
 
683
 
 
684
 
 
685
<h3>VL Changes</h3>
 
686
 
 
687
<p>VL has undergone significant extensions and changes, mostly toward extending
 
688
VL to support a subset of SystemVerilog.  VL is intended to also still support
 
689
Verilog-2005, and in many cases its Verilog-2005 support has been improved as
 
690
new SystemVerilog features have been implemented.  Some highlights:</p>
 
691
 
 
692
<ul>
 
693
 
 
694
<li>VL now has a more extensive \"systest\" suite for checking its work against
 
695
NCVerilog and VCS, and a preliminary \"failtest\" suite for ensuring that
 
696
certain modules with bad constructs are properly rejected.</li>
 
697
 
 
698
<li>Added parsing support for many constructs such as interfaces, packages,
 
699
generate statements, structs, unpacked arrays, etc.  The parser functions now
 
700
pass around a \"parse state\" object and generates warnings in a more coherent
 
701
way.  This results in certain speedups to its certification and allows for
 
702
distinguishing the names of data types from other identifiers, which is
 
703
necessary for parsing certain constructs.</li>
 
704
 
 
705
<li>More comprehensive parameter support.  This involved reworking
 
706
unparameterization to handle SystemVerilog data types, and adding support for
 
707
richer expressions in wire ranges, etc., by reworking how constant expressions
 
708
are evaluated to handle many more operators and operands of mixed sizes/types.
 
709
Generate statements are also now supported to some degree.</li>
 
710
 
 
711
<li>Added support for fancier ports, e.g., ports with data types, module
 
712
instances with @('.name') and @('.*') style connections, and interface
 
713
ports.</li>
 
714
 
 
715
<li>Added support for combinational user-defined primitives, and at least basic
 
716
parsing support for sequential UDPs.</li>
 
717
 
 
718
<li>Added some support for SystemVerilog packages and imports.  A new
 
719
\"scopestack\" abstraction is now widely used to provide more comprehensive
 
720
handling of nested scopes (e.g., named begin/end blocks), packages, etc.  There
 
721
is now some support for functions defined at the global scope.</li>
 
722
 
 
723
<li>Sizing has been extended to handle unpacked arrays.  The sizing code has
 
724
been reorganized to be more modular, and extended to handle additional
 
725
operators.</li>
 
726
 
 
727
<li>Miscellaneous improvements.  The pretty-printer has been extended to handle
 
728
the new SystemVerilog constructs, ansi-style ports, etc.  Some transforms are
 
729
more configurable, e.g., gate elimination can easily use alternate replacements
 
730
for gate instances.  There is better support for @('case') statements,
 
731
especially in @('always_comb') blocks.  Various operators are now supported to
 
732
various degrees, e.g., @('++'), casting operators, @('$bits'), streaming
 
733
concatenations.  The preprocessor now supports @('`define') macros with
 
734
arguments.  The hierarchy tools have been greatly simplified.</li>
 
735
 
 
736
<li>Numerous organizational changes, bug fixes, and updates to existing tools
 
737
and transforms to keep things working.</li>
 
738
 
 
739
</ul>
 
740
 
 
741
<p>Besides these improvements to the core library, there have been various user
 
742
interface improvements.  For instance, the VL @(see vl::server) has been
 
743
entirely rewritten and is now included in the @(see vl::kit); it allows you to
 
744
view Verilog modules in a web browser.  The loader has been made more
 
745
user-friendly and more gracefully handles search paths, errors, etc.  The
 
746
@(see vl::lint)er has been tweaked to provide better output and to run more
 
747
quickly.</p>")
 
748
 
 
749
 
51
750
 
52
751
(defxdoc note-6-5-books
53
752
  :parents (note-6-5)
54
753
  :short "Release notes for the ACL2 Community Books for ACL2 6.5 (August
55
754
2014)."
56
755
 
57
 
; Currently covered: through revision 2894.
58
 
 
59
756
  :long "<p>The following is a brief summary of changes made to the @(see
60
757
community-books) between the releases of ACL2 6.4 and 6.5.</p>
61
758
 
295
992
<p>The new @('oracle/') directory contains tools and examples from Oracle,
296
993
Inc.</p>
297
994
 
298
 
 
299
995
<h5>New Demos</h5>
300
996
 
301
997
<p>A new demo, @('demos/tutorial-problems/equivalence-of-two-functions'), shows
1147
1843
 
1148
1844
<p>@('clause-processors/magic-ev') now has special handling for OR.</p>
1149
1845
 
1150
 
<p>The @(see testing) library has been enhanced.</p>
 
1846
<p>The @(see Cgen) library has been enhanced.</p>
1151
1847
 
1152
1848
<p>@(see tshell) now has improved output-filtering capability, which @(see
1153
1849
satlink) takes advantage of.</p>