|
|
|---|
|
|
|
|---|
Release notes for the ACL2 Community Books for ACL2 6.5 (August 2014).
The following is a brief summary of changes made to the community-books between the releases of ACL2 6.4 and 6.5.
The acl2-books Wiki page on ReleaseVersionNumbers gives SVN revision numbers corresponding to releases. See also note-6-5 for the changes made to ACL2 itself. For additional details, you may also see the raw commit log.
When we move a book, we often add a stub book in its previous location to help you transition your include-book commands. The build::cert.pl build system prints warnings when a stub book is being included.
Stub books have a lifespan of one release. The following books were stubs in ACL2 6.4, so we've deleted them.
Previous Location New Location ------------------------------------------------------------------ cutil/*.lisp std/util/*.lisp tools/defconsts std/util/defconsts parallel/with-waterfall-parallelism misc/with-waterfall-parallelism parallel/without-waterfall-parallelism misc/without-waterfall-parallelism serialize/unsound-read std/io/unsound-read centaur/bitops/bitsets std/bitsets/bitsets centaur/bitops/bitsets-opt std/bitsets/bitsets-opt centaur/bitops/sbitsets std/bitsets/sbitsets ------------------------------------------------------------------
We've moved several books to new homes in an effort to improve the overall organization of the books. Users of these libraries will need to update their include-book commands, and in some cases, packages have also changed.
The table below shows which libraries have moved and where they have moved
to. Books with stubs may continue to work until the next release, but you'll
need to update your
Stubs? Previous Location New Location ---------------------------------------------------------------------- Yes str/ std/strings/ No memoize/ centaur/memoize/ No centaur/doc.lisp doc/top.lisp ----------------------------------------------------------------------
The defpkg commands for xdoc, std/strings, std/osets, and std/bitsets have been merged into a single
Preliminary work has been carried out toward unifying coi/std versions of osets. In particular:
The std/lists function
The
The bitops library's
The new
Support for ACL2(r) is now directly included in the top-level Makefile.
ACL2(r) users no longer need to use a separate build process and can now make
use of many additional books. Books that are incompatible with ACL2(r) should
be annotated with
The top-level Makefile has been made more robust in various ways.
The build::cert.pl build system has been enhanced in many ways. Of particular note, it now deals more automatically with portcullis files, which may help to improve the reliability of including uncertified files. Other improvements include:
The build speed has been improved in various ways.
Added a TAGS target to the Makefile.
Added scripts to support using a Jenkins continuous integration server to continually rebuild ACL2 and the books on various platforms.
Books contributed by Computational Logic, Inc. are now licensed under a (more permissive) 3-clause BSD style license instead of the GNU General Public License.
Books contributed by Centaur Technology, Inc. are now licensed under a (more permissive) MIT/X11 style license instead of the GNU General Public License.
Books contributed by Jared Davis / Kookamara are now licensed under an MIT/X11 style license instead of the GNU General Public License.
Many books that lacked explicit licensing information have been updated to include appropriate copyright headers.
The
The new remove-hyps tool may be useful for identifying unnecessary hypotheses in theorems.
fty is a new library offers functionality similar to std or defdata libraries. This library enforces a certain fixing-function discipline and may help to avoid many type-like hypotheses on theorems.
The new book
The new with-supporters macro can be used to automatically produce redundant versions of events that are needed from local include books.
The new flag::def-doublevar-induction macro can be used to create certain kinds of induction schemes, and may be especially useful for proving congruence rules about mutually recursive functions.
The new nrev book is something like
The new fast-alist-pop function provides something akin to
The new
The new
A new demo,
A new demo,
COI's
A new demo,
The
There are now some preliminary recommendations for best-practices for developing ACL2 books.
The documentation for portions of the ihs library and plev had been inadvertently excluded from the manual, but are now included.
A new topic describes some noteworthy clause-processor-tools.
The topic hierarchy has received some attention, e.g., all topics that were
formerly listed under the grab-bag
Converted the documentation for esim, b*, and other topics into xdoc format.
Many topics have been improved by eliminating typos, making minor
clarifications, adding appropriate cross-references, fixing broken links, and
ensuring that
The new xdoc::order-subtopics command can be used to control the order that subtopics are presented in.
The "classic" XDOC viewer is no longer supported.
The XDOC viewers have been improved in many ways.
Various bugs have also been fixed in the core XDOC system.
Other minor changes:
A new book of basic induction-schemes has been added.
Certain equivalence relations like chareqv and streqv have
been factored out of the std/strings library and moved into
lnfix and lifix are now enabled, inlined functions instead of
macros. This may help to simplify guard obligations in functions that call
An std/lists/update-nth book has been added.
A
Added a missing rule about ACL2-count to
uniquep no longer uses equality-variants. Theorems that
target
Various books have been reorganized to reduce dependencies.
The general purpose alist functions append-alist-vals and append-alist-keys have been moved out of vl and into std/alists.
There are new books for alist-fix and hons-remove-assoc.
The new
Various books have been reorganized to reduce dependencies.
Most osets functions are now disabled by default. They can be re-enabled
using the ruleset
Some useful but sometimes expensive rules, including for instance the set::pick-a-point-subset-strategy and set::double-containment, and also
including other rules such as the transitivity of set::subset, are now
disabled by default. They can be re-enabled using the ruleset
Some new macros have been added.
The define macro has been improved in many ways.
Other macros have also been improved in various ways.
Many macros now have a
The
There are now books for many built-in ACL2 list recognizers that were previously not covered, e.g., boolean-listp, integer-listp, etc.
Many logical definitions throughout the std/strings library have been cleaned up. Also, many definitions have been changed to use define for better documentation.
The new book
The new str::pretty routine can convert arbitrary ACL2 objects into pretty-printed strings. Is a fast, state-free, logic mode reimplementation of much of ACL2's pretty printer.
There are now a much richer collection of numeric functions, especially for non-decimal bases; see str::numbers.
The string library now has a very efficient, bitset-like way to represent sets of characters, and some functions for working with these character sets. See str::charset-p.
The read-string function will now produce better error messages and
can (optionally, via raw Lisp) avoid checking
Defdata's output has been tweaked.
The defdata library now supports range types.
Counterexample generation has been updated to use tau instead of the former
COI's
The experimental quicklisp build has been updated in many ways.
Quicklisp files are now installed under the
The Quicklisp install can be carried out using a proxy.
The quicklisp books now include support for the
oslib::getpid has been extended to work on Lisps other than CCL.
Added minimal tests to oslib functions such as oslib::file-kind and oslib::date.
OSLIB has new oslib::lisp-type and oslib::lisp-version functions.
A new book,
We have remove dependencies on
The
GL has better if handling, and as a result may be better able to cope with unsatisfiable path conditions (i.e., unreachable code regions) when using SAT-based gl::modes.
New gl::preferred-definitions may slightly improve performance of bit-vector operations like logcar, logcdr, loghead, and logtail.
Some symbolic arithmetic functions have been changed so as to possibly improve AIG performance.
GL's rewrites to 4v constants have been improved.
The new macro gl::gl-thm is like def-gl-thm, but doesn't store the theorem. That is, it's like thm is to defthm. Similarly, gl::gl-param-thm is to def-gl-param-thm, and def-gl-rule is similar to defrule.
The definitions of
Minor bugs have been fixed.
The documentation for GL has been generally improved.
VL has been significantly refactored. All of the internal vl::syntax is now based on fty, which is a major change. The representation of vl::statements is especially different.
VL is beginning to gain support for some limited SystemVerilog constructs. This is a major change that affects all areas, e.g., lexing, parsing, syntax, and transformations.
VL now support certain kinds of combinational always blocks. It also supports richer edge-triggered always blocks, including, e.g., registers with asynchronous set/reset signals.
Many bugs have been fixed, some severe. For instance, VL was incorrectly
translating BUF, NOT, and XNOR gates with "extra" terminals. The new VL
Warnings have been improved. For instance, VL now warns about 0-bit replications since some Verilog tools do not implement them correctly.
Many ttags have been removed from VL, using nrev.
VL's always/delay transforms can now optionally produce less bitblasted modules.
The vl::kit includes new commands such as
Numerous other minor bug fixes, extensions, performance improvements, etc.
satlink now uses
The default sexpr-rewriting rules have been expanded and improved. These changes may improve decomposition proofs and also the performance of GL-based STV proofs.
tshell should now handle interrupts more reliably.
The executable counterparts of symbolic-test-vectors are now disabled by default.
There is now better support for decomposition proofs of symbolic-test-vectors, see files such as
The new stv-run-for-all-dontcares function is a less conservative alternative to stv-run.
Some lemmas have been localized in esim.
aignet now has a basic
The bridge::json-encoding routines now use define for better documentation.
Some aignet functions and
The bitops
Improved and documented the logbitp-reasoning hint.
Added bit->bool to the bitops library.
The new
(File interface/emacs/inf-acl2.el) One now gets a clear error, suggesting a
solution, when Emacs command
The make-flag tool now uses slightly faster, more robust hints.
The witness-cp clause processor has been made more flexible.
The
The def-universal-equiv macro now takes an
The
The book
Something happened to profiling.lisp in r2423.
disassemble$ now supports macro aliases.
Several ordinary files that were incorrectly marked as executable are now properly non-executable.
The tau
Many explicit function definitions have been replaced with constraints, in
order to make theorems about those functions more useful for functional
instantiation later. For example, instead of insisting that
The theory of integration is now updated to conform to the current version of continuity and differentiability (which allows functions that are only continuous or differentiable over a particular domain).
The concepts of continuity, differentiability, and integration now have both non-standard and classical definitions. These are shown to be equivalent for classical functions without parameters. Even when parameters are present, the classical definitions can be used to take advantage of important theorems, such as the intermediate-value theorem, mean-value theorem, fundamental theorem of calculus, etc.