ACL2 Sedan Release Notes

1 ACL2s 1.2.0.0 (with ACL2 8.0)

Release Date : 2018-01-08 Mon

1.1 New Features

  • Cgen now provides support for interactive disproving via fixers.
  • TODO

1.2 Bug Fixes and miscellaneous improvements

1.3 System-level Changes and Notes

  • Support for 32-bit platforms dropped.

1.4 Changes to Existing Features

1.5 Known Issues

1.6 Major topic documentation links

2 ACL2s 1.1.8.0 (with ACL2 7.1)

Release Date: 2016-01-10 Sun

2.1 New Features

  • Cgen now provides first class support for the membership relation, in a similar fashion to the support it provides for equality. For exmaple, if Cgen sees a (member-equal x L), then it infers that x has the type (enum L) and appropriately samples it during its test-data generation phase.
  • Cgen now collects statistics across its test-runs for each of the hypotheses of the conjecture under test. This gives an idea of which hypotheses are more easily satisfied by Cgen testdata.
  • It is possible to attach additional constraints to types that helps Cgen refine (narrow down) its sampling space for variables of that type. The user can use defdata-attach to specify such constraint-rules as follows: 
    (defdata-attach imemory ;type-name
  :constraint (mget a x) ;x is the variable of this type
  :constraint-variable x
  :rule (implies (and (natp a) ;additional hyps
                      (instp x.a)
                      (imemoryp x1))
                 (equal x (mset a x.a x1))) ;refine
  :meta-precondition (or (variablep a)
                         (fquotep a))
  :match-type :subterm-match)

2.2 Bug Fixes and miscellaneous improvements

  • Improved runtime reporting in defunc.
  • Improved defunc support in 'Programming' session mode and for program-mode functions.
  • The output message for body-contract failure did not show the failing body-contract to be blamed for defunc bodies with let. The situation has been improved.
  • Printed counterexamples/witnesses are always checked for soundness.
  • The incremental search-strategy (for counterexamples) has been heuristically tuned for improved performance.
  • defdata-attach constraint rules are automatically generated for user-defined maps and records that expand/refine variables of these types triggered by hypotheses about map/record fields. This significantly improves Cgen's counterexample search for conjectures involving these types when using the incremental search-strategy.

2.3 System-level Changes and Notes

  • On Windows it was required that ACL2s be installed in a directory without spaces in it; this requirement has been removed.
  • The makefile/certification scripts within each plugin directory are self-contained. It is possible to recertify the ACL2s system books from within the eclipse/plugins directory via the following commands (on Windows you need Cygwin installed) : 
    cd <your-eclipse>/plugins/acl2s_modes<version-number>
export ACL2=<your-eclipse>/plugins/acl2_image<bla>/run_acl2[.exe]
./certify-all-acl2s-system-books.sh
  • The Linux ACL2 images might not work on Linux machines with glibc version older than 2.15.
  • ACL2 image on Windows uses CCL 1.11 (32bit); the 32bit executable works fine on both 32bit and 64bit Windows platforms.
  • Only the following directories under books are pre-certified (and pre-compiled) in the distributed ACL2 images: 
    arithmetic arithmetic-3 arithmetic-5 ihs std xdoc tools misc data-structures
acl2s add-ons coi hacking make-event meta ordinals sorting textbook tools

    To build/certify other books, either use the perl script <acl2image>;/books/build/cert.pl from the command line, or use the ACL2s Certify-book command/button to individually certify each book (one at a time and in the right order).

2.4 Changes to Existing Features

  • Nested testable contexts (e.g. nested thm, defthm etc) are no longer supported. This makes cgen::flush irrelevant.
  • Given a type foo, the enumerators for foo are nth-foo and nth-foo/acc. By default the enumerators attached to them are nth-foo-builtin and nth-foo/acc-builtin, respectively. To use other enumerators, use the macro defdata-attach.

2.5 Known Issues

  • For certain Windows installations with a lot of programs and updates installed, the ACL2 image will not start giving the following reason: 
    Can't allocate required TLS indexes.
First available index value was 31 ..

    This is a known issue with CCL (CLozure Common Lisp) on Windows. In the past we used SBCL, but for obscure reasons ACL2 book certification fails for recent SBCL implementations. If you run into the TLS issue, see the FAQ.

2.6 Major topic documentation links

3 ACL2s 1.1.7.0 (with ACL2 7.0)

Release Date: 2015-02-02 Mon

3.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.

3.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.

3.3 Major topic documentation links

4 ACL2s 1.1.6.0 (with ACL2 6.5)

Release Date: 2014-09-24 Wed

4.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.

4.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.

4.3 Bug Fixes

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

4.4 Major topic documentation links

Author: harshrc <harshrc@ccs.neu.edu>

Date: 2018-01-08 06:45:49 EST

HTML generated by org-mode 6.30c in emacs 23