		Search-engine friendly clone of the ACL2 documentation.

Note-7-0-books

Release notes for the ACL2 Community Books for ACL2 7.0 (January 2015)

The following is a brief summary of changes made to the community-books between the releases of ACL2 6.5 and 7.0.

The acl2-books Wiki page on Release Version Numbers gives the Git/SVN revision numbers corresponding to releases. See also note-7-0 for the changes made to ACL2 itself. For additional details, you may also see the raw commit log.

Organizational, Build System, and Name Changes

Source Code Moved

The ACL2 Community Books and ACL2 System source code repositories have been merged into one repository and are now available at

https://github.com/acl2/acl2

See the Readme.md file found there for more details. See also the git-quick-start guide if you are interested in contributing.

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

  Previous Location                New Location
---------------------------------------------------------------
  str/*                            std/strings/*

  xdoc/portcullis                  std/portcullis
  std/osets/portcullis             std/portcullis
  std/bitsets/portcullis           std/portcullis
  std/strings/portcullis           std/portcullis

  coi/osets/instance               std/osets/instance
  coi/osets/computed-hints         std/osets/computed-hints

  centaur/bitops/sign-extend       centaur/bitops/fast-logext

---------------------------------------------------------------

Build System Changes

The arithmetic-2 library is no longer built by default when running an ordinary make. All books that previously depended on arithmetic-2 have been transitioned to use arithmetic-3 instead. If your own work depends on arithmetic-2, you can still build these books, e.g., by running make arithmetic-2 in the books directory.

Many minor tweaks and cleanups have been made to the build system itself.

cert.pl now has better support for provisional-certification.
The build::cert_param mechanism, which is used by build::cert.pl to indicate that books have special requirements, is now documented.
New cert_param directives have been added to avoid certifying certain books on incompatible Lisps.
build::cert.pl now better avoids overflowing the maximum number of arguments to shell commands on some platforms when certifying large numbers of books.
The new :ignore-certs feature of include-book is now used in special two-pass books like std/strings/defs-program.lisp, and should help to make building these books more reliable.
Hundreds of old Makefiles from the books-certification-classic era have been eliminated. Some obsolete GCL-specific directives have also been eliminated.
Installing quicklisp now works from behind a proxy. See Using a Proxy in books-certification for details.
The implementation of ``make everything'' has been cleaned up. In particular, it no longer sets USE_QUICKLISP=1 since this is not appropriate for some Lisps.
The make clean command now does a better job of cleaning up generated files.

Numerous books have been patched up for better portability across Lisps and integration with ACL2(p). For instance: In many cases, previous calls of without-waterfall-parallelism are no longer necessary, largely due to thread-safe memoization; several oslib functions have been extended to work on additional Lisps; many books with raw Lisp code now use include-raw for more portable compilation behavior across Lisps.

Various other utilities have been made more reliable.

For Emacs TAGS users, the etags.sh script has been improved to permit whitespace before definitions.
For ACL2 packaging mechanisms, the fix-cert utility has been improved and now includes scripts for moving ACL2 distributions.

Supporting scripts for the Jenkins continuous integration server can now be found in the build/jenkins directory. These scripts have received significant attention and can now support multi-configuration builds for checking ACL2 books compatibility with many host Lisps.

Name Conflict Resolution

Progress has been made toward resolving name clashes in order to be able to include more books together. This work involves renaming certain lemmas and may require updates to your books.

Arithmetic-2

floor-mod-elim no longer forces its hypothesis.

Arithmetic-5

floor-=-x/y now has additional corollaries.

IHS

floor-mod-elim no longer forces its hypothesis.
floor-=-x/y now has additional corollaries.
justify-floor-recursion has been renamed to floor-recursion.
cancel-floor-+ has been renamed to cancel-floor-+-basic.
cancel-mod-+ has been renamed to cancel-mod-+-basic.
rationalp-mod no longer requires (rationalp x).

COI/osets

Many coi/osets books are now just small wrappers around std/osets books.
COI's double-containment rule has been renamed to double-containment-expensive.

Licensing Changes

Robert Krug's arithmetic-3 library of is now available under a BSD-3-Clause style license instead of the GNU General Public License.

Several books contributed by David Rager, which were formerly released under the GNU General Public License or a BSD-3-Clause style license, are now instead released under a (more permissive) MIT/X11-style license.

Several books contributed by Oracle, which were formerly released under the GNU General Public License, are now instead released under an MIT/X11-style license.

The ubdds library and a few "miscellaneous" books have also been transitioned from the GNU General Public License to a 3-clause BSD style license.

Several books in the coi library, which previously lacked explicit license information, now have explicit MIT/X11-style licenses.

New Libraries and Documentation

The ACL2+Books manual has a great deal of new and improved content and many topics have been reorganized to provide a more coherent hierarchy. Notably, all documentation in the legacy defdoc format has been rewritten into the xdoc format. Some highlights:

The ihs documentation has been considerably updated.
The defsort macro is now documented.
The sneaky documentation has been considerably expanded.
Topics like lists, strings, alists, etc., now group together some related programming functions.

The ACL2 Sidekick is an experimental and very preliminary graphical add-on to ACL2. It currently features a session viewer, theory linter, a horribly primitive interface to the proof-builder, and a slick Lookup feature that can show you documentation and other information about various symbols.

The new system/toothbrush directory provides a way to create applications with ACL2 that have a much smaller memory footprint than an ordinary ACL2 save-exec image. See the README file in this directory for more information.

The new depgraph::depgraph library now contains a few algorithms for working with dependency graphs. It provides depgraph::toposort, a topological sort, depgraph::invert, an edge-inversion algorithm, and depgraph::transdeps, which can compute the transitive dependencies for a set of nodes. This functionality was formerly part of vl but has now been made more general and extracted.

The new projects/codewalker/ directory contains Codewalker, a utility for exploring code in any programming language specified by an ACL2 model to discover certain properties of the code. Demos of Codewalker are also in that directory.

The new directory projects/hybrid-systems/ is a specification/verification project by Shant Harutuntian using ACL2(r) (see real), in support of his 2007 Ph.D. dissertation, with a few recent updates (because of ACL2 changes) made by Cuong Chau.

There are also several new small tools and books.

(CCL Only) The new spacewalk tool can be used to get a report about heap memory usage. It may be useful for identifying unusually large functions and constants in your ACL2 session.
The new simp tool can be used to ask ACL2 to simplify terms under certain hypotheses.
The new tool misc/check-fn-inst can be used to check the constraints to a functional instantiation.
The new tool, def-saved-obligs, can be used to save proof obligations for an event as independent defthms.
The new tool, system/dead-source-code.lisp, may be useful for finding dead code in the ACL2 sources.
The new books system/cantor-pairing-bijective.lisp and system/hl-nat-combine-onto.lisp contain proofs of bijectivity and surjectivity (one-one/onto and onto, respectively) of cantor-pairing functions.

Changes to Major Libraries

XDOC Changes

The web-based XDOC viewer has been improved. It now uses newer versions of the JQuery and Typeahead libraries. Some bugs with the typeahead (jump to) box have been fixed and it has been extended to show more results. The jump-to box has been extended with a Alt+/ hotkey (or perhaps some other key combination like Ctrl+/, depending on your browser). Middle clicking on XDOC links should now properly open them in new tabs and the fonts have been updated. Some ugly quotes are now replaced by ``smart'' replacements.

Significant work has been done to try to make XDOC content accessible to search engines such as Google. A new PHP script largely replaces previous failed efforts to generate "static" HTML files, site maps, and so forth.

XDOC now supports "resource directories" for incorporating images, PDF files, and other kinds of resources. See xdoc::add-resource-directory for details.

XDOC now features xdoc::katex-integration for writing LaTeX-like formulas like \left( \sum_{i=0}^{n} \sqrt{f(i)} \right) < \frac{n^2}{k} within your documentation. Note that ACL2's new fancy-string-reader can be used to make escaping simpler, and this may be especially useful when trying to write LaTeX-like formulas, where the escaping of \ characters can be irritating.

There are also many other minor changes:

The defpointer macro has been integrated into XDOC itself. (It was formerly only part of the ACL2 system documentation.)
defsection and define now permit plain strings to be included among the list of events. These strings are incorporated into the resulting documentation as running commentary.
The defxdoc, defsection, and define macros now all evaluate the arguments to :short and :long instead of quoting them. This may make it more convenient to write macros that produce documentation from boilerplate templates, e.g., you can now directly write things like :short (cat ...).
Tweaked defsection so that you can give :extension (foo) instead of just :extension foo.
Better error handling on xdoc-extend and xdoc::xdoc-prepend.

std Library Changes

std/basic

Added tuplep and impossible.

std/lists

Cleaned up rules about take in std/lists/take.

replicate is now an alias for repeat and is compatible with the definition of repeat in the COI libraries, fixing a longstanding incompatibility.

The all-equalp function has been added.

Several lemmas about intersection$, intersectp, and set-difference$ have been extracted from vl and moved into std/lists. See for instance std/lists/intersection$, std/lists/intersectp, and std/lists/set-difference.

std/util

The b* binders for std::defaggregates now also bind the variable, fixing a longstanding issue. Also, the syntax ((prodname name)) is now permitted as an abbreviation for ((prodname name) name). (This is often useful when destructuring a function's arguments).

The b* binders for std::defaggregate (and also fty::defprod) are now extensible and can translate bindings like x.foo into calls of user-defined functions. See the description of Extra Binder Names in the documentation of std::defaggregate for details.

The std::deflist, std::defalist, std::defprojection, and std::defmapappend macros are now "pluggable" and can be extended with additional theorems; see for instance the new book std/lists/abstract.lisp.

The new books std/util/deflist-base and std/util/defalist-base offer lighter-weight alternative to std/util/deflist and std/util/defalist.

The defrule book now has fewer dependencies.

Documentation for std::deflist has been improved. Deflist now uses define so that you get a signature block in the resulting documentation. The documentation for automatically generated deflist events is now put in a more sensible order and split off into a foolistp-basics section underneath of foolistp, to reduce the prominence of this "boilerplate" documentation. Deflist can now also create documentation even in the already-definedp case.

Fixed an obscure bug with define's return-specifiers that could affect non-executable functions that involve stobjs.

The define macro now interprets :inline nil as "make this a $notinline function" instead of "make this a regular function instead of an inline one."

The define, defines, and also the fty::deffixequiv macros now have improved, more advanced default hints set for inductive proofs in return specs and deffixequiv(-mutual) forms.

std/strings

Certification time has been improved.

The fast-cat book (see str::cat) now uses include-raw to avoid possible issues on various Lisps.

std/io

Added read-file-as-string function.

std/alists

There are some new functions: fal-find-any and fal-all-boundp.

Moved worth-hashing into std/alists from misc/hons-help.

std/typed-lists

Move cons-listp and cons-list-listp out of VL and into std/typed-lists.

Defdata (Data Definition Framework)

Defdata has undergone significant improvements. Automated theorem proving support has been increased by a tight integration with Tau-system. A significant new capability is the support for parametric polymorphism via sig rules. There have been many improvements in its engineering too.

Tau Integration

Defdata analyzes the predicate definition of every new type and, if possible, produces a set of Tau rules that completely characterize the type. Defdata thus provides the following guarantee: If Tau is complete over the type reasoning theory, then adding a type to the current theory via defdata preserves completeness.

Parametric Polymorphism

Defdata provides a new macro sig which can be used to define signatures of polymorphic functions such as append, remove1, put-assoc etc:

(sig append ((listof :a) (listof :a)) => (listof :a))
(sig remove1-equal (all (listof :a)) => (listof :a))
(sig put-assoc-equal (:a :b (alistof :a :b)) => (alistof :a :b))

Defdata automatically instantiates these generic theorems (type signatures) for previously defined types and as new types are defined after the sig forms. Defdata, thus implements parametric polymorphism, by providing the following invariants:

Every new defdata type is instantiated for every polymorphic signature (specified via sig) that matches (one of its argument types).
Every new polymorphic signature is appropriately instantiated for all defdata types of the right shape in the current world.

Dependent type hypotheses are supported by sig -- e.g. the polymorphic signature of nth is specified as follows.

(sig nth (nat (listof :a)) => :a
     :satisfies (< x1 (len x2)))

Other Theory Reasoning

Theory support for Records (structs) and Maps has been tuned to be more robust. Destructor Elimination is now available for records.

Advanced Usage

Defdata has been re-engineered to have a plug-in like architecture. The following macros provide ways to extend the Defdata language and its semantics.

register-user-combinator -- Add user-defined syntactic sugar to the defdata language. e.g. alistof was added with minimal coding overhead using this facility (See defdata/alistof.lisp).

defdata-attach -- Replaces/subsumes) defdata-testing; it can be used to change or add defdata type metadata.

Defsort

The interface to defsort has been extended, and it can now reuse existing list recognizers.

Defsort can now (optionally) prove that the new sorting function is equivalent to an insertion sort.

Defsort now allows extra arguments, e.g., to parameterize the sort.

Tools

The include-raw utility has been made more robust. It now checks the write-date of compiled files, to avoid including stale files.

The utilities profile-ACL2 and profile-all now work in the ACL2 loop, and are documented.

The watch utility works again. Thanks to Bob Boyer for providing fixes. To use this utility:

(include-book "centaur/memoize/old/watch" :dir :system :ttags :all)
:q
(watch)
(lp)
; Now in Emacs, bring into a buffer the file reported by (watch), whose
; name is of the form watch-output-temp-n.lsp.  Then execute ACL2 forms.

The untranslate-patterns tool is now compatible with define's untranslate-preprocess hook.

OSLIB

OSLIB has been reorganized to try to make it somewhat more coherent. Most files in oslib are now split up into, e.g., argv-logic.lisp (no raw code or ttags) and argv.lisp (actual implementation).

OSLIB has new functions including oslib::dirname, oslib::basename, oslib::copy, and oslib::catpaths.

The oslib::ls, oslib::ls-files, and oslib::ls-subdirs functions have been improved to return better error information, and made more portable across Lisps.

Tau

The book tau/bounders/elementary-bounders has been improved by adding guards, thanks to Dmitry Nadezhin.

Changes to Centaur Libraries

bitops

The new bitops::bitops/part-install macro can be used to set particular bits of an integer to a value. It is somewhat similar to utilities like wrb from the IHS library, but its interface is perhaps more intuitive.

The new bitops::bitops/fast-rotate macros provide optimized versions of rotate-left and rotate-right.

The new bitops::bitops/logbitp-bounds book provides a few lemmas relating logbitp to expt.

fty

The std::deflist and fty::deflist books are now integrated, so that fty::deflist can provide the ordinary std::deflist theorems. The fty::deflist and fty::defalist macros now provide at least append theorems by default.

The documentation-generating macros have been enhanced.

The fty::deftypes macro now uses more aggressive theory management to speed up certification, and also has more comprehensive error checking.

The fty::deffixtype macro has better error checking.

The cases macros introduced by fty::deftypes now support an :otherwise case.

The fty::deftypes make- macros now disallow duplicated keywords.

The fty::deflist and fty::defalist macros can now tolerate already-defined predicates.

The fty::basetypes book has been filled out a bit, e.g., it now includes maybe-natp.

By default, fty::deffixtype now verifies the guards on the equivalence relations it introduces.

Quicklisp

Quicklisp can now read proxy information from the HTTP_PROXY_WITH_PORT environment variable. See also the "Using a proxy" page in books-certification. BOZO move that into Quicklisp? Blah, all this stuff always ends up duplicated everywhere.

Quicklisp now includes books for loading the uiop library and a more sensible cl-fad book. These libraries may be useful for doing file system things. The CCL-only restrictions on bordeaux-threads and hunchentoot have been dropped since these libraries seem to be working fine on modern SBCL distributions. A book for the html-template library has also been added.

The Quicklisp build should be more robust. It now checks for existing Quicklisp installations and produce a sensible error message instead of dying horribly.

Other

The getopt library now has a basic test suite.

The centaur/misc/sharedlibs code for relocating shared libraries has been extended with a test/demo script. The sharedlibs functions no longer cause errors when used on non-CCL Lisps (they simply print a message, instead.)

The template-subst tool has been expanded with some additional functions.

The profile-all and profile-ACL2 functions can now be used from within the ACL2 loop instead of only from raw Lisp.

The flag::def-doublevar-induction macro has been extended and improved.

For esim, there is a new tool for stv decomposition theorems, oracle/stv-decomp-theory-expander.lisp, and a demo of using this tool in centaur/regression/composed-stv.lisp. The documentation tables for STVs should now look nicer in the printer-friendly xdoc view.

In the 4v library, there are a few new *sexpr-rewrites*.

Minor bug-fix to avoid complaint in an aignet bind-free routine.

Added satlink::gather-benchmarks, a plugin for collecting DIMACS files that SATLINK sends to the SAT solver. You could use this to gather benchmarks for evaluating SAT solvers or for the SAT solving competitions.

In gl, fixed a bug in trace-gl-interp.

VL Changes

VL has undergone significant extensions and changes, mostly toward extending VL to support a subset of SystemVerilog. VL is intended to also still support Verilog-2005, and in many cases its Verilog-2005 support has been improved as new SystemVerilog features have been implemented. Some highlights:

VL now has a more extensive "systest" suite for checking its work against NCVerilog and VCS, and a preliminary "failtest" suite for ensuring that certain modules with bad constructs are properly rejected.
Added parsing support for many constructs such as interfaces, packages, generate statements, structs, unpacked arrays, etc. The parser functions now pass around a "parse state" object and generates warnings in a more coherent way. This results in certain speedups to its certification and allows for distinguishing the names of data types from other identifiers, which is necessary for parsing certain constructs.
More comprehensive parameter support. This involved reworking unparameterization to handle SystemVerilog data types, and adding support for richer expressions in wire ranges, etc., by reworking how constant expressions are evaluated to handle many more operators and operands of mixed sizes/types. Generate statements are also now supported to some degree.
Added support for fancier ports, e.g., ports with data types, module instances with .name and .* style connections, and interface ports.
Added support for combinational user-defined primitives, and at least basic parsing support for sequential UDPs.
Added some support for SystemVerilog packages and imports. A new "scopestack" abstraction is now widely used to provide more comprehensive handling of nested scopes (e.g., named begin/end blocks), packages, etc. There is now some support for functions defined at the global scope.
Sizing has been extended to handle unpacked arrays. The sizing code has been reorganized to be more modular, and extended to handle additional operators.
Miscellaneous improvements. The pretty-printer has been extended to handle the new SystemVerilog constructs, ansi-style ports, etc. Some transforms are more configurable, e.g., gate elimination can easily use alternate replacements for gate instances. There is better support for case statements, especially in always_comb blocks. Various operators are now supported to various degrees, e.g., ++, casting operators, $bits, streaming concatenations. The preprocessor now supports `define macros with arguments. The hierarchy tools have been greatly simplified.
Numerous organizational changes, bug fixes, and updates to existing tools and transforms to keep things working.

Besides these improvements to the core library, there have been various user interface improvements. For instance, the vl::vl-server has been entirely rewritten and is now included in the vl::kit; it allows you to view Verilog modules in a web browser. The loader has been made more user-friendly and more gracefully handles search paths, errors, etc. The vl::vl-linter has been tweaked to provide better output and to run more quickly.