ACL2 Directions

                              ACL2 Workshop 2004
                                 Matt Kaufmann
                                    J Moore

Here are some potential items for discussion.

TABLE OF CONTENTS:

1. COLLECTING CONTRIBUTED BOOKS
2. WHAT'S NEW
   A. New release, and release notes
   B. Incremental releases
3. CURRENT STATE OF "TO DO" LIST
4. NEXT WORKSHOP

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1. COLLECTING CONTRIBUTED BOOKS
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

The ACL2 distribution comes with a collection of certifiable books (in the
books/ directory), and one can also download contributions to the workshops.

We propose collecting other certifiable books from the community and attempting
to maintain them over future releases.  This benefits the developers by
providing more test cases, and it benefits users because the developers will
attempt to keep the books up-to-date for subsequent ACL2 releases.

We need to decide, then, on a directory structure.  Here is one possible plan.

We can send out an email to acl2@lists.cc.utexas.edu with an initial subset of
the distributed books that we believe are in general use.  ACL2 users would be
invited to reply to that email, pointing out any books missing from that
collection.

All remaining books would be placed in a new books/contrib/ directory,
including the workshops, which would go into:

books/contrib/workshop-1999/
books/contrib/workshop-2000/
books/contrib/workshop-2002/
books/contrib/workshop-2003/
books/contrib/workshop-2004/

The other subdirectories of contrib might be organized by topic.  There would
also be some sort of master index:  a text file giving directories for
contributions.  For example, if John Smith contributes a book
on factorial called factorial.lisp, it might go into
books/contrib/arithmetic/john.smith/factorial.lisp
and there might be several index entries:

factorial: contrib/arithmetic/john.smith/factorial.lisp
Smith, John: contrib/arithmetic/john.smith/factorial.lisp
binomial coefficient: contrib/arithmetic/john.smith/factorial.lisp

The ACL2 installation page would provide links gzipped tar files supplied upon
request.  For example, there might be one for books/contrib/workshop-*/, one
for books/contrib/arithmetic/, and so on.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2. WHAT'S NEW
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   A. New release, and release notes
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

We have returned to a single documentation topic for release notes, for easier
searches.  See for example the documentation topic NOTE-2-9.  There are several
soundness bug fixes and other significant improvements in ACL2 Version 2.9, so
we recommend that you update to it soon.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   B. Incremental releases
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Pretty soon we will put out the first incremental release, 2.9.1.  We expect
that an incremental release X.Y.Z will require recertification of all books by
default, but we expect to provide a mecahnism for allowing books certified with
the previous major release X.Y, or with incremental releases X.Y.W for W<Z, to
be used at one's own risk.  Incremental releases X.Y.Z will differ from major
releases X.Y in at least the following ways.

a.  An incremental release will leave the ACL2 web space largely unchanged,
other than making available a gzipped tar file for the new release and for
associated books (currently the workshop books).

b.  Incremental releases will generally only be tested thoroughly with one or
two underlying Lisps.

c.  Because incremental releases are pretty easy to make, we will attempt to
accommodate requests for them on short notice.  So you may see them rather
frequently, but unlike major releases, we do not expect users to update their
local ACL2 whenever there is an incremental release.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3. CURRENT STATE OF "TO DO" LIST
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

The following list contains (overly?) brief summaries of potential ACL2 tasks
as of November 10, 2004.  It is intended to provide some idea of the nature of
improvements that may be forthcoming.  We hope that it will both inspire
additional ideas for improvement and, less importantly and somewhat
paradoxically, provide a context for our reluctance to take on difficult tasks
without reasonably clear benefit.

Some items are labeled "[VOLUNTEER?]" to identify tasks that someone besides
the developers, perhaps a doctoral student, might reasonably take on (in which
case we could send a more detailed description of the task).

The task list is divided into groups, very roughly from most to least likely to
be completed soon.  We do not plan to discuss any of these items in particular,
but people are welcome to ask about them.

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Fix apparent bug in which goal is attacked by a computed hint.
Support alpha releases.
Rework :dir :system to work with downloaded images.
Proof-checker issues, especially, macro commands in instructions.
Revisit the Satriani hack, and/or implement :do-not-clausify hint.
Extend :pl, or add an analogue, for showing :forward-chaining rules.
Return a non-zero error code when "make regression" fails.
Perhaps allow references to macros in theory expressions.
Fix make clean.
Fix linkup business with nonstd and sqrt.
Consider developing a systematic way to maintain *acl2-exports*.
Allow user-settability of printing-related globals inside the ACL2 loop.
Consider supporting :dir for LD.
Allow break-rewrite stack inspection (using cw-gstack) at the top level.
Investigate seemingly slower translation in one case by GCL.
Eliminate del and do some related mods wrt. delete and remove.
Defeat verify-termination for functions that should not be executed in the
  logic.
Fix missing report of a rule used in rewriting.
Consider improving documentation for SET-DEFAULT-HINTS.
Complete collection of 2004 workshop contributions.
Consider improving congruence handling.
Look at ACL2 Workshop 2004 papers that advocate ACL2 changes.
Perhaps investigate a consequence of a change made back in 2.7.
Add Marktoberdorf work to the regression suite.
Flesh out Wiki article.
Automatically declare encapsulated functions to be non-executable.
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Consider issuing a warning to consider disabling an executable-counterpart when
  HIDE is introduced for aborted evaluations.
Build in compound recognizer rule for natp (perhaps posp too).
Possible issue in interaction of functional instantiation with defevaluator.
Figure out if the inclusion books/nonstd/sqrt is appropriate (rather than
  books/sqrt).
Consider eliminating gcl-patch.lisp from all-files.txt.
Improve rewrite and/or show-rewrites in proof-checker to deal with syntaxp.
Consider skipping THM in program mode.
Consider using sys-proclaim.lsp to improve GCL performance.
Add documentation for the-error.
Remove RAG comments from ACL2 sources.
Improve documentation on "govern" vs. "rule" for induction, termination.
Document the use of Makefiles for book certification.
Maybe extend use of the double-whammy type-set heuristic, or enable forcing in
  type-alist-clause.
Improve Makefile support for dependencies.
Add interfaces to useful Lisp routines.
[VOLUNTEER?] Make it possible to include lots of distributed books together.
Look into supporting ACL2 builds on SBCL.
Stobjs don't need to create one-element array fields for other than fixnums.
Deal differently with THE for induction and recursion (termination).
Make the ACL2 home page less discouraging.
Extend :doc rewrite with some email I sent to acl2-help.
Improve documentation for how to give hints in a mutual-recursion.
Cause a clear warning when a bad assumption ("bad-ass") causes simplification
  to fail.
ACL2 home page organization: workshop papers vs. Books and Papers section.
Fix printing of "simple" by preprocess-clause.
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Allow :monitor condition to consider the name of the current goal.
Consider making set-guard-checking an embedded-event-form.
Improve error message for non-embedded-event-forms.
Fix raw-arity calculation for defstobj -- actually for interface-er?
Add example to :DOC IO.
[VOLUNTEER?] Fix pathname issues on Windows.
Add "Used:" field to summary.
Cause an error if synp (syntaxp or bind-free) is applied to a let-bound
  variable.
Deal with issues involving book directories, including absolute pathnames in
  certificate files.
Avoid infinite loops caused when tracing functions that implement trace.
Update looking up of hyps for forward-chaining, and some :doc, to comprehend
  calls of equivalence relation.
Add guard documentation: guard proof obligations, translation of types to
  guards.
Avoid "normalizing" ground terms.
Fix possible bug in cw-gstack.
Add tutorial link on ACL2 home page pointing to our tutorials and ELM-ART.
Avoid allowing symbols with deceased packages to sneak in via stobjs and state
  globals.
Fix textbook solution files.
Allow :instructions inside :hints.  This seems quite feasible, actually.
Print "(forced/immediate)" or "(case-split)", not just "(forced)".
Improve :pe to print a more appropriate amount of information.
Make safe-mode more available, perhaps simply by advertising it.
Fix performance issue with nu-rewriter.
Consider adding a bit more documentation for mfc-clause and such.
Fix warnings on missing compiled files when including arithmetic books.
Reconsider when defconst should be redundant in light of redefinition.
Deal with issue that rewrite rules can be illegal because of evaluation by
  translate ("constant folding").
Deal with problematic interactions between WET and tracing.
Fix typos in "Precise" paper.
Consider non-exec identity function to defeat signature checking.
Consider adding a new functional instantiation example.
Avoid bogus warning about replacing a doc string.
Improve skip-proofs warning from include-book to list event names.
[VOLUNTEER?] Allow user to specify a channel or file for cw.
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Eliminate compiler warnings for unused variables from mbt and mbe.
Make '' print in emacs info as '' and not as ".
Look into gprof profiling with GCL.
[VOLUNTEER?] Update nonstd stuff to include recent additions, in particular
  ordinals and arithmetic.
Make sure that we always consult default hints when appropriate.
Add documentation example showing the use of macros to schematize functions.
Avoid needless WET message.
Fix guard problems for << in finite-set-theory books.
Improve avoiding the printing of successive identical goals, and avoid
  untranslate with printing off.
Consider Vernon's improvements for better space and time efficiency in theory
  manipulation.
Make set-case-split-limitations apply to defun processing.
Add time$ so that one can time in the ACL2 loop.
Consider enabling :induction runes automatically when ":induct term" is
  supplied.
Avoid silencing of proof of :theorem specified in :use hint.
Give users control over the functions printed by theory warnings.
Disable some built-in functions or create an appropriate theory for doing so.
[VOLUNTEER?] Modify Allegro tracing to avoid deprecated "advise" feature.
Show which terms are forcibly expanded during proofs by induction.
Improve proof-checker documentation on truncated addresses and hypotheses.
Consider strengthening relieve-hyp to rewrite twice because of geneqv issues.
Consider adding more rules for defequiv to avoid proof failures for obvious
  thms.
Consider disallowing ubt-fn in definitions.
Improve consistency in errors caused by unnecessary defcong events.
Warn when :MONITORing or changing world when inside the brr wormhole.
[VOLUNTEER?] Disallow invalid tracing options in Allegro.
[VOLUNTEER?] Cause error or warning on loop-stopper when it doesn't apply.
Add ACL2 Workshop 2002 at "Submit Documents" button at
  http://citeseer.nj.nec.com/cs.
[VOLUNTEER?] Implement queries for skip-proofs/defaxioms in current session.
Warn on bad combination of forward-chaining and type-prescription rules.
Consider handling state like other stobjs, where guard is always augmented.
Use immediate-force-modep so that proof-checker's BASH does not create forcing
  rounds.
Consider efficiency improvements for hiding during Allegro-based tracing.
Document how hints are inherited and perhaps improve how this is done.
[VOLUNTEER?] [Does Robert need this for var-fn-count?] Introduce flag functions
  automatically for mutual-recursion, or manually for var-fn-count.
Avoid odd loop involving specious simplification and elimination.
Fix :doc bdd-algorithm as needed.
:Bdd hints can fail silently in a way that is confusing to the user.
The fmt functions drop right-square-brackets with ~& (but not ~x, e.g.).
Speed up failed book certifications.
Consider using macrolet in oneify-cltl-code.
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Allow relations to be noted as well-founded based on other well-founded
  relations, not nececessarily o<.
Modify include-book for raw mode to evaluate portcullis of book.
Puffing an uncertified include-book of an empty book causes an error.
Remove t-stack component of the state.
Try to get control-c from proof-checker to put you back in proof-checker.
Allow evaluation during type-set, in particular relieving of hyps.
Fix printing of symbols with very long names.
[VOLUNTEER?] Consider doing more profiling.
Print nice errors when trace is called instead of trace$, etc.
Consider dealing with non-rewritten terms from linear arithmetic and bind-free.
Fix time triples:  either fix under-reporting, or come up with a clear story.
Make :ubt automatically untrace where appropriate.
Improve performance of FN-COUNT-EVG-REC.
Improve (pstack t) and (pstack :all) for ACL2 users (as opposed to developers).
Advertise break-on-error when errors are printed.
Improve documentation on case-split vs. force.
[VOLUNTEER?] Consider speeding up Sandip et. al's 2003 workshop contribution.
Add documentation showing how to use :induct hints.
Perhaps avoid rolling back the world for LD on certain aborts, e.g. from inside
  break-rewrite.
Improve prover output when HIDE is introduced because of constrained subroutine
  call.
Improve heuristics that avoid tail-biting.
Create summary page for the most common proof-checker commands.
Warn on recursive calls in :exec arg to mbe, at least outside defexec.
Provide an event for reordering rules.
Improve handling of ignored variables to avoid compiler warnings.
Consider allowing :use and :cases hints together.
Add :DOC EFFICIENCY under :DOC PROGRAMMING.
Allow :rewrite rules that rewrite calls of NOT.
Write blurb for Franz web site.
Speed up monitoring definitions from large mutual-recursion nests.
Print an informational message when normalization of a defun isn't a no-op, and
  perhaps eliminate normalization by default.
Consider rules realp-+, rationalp-+, etc., and whether or not they should be
  enabled.
[VOLUNTEER?] Fix processing of user-defined documentation.
[VOLUNTEER?] Try proclaiming in other lisps (not just GCL and OpenMCL).
[VOLUNTEER?] Extend nonrec fn warning for :rewrite rules from nonrec defs to
  arbitrary enabled :rewrite rules.
Consider releasing Matt's pretty-printer.
Add proof-checker documentation, say from the tutorial.
Loosen requirements involving free vars for functional instantiation.
[VOLUNTEER?] Improve appearance of proofs by putting generated symbols in
  appropriate packages.
Consider stobj-related improvements, especially under-the-hood macros.
Improve structure of released books/ directory.
Remove portcullis requirement of undoing a certify-book before a corresponding
  include-book.
[VOLUNTEER?] Fix rtl/rel4 for nonstd, as it is not currently part of the nonstd
  regression suite.
[VOLUNTEER?] Save the proof output into a data structure that can be printed
  later.
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
[VOLUNTEER?] Look into possible efficiency improvements.
Recognize redundant defdoc events, and perhaps replace deflabel with defdoc in
  sources.
Add a new books/defexec/ directory to the distribution.
Eliminate irrelevant-formals error, or change message, when due to
  non-termination.
Allow proof-checker REWRITE command to relieve some hyps and not others.
Add analogues of defund and defthmd, but enabling, so that redundant functions
  are enabled when book is included.
Consider whether we still need the fnstack heuristic.
Consider improving tracking of congruence rules.
Allow two passes of rewrite for relieve-hyp, because of congruence reasoning.
Document walkabout.
Consider using mbe to make executables tail-recursive.
Does redefinition of a function to a macro or vice-versa work well enough?
Figure out a way to allow acl2-defaults-table events for local events.
Time Windows vs. Linux.
"Guard" warning doesn't respect include-book.
Add hints for non-linear arithmetic.
Consider ideas for improving fertilization.
[VOLUNTEER?] Allow :expand hints to work on :definition rules.
[VOLUNTEER?] Support compiled files of *1* functions through certification,
  and/or make COMP an embedded event form.
Consider binding vars with equality hyps for :forward-chaining rules, as with
  :rewrite rules.
Improve equality reasoning:  strengthen it, and avoid certain loops.
Ignore hints for purposes of redundancy of encapsulate.
Consider adding to :doc defun a discussion of how ACL2 guesses measures.
Make it easy to set default hints like :do-not '(generalize) without
  interfering with hints provided by the user.
Consider using resolution for forward chaining and perhaps other purposes.
Consider getting rid of preprocess-clause.
Improve termination proofs with built-in-clause rules for cadr etc.
Improve the records book(s), in particular with some new rules.
Improve assume-true-false to note x as a consp when (car x) or (cdr x) is
  non-nil.
Extend match-free-error handling to more rule classes.
Support connections with separate tools.
[VOLUNTEER?] Write a dead code tool.
Add a warning for :forward-chaining rules that cannot possibly fire.
Have LD change the package permanently, and allow defpkg in books.
Figure out a way to load a book's compiled file when the book has already been
  included.
Improve type-prescription system for understanding multiple-valued returns.
Consider adding forward-chaining conclusions to the clause.
Improve rewrite failure reports by :brr when a free variable is involved.
[VOLUNTEER?] Consider sorting :doc topics in case-insensitive way.
Report functions responsible for case splitting, and consider speeding up
  preprocess-clause.
Improve efficiency of accumulated-persistence; maybe always leave it partially
  on?
Improve efficiency of some proof-checker built-in commands.
Allow package reincarnation and fix space problems.
Make Rob Sumners's new simplifier ready when he's ready.
Add more aggressive proof heuristics or at least "wizard" warnings.
Connect user-specified backchain limit with bdd package.
Speed up irrelevant formal checking.
[VOLUNTEER?] Add user-defined memoization to ACL2.
Allow stobj names in macros, not to be used as stobjs.
Consider loading acl2r.lisp in acl2.lisp to avoid potential problems.
[VOLUNTEER?] Develop FAQ.
Allow macroexpansion of arguments to a macro, to support inside-out
  macroexpansion.
[VOLUNTEER?] Support inlining of function calls.
Consider outside-in rewriting.
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Very few of the remainder of these are likely ever to be done.
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
[VOLUNTEER?] Implement ACL2-modified trace/untrace for clisp as exist already
  for GCL, Allegro, and OpenMCL.
Consider namespace issues (example: built-in name int=).
Consider causing an error rather than exiting proof-checker when the command is
  nil.
Consider type inference of Pavel Curtis?
Consider adding pattern matching.
Consider heuristics for making rules :once rules instead of :all rules.
[VOLUNTEER?] Allow execution of "non-executable" functions.
Consider default of t for :otf-flg.
Consider avoiding forcing in certain cases involving linear arithmetic.
Allow user-defined pattern-matching for one-way unification.
For certify-book, allow local incompatibility check before processing events.
Add some form of AC matching, or maybe just commutative matching.
Provide direct hooks into saving the system.
Further ideas for output inhibition:  certification and hints.
Add hash tables to ACL2.
[VOLUNTEER?] Write pattern-matching macro for ACL2 definitions.
Improve theory handling in proof-checker.
Enhance demos by using tools (e.g., proof trees).
[VOLUNTEER?] Move documentation out of sources, etc.
[VOLUNTEER?] Double-check speed of Windows printing.
Implement appending to files by print routines.
Mechanize checks that built-in defaxioms follow from the logic.
Extend accumulated-persistence to meta and linear rules.
Extract singly-recursive functions from mutual-recursion nests.
Improve performance perhaps by using a vector for multiple values instead of a
  list.
Implement a defalias event or :rule-classes :alias, for rule sharing.
Consider allowing include-book in (encapsulate () ...).
Check uses of ~x vs. ~p in fmt strings.
Check for use of ~ilc where ~il is better.
Consider defun-std and *1* issue for nonstd.
Bunches of remaining non-standard analysis issues.
Allow conjunctive triggers for :forward-chaining rules.
Implement hash-cons.
Consider making in-local-flg untouchable in some manner.
Maintain notion of ACL2 home directory even for Windows.
Support user-directed generalization.
Consider a particular improvement to search-type-alist.
Implement :match-free for :meta rules.
Consider if there are remaining problems with revert-world-on-error and
  cloaked-set-w!.
Improve fixnum support in CLISP?
Speed up developer builds of documentation.
Make match-free more flexible (finer control).
[VOLUNTEER?] Allow more advanced hint control, e.g., time limits.
Extend/improve local-stobjs by introducing local-stores.
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
4. NEXT WORKSHOP
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Pete Manolios and Matt Wilding will be the co-chairs for the next ACL2
workshop.  (Thanks, Pete and Matt!)

We can discuss time, place, co-location with which conference, possibility of
parallel sessions or 3 days, and so on.