ACL2 Sedan Release Notes

1 ACL2s (with ACL2 7.0)

Release Date: [2015-02-02 Mon]

1.1 Changes to Existing Features

  • Every ACL2s session mode now starts in its respective package, except Compatible mode which is in ACL2 package.
  • API functions for Defdata, Cgen, and the defdata type namespace are now in the ACL2S package.
  • ACL2s defaults/parameters and defdata language keywords are package agnostic.
  • Defdata/Sig enhancements and restrictions:
    • Fixed bug in sig to take into account signatures with more than one type variable.
    • Singleton types handled now by using (lambda (x) (equal x constant)) as the predicate name.
    • If polymorphic type expression to be matched is a variable i.e :a, we skip.
    • When finding matches in the type table, we skip over types that do not have non-empty prettyified-def entry
  • Base-theory.lisp builds on std library and sets up polymorphic theory support (automated instantiation of generic type theorems) for a wide variety of list and alist functions.
  • Most ACL2s session modes provide base-theory (see above), although some might not give direct access to it via package isolation.

1.2 Bug Fixes

  • Numerous bug fixes were made in Cgen and Defdata and improved error messages.
  • Fixed bug in CCG to get it to work in encapsulate/include-book contexts.

1.3 Major topic documentation links

2 ACL2s (with ACL2 6.5)

Release Date: [2014-09-24 Wed]

2.1 Changes to Existing Features

  • Cgen has been refactored to be usable programmatically. In particular, the function prove/cgen is provided as the main API to Cgen/testing. In fact, test? has been reimplemented as a user of prove/cgen. See :doc prove/cgen.
  • Cgen/testing is disabled in DEFUN event contexts.
  • Dest-elim for records and maps is now more generally implemented using computed override-hints (earlier we had a Cgen-specific approach).
  • A new parameter print-cgen-summary controls summary output in test? and subgoal-timeout has been replaced with the cgen-timeout parameter. These can be get/set using acl2s-defaults – see :doc acl2s-defaults.
  • Added cgen:flush to flush the Cgen globals left in an ill-formed state due to interrupts. See :doc cgen::flush.
  • Cgen now prints evalable counterexamples/witnesses (that can be copied into a let* binding).
  • The defdata-testing macro has been replaced by the more general defdata-attach, which can be used to change/add type metadata associated with each type stored via register-type and defdata in the table type-metadata-table.
  • Defdata was reimplemented as a framework and has been moved out of Cgen to reflect its more independent status. See the essay at bottom of defdata/defdata-core.lisp
  • Heuristic changes were made to nth-all and other standard base enumerators (to tweak the distribution of sampled testdata).
  • ACL2s session modes use better theory reasoning support via the std libraries.
  • Polymorphic signatures were added for relevant base functions in all of the modes supported by ACL2s.

2.2 New Features

Parametric Polymorphism support in ACL2s (Defdata)
Defdata enforces the following:
  1. Every new defdata type is instantiated for every polymorphic signature (specified via sig) that matches (one of its argument types).
  2. Every new polymorphic signature is appropriately instantiated for all defdata types in the current world.

See Data Definitions in the ACL2 Sedan for more information.

Tau Characterization of defdata types
For a significant subset of defdata definitions, we have a complete Tau characterization. This means that if Tau-System is complete over the type reasoning theory, then adding a type to the current theory via defdata maintains this completeness. See Data Definitions in the ACL2 Sedan for more information.
Defdata extensions
Numerous improvements to subtyping information, new base types, and an alistof combinator was added.

2.3 Bug Fixes

  • Interrupt functionality in ACL2s has been made more robust.
  • Numerous bug fixes were made in Cgen and Defdata.

2.4 Major topic documentation links

Author: harshrc

Created: 2015-02-03 Tue 11:52

Emacs 23.4.1 (Org mode 8.2.5h)