Note-6-4-books
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.
Build System Changes
In previous versions of ACL2, the default make command for building the
Community Books could take several hours. Starting in ACL2 6.4, the default
build is much faster because it excludes many books.
This particularly affects what happens when you run make from the
books directory. We have not changed how make regression
works from the acl2-sources directory—it still builds (nearly) all
of the books.
See books-certification for details about how to use the new build
system.
Deleted Stubs
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
-----------------------------------------------------------------------
Book Reorganization
We've moved several books to new homes in an effort to clean up the
top-level books directory. Users of these libraries will need to update
their include-book commands, and in some cases, packages may 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 include-books eventually.
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
----------------------------------------------------------------------
Deprecated Books
We've deleted the RTL rel7 and rel8 directories; please upgrade to
rtl/rel9. Note that rel8 is essentially part of rel9, so if you
can't directly upgrade to rel9, you may try replacing
(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)
Scripts Moved
We've moved many build scripts like build::cert.pl, clean.pl,
and critpath.pl from the top-level books directory, into a new
books/build directory. You may need to update paths to these files in
your Makefiles or other build scripts.
Documentation Changes
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 system/doc/acl2-doc.lisp.
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.
Enhancements to Particular Libraries
General Libraries
std - standard libraries
- Added a str::binify function, similar to str::hexify.
- Documented binify and hexify.
coi - family of libraries
- coi/util/defun-support now numbers congruence theorems.
- coi/nary/nary has been tweaked with double-rewrite and now
has additional examples; see coi/nary/example2.lisp
- Fixed name clashes between coi/generalize and witness-cp
bitops - arithmetic library
rtl - arithmetic library
- rtl/rel9 library now certifies much faster.
- Clarified licensing information on RTL libraries (GPL).
xdoc - documentation system
- 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.
defrstobj - machine modeling library
- 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.
GL and Boolean Reasoning
gl - bit-blasting tool
- 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.
aig and aignet - and inverter graph libraries
satlink - interface to sat solvers
- 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.
Hardware Verification Libraries
vl - Verilog toolkit
- 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.
esim - symbolic hardware simulator
- 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.
4v-sexprs - four-valued logic of esim
esim-tutorial - ESIM hardware verification demos
- The multiplier proof by decomposition now has comments
- Added a decomposition proof using rewriting, instead of by GL
New Tools and Examples
A new tool, centaur/misc/outer-local, lets you mark events as
local to an external context.
A new tool, tools/last-theory-change, lets you see when a rule was last
enabled or disabled.
A new tool, centaur/misc/dag-measure, may be useful when writing
functions that traverse directed acyclic graphs.
A new book, misc/enumerate.lisp, demonstrates a trick by J Moore to
separately consider all possible cases for a particular term during a
proof.
A new book, misc/multi-v-uni.lisp, includes a result from 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, demos/patterned-congruences.lisp demonstrates patterned-congruence rules.
Miscellaneous Libraries
Added some type theorems to regex-ui.
Updated version of models/jvm/m1/wormhole-abstraction.
clause-processors/magic-ev now has special handling for OR.
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 intern-debugging
book.
Added a workaround for a program-mode bug in SULFA's
sat/local-clause-simp.lisp.
Fixed guard violations in workshops/2004/sumners-ray/support/invp.lisp
and workshops/2009/sumners/support/kas.lisp.
Fixed a couple of clashes between arithmetic-5/ihs and bitops.
milawa. Integrated Milawa into books/Makefile; fixed some
issues with ccl:: prefixes and other non-portable constructs.
The ordinals library is now licensed under a (more permissive)
BSD-style license.
Other Changes
Make system
- 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 file books/Makefile has been renamed to
books/GNUmakefile. A trivial Makefile which simply prints an error
has been added for non-GNU makes.
XDOC Fancy Viewer - documentation web pages
- 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.
