Release notes for the ACL2 Community Books for ACL2 6.4 (January, 2013).

The following is a brief summary of changes made to the community-books between the releases of ACL2 6.3 and 6.4. See the acl2-books Wiki page on ReleaseVersionNumbers for svn revision numbers corresponding to releases. See also note-6-4 for the changes made to ACL2 itself.

For additional details, you may also see the raw commit log.

In previous versions of ACL2, the default **excludes many books**.

This particularly affects what happens when you run *not* changed how

See books-certification for details about how to use the new build system.

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.3, so we've deleted them.

Previous Location New Location ----------------------------------------------------------------------- finite-set-theory/osets/sets.lisp std/osets/top.lisp finite-set-theory/osets/map.lisp std/osets/* finite-set-theory/osets/map-tests.lisp finite-set-theory/osets/instance.lisp finite-set-theory/osets/membership.lisp finite-set-theory/osets/sort.lisp finite-set-theory/osets/cardinality.lisp finite-set-theory/osets/under-set-equiv.lisp finite-set-theory/osets/quantify.lisp finite-set-theory/osets/computed-hints.lisp finite-set-theory/osets/delete.lisp finite-set-theory/osets/intersect.lisp finite-set-theory/osets/primitives.lisp finite-set-theory/osets/union.lisp finite-set-theory/osets/difference.lisp finite-set-theory/osets/outer.lisp finite-set-theory/osets/portcullis.lisp std/lists/make-character-list.lisp str/* std/lists/coerce.lisp std/misc/explode-atom.lisp std/misc/explode-nonnegative-integer.lisp std/io/unsigned-byte-listp.lisp std/typed-lists/* std/io/signed-byte-listp.lisp std/io/read-object.lisp std/io/base.lisp centaur/aig/base.lisp {aig,faig}-base centaur/aig/three-four.lisp faig-constructors.lisp centaur/misc/resize-list.lisp std/lists/resize-list.lisp centaur/misc/equal-by-nths.lisp std/lists/nth.lisp -----------------------------------------------------------------------

We've moved several books to new homes in an effort to clean up the
top-level

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 cutil (cutil::*) std/util (std::*) (see also cutil/README) Yes tools/defconsts std/util/defconsts Yes serialize/unsound-read std/io/unsound-read No paco projects/paco No milawa projects/milawa No taspi projects/taspi No security projects/security No security/suite-b projects/security/sha-2 No wp-gen projects/wp-gen No concurrent-programs projects/concurrent-programs No deduction/passmore projects/equational No leftist-trees projects/leftist-trees No symbolic projects/symbolic No translators projects/translators No quadratic-reciprocity projects/quadratic-reciprocity No parallel misc/ or, for some books, demos/parallel or system/parallel No tutorial-problems demos/tutorial-problems No workshops/2013-greve-slind coi/defung ----------------------------------------------------------------------

We've deleted the RTL

(include-book "rtl/rel8/lib/top" :dir :system)

with

(include-book "rtl/rel9/support/lib3/top" :dir :system) (include-book "rtl/rel9/arithmetic/top" :dir :system)

We've moved many build scripts like build::cert.pl,

The ACL2 system documentation has been extracted from the ACL2 sources,
converted into xdoc format, and is now located in the Community Books.
This allows for a tighter integration between the system and book
documentation, e.g., system topics like io can now directly link to
related libraries like std/io. See note-6-4 for details; and see
especially the file

A new, feature-rich Emacs-based documentation browser named ACL2-doc has been developed by Matt Kaufmann, and has many features.

We've added at least some minimal xdoc documentation for several projects: see concurrent-programs, des, equational, jfkr, milawa, paco, leftist-trees, sha-2, taspi, and wp-gen.

We've added significant documentation for many books and utilities, including at least:

- build::cert.pl - a build system for certifying ACL2 books
- defconsts - like
defconst but supports stobjs, state, and multiple values - defrstobj - a macro for introducing record-like stobjs
- bitops - an arithmetic library especially for bit-vector arithmetic
- def-universal-equiv - a macro for universally quantified equivalences
- arith-equivs - equivalence relations for naturals, integers, and bits
- set-max-mem - a memory management scheme for ccl
- str::base64 - base64 string encoding/decoding

We've made hundreds of other minor documentation improvements, and we invite everyone to contribute improvements.

- A new std/basic library has been added for basic definitions.
- Optimized bitset libraries (formerly in bitops) are now in std/bitsets.
- std/io has a new read-string utility.
- std::deflist and std::defprojection macros now implement define-like
/// syntax. - The std/util macros now respect set-default-parents.
- std::defaggregate now prohibits duplicate keys in
make- andchange- macros. - std::defaggregate macro now has a new
:legiblep :ordered option, which balances performance and legibility. - define now saves some additional information about definitions in tables.
- Fixed bugs with the untranslate-preprocess support in define.

- Added a
str::binify function, similar to str::hexify. - Documented
binify andhexify .

coi/util/defun-support now numbers congruence theorems.coi/nary/nary has been tweaked with double-rewrite and now has additional examples; seecoi/nary/example2.lisp - Fixed name clashes between
coi/generalize andwitness-cp

- Added significant documentation, including overview documentation.
- Added fast bitops::bitops/fast-logrev and bitops::bitops/merge functions.
- Reduced dependencies and use of non-local includes.

rtl/rel9 library now certifies much faster.- Clarified licensing information on RTL libraries (GPL).

- Added support for
<table> tags. - Added xdoc::preprocessor
@(`...`) syntax for Lisp evaluation within documentation strings. - The
:xdoc command now shows where topics came from, and prints parents more nicely. - xdoc::save now warns about redefined topics and broken (internal) links.
- xdoc::save now creates a link checking page to identify broken external links.
- xdoc::xdoc-prepend and xdoc-extend now have additional error checking.

- Reimplemented defrstobj to be based on abstract stobjs.
- Large rstobjs are now faster to define.
- Good-rstobj predicates are no longer necessary.
- Generalized def-typed-record to support more general fixing functions, for better compatibility with new gl features.
- Moved old defrstobj code to legacy-defrstobj.

- Optimized symbolic subtraction and logeqv.
- Optimized path condition handling in AIG modes.
- Added a vacuity check in AIG modes.
- gl-mbe has been reimplemented using gl::gl-assert, a more general mechanism.
- A new gl::gl-concretize utility gives more control over GL in AIG modes.
- Added gl-force-true-strong and gl-force-false-strong.
- logcons can now unify with integer g-number objects.
- Fixed a bug with gl-mbe printing.
- Tweaks for better counterexample printing.
- Tweaks to avoid overwriting a user's gl-mode by including GL books.

- New aig-constructors ruleset.
- Added aignet aiger file reader/writers.

- Improved compatibility with additional SAT solvers.
- Documented various satlink::sat-solver-options that are known to work.
- Added scripts for using solvers with (external, unverified) satlink::unsat-checking capabilities.
- Optimization to avoid stack overflows in satlink::eval-formula.
:verbose mode no longer prints variable assignments (they were sometimes too long for Emacs to handle).

bed::bed is a new, preliminary library for Boolean expression diagrams.

- Expanded vl2014::always-top with support for basic
case statements. - Expanded vl2014::expr-simp to make more reductions and be more modular.
- Added new support for hierarchical identifiers.
- Cleaned up support for gate instances.
- Multiplier synthesis now better matches GL's multipliers.
- Modernized and documented many files.

- Added a compiler from symbolic-test-vectors into C++ programs.
- Guards are now verified on
map-aig-vars-fast . esim/stv/stv-decomp-proofs.lisp adds a special theory for decomposition proofs; see the multiplier demo in the esim-tutorial.

- sexpr-rewriting now works toward a fixpoint to better support decomposition proofs.
- Added 4v-sexpr-purebool-p for detecting pure Boolean 4v-sexprs
- Documented sexpr-equivs.

- The multiplier proof by decomposition now has comments
- Added a decomposition proof using rewriting, instead of by GL

A new tool,

A new tool,

A new tool,

A new book,

A new book, *A
Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor
View* by J Moore, in Formal Methods in System Design, March 1999.

A new book,

Added some type theorems to

Updated version of

The Cgen library has been enhanced.

tshell now has improved output-filtering capability, which satlink takes advantage of.

def-universal-equiv now features xdoc integration.

Fixed a bug related to undoing inclusion of the

Added a workaround for a program-mode bug in SULFA's

Fixed guard violations in

Fixed a couple of clashes between

milawa. Integrated Milawa into

The

- The Makefile has been made more robust, especially for ACL2(r).
- To improve the error message when attempting to use non-GNU implementations
of
make , the filebooks/Makefile has been renamed tobooks/GNUmakefile . A trivialMakefile which simply prints an error has been added for non-GNU makes.

- Mostly fix back-button issues.
- Fixes for compatibility with Internet Explorer and Safari.
- Broken links now properly lead to the broken-link topic.
- Added "package box" to shows what package non-ACL2 topics are from, to reduce confusion.
- Added download this manual feature.
- Added printer friendly feature
- Clarified the scope of LICENSE files in XDOC manuals.
- Other bugfixes and cosmetic tweaks.