|
|
|---|
|
|
|
|---|
Release notes for the ACL2 Community Books for ACL2 7.1 (May 2015)
The following is a brief summary of changes made to the community-books between the releases of ACL2 7.0 and 7.1.
The acl2-books Wiki page on Release Version Numbers gives the Git/SVN revision numbers corresponding to releases. See also note-7-1 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 7.0, so we've deleted them.
Previous Location Replacement
--------------------------------------------------------------------------------
centaur/vl/mlib/context centaur/vl/parsetree
centaur/vl/util/toposort centaur/depgraph/toposort
centaur/vl/transforms/xf-unparameterize centaur/vl/transforms/unparam/top
misc/{qi,qi-correct} centaur/ubdds/lite
oslib/logic-defs oslib/top-logic
tools/defredundant std/util/defredundant
--------------------------------------------------------------------------------
The directory
The directory
David Russinoff has contributed a new version of the rtl library:
Marijn Heule's
Matt Kaufmann and Cuong Chau have formalized the overspill property in
ACL2(r), see
The new
The new directory
The new book
The
The documentation for data-structures is now included in the manual; previously it was excluded because of name conflicts with other libraries, but these have now been resolved.
As mentioned above, the newest rtl library is now in an
The bitops library is now in a new
Renamed
The b* book has moved from
Added new print-legibly and print-compressed functions to
std/io. These can print to
There is new syntactic sugar based on define's named return values.
The new defret macro offers a more comfortable syntax for proving
theorems about return values by their name. Also, the new
The define macro now checks the arity of
Some
Added a new oslib::universal-time function.
Fixed a raw lisp bug with the definition of @9see oslib::ls), and added a regression test.
Fixed minor bugs with oslib::copy.
Bitops is now in a package. To minimize backwards incompatibility, the new
package imports a lot of stuff that you might not expect. For instance all of
the logops-definitions, and their recursive
Extended the bitops::bitops/merge book with several new 256- and 512-bit merges, merge-8-u2s, and improved its documentation.
Added nth-slice128.
The case macros from fty::defflexsum and fty::deftranssum now
require a variable, and cannot bind that variable itself, because the syntax
for doing so was too weird and unintuitive. They can now also be used to
carry out type-checks, e.g.,
The macros
The fancy viewer's jump-to box should perform better. It now suggest exact name matches first and otherwise shows results in importance order, instead of alphabetical order, which may be better when there are many matches.
The fancy viewer now features a mobile-friendly version with many features. This should greatly improve access to ACL2 documentation at parties, sporting events, and other social occasions.
Fixed a bug with
Fixed a bug with using multiple defsection extensions with the same name. Defsection now requires a non-nil symbol as the section name.
As the manual has grown substantially, some memory management measures have
been taken in
The approach to distributing Common Lisp libraries has been updated to use the new Quicklisp bundles feature. Some additional Common Lisp libraries have been added to the bundle.
The tshell library is now based on the Shellpool Common Lisp
library (via quicklisp). This may improve reliability and cross-lisp
portability for
VL and ESIM have undergone major changes, including a fork of VL. For details about these changes, see note-7-1-vl.
Ben Selfridge's leftist-trees library is now available under an MIT/X11 style license instead of the GNU General Public License.
The bounding theorems for logext in
For the tau-system, there is now a unary-- bounder in
The defsort macro has been enhanced to better support the fixtype
discipline of the fty library. In support of this, it now
requires a stricter transitivity property, i.e., the comparison function must
support unconditional transitivity, regardless of element type. (This is
typically easy to achieve by using
The Codewalker demo books have been improved to use built-in function nat-listp and weaken the hyps (state invariant) so that the state components consist of integers, not naturals.
gl now uses an improved theory for better def-gl-clause-processor event performance.
The template-subst tool now has some extended repetition capabilities.
Various other libraries have received minor cleanups.
build::cert.pl, et al. now tolerate
Errors during portcullis events (i.e.,
Various updates have been made to the Jenkins scripts to keep things up to date.
For most Lisps, build::cert.pl will now include garbage collection messages in output logs files. This may occasionally be useful when debugging performance issues.