ACL2 Seminar, 10/15/03:
The ACL2 ToDo List as of 10/13/03
 Matt Kaufmann

Abstract

I'm hoping that this seminar will help us answer the following question: How much more should we do to ACL2 before releasing ACL2 Version 2.8?

For some time I have been keeping a list of ACL2 "to do" items, the "ToDo List". Recently I've organized the ACL2 ToDo List in two ways: (1) Adding one-line summaries and (2) organizing into priority levels. This talk will discuss the list of one-line summaries, with the following goals.

The current list of one-line summaries of ToDo List items is presented below. (Details are kept elsewhere.) The one-liners are organized as follows. [The rest of this page is also available as a text-only version.]

DISCLAIMER: Many one-line summaries are rather technical in nature, and not really expected to be understandable in isolation.

MUST DO

1. Modify proof-checker type-alist command to specify use of conclusion and/or governors.
2. Eliminate some parameters all-new-flg in linear arithmetic functions.
3. Update installation.html if instructions at GCL web site aren't sufficient.
4. Update Makefile-generic with what's at AMD, including make-depend.lisp.
5. Add "make install" target that creates ACL2 executable script.
6. [Ask J.] Remove ld-redefinition-action from untouchables?
7. [J] Fix redefinition issues related to stobjs.
8. [J] Complete Robert's changes involving interaction of linear arithmetic with forward-chaining and type-set.
9. [Warren volunteers] Request build of ACL2 2.8 on MCL 5.0, Mac OS X, before release.
10. Add a new books/defexec/ directory to the distribution.
11. [Ask J.] Add :rewrite rules realpart-+ and imagpart-+.
12. Fix :doc type-spec to mention that NOT, AND, and OR can be used.
13. Fix soundness bug in packages due to incompatible symbol-package-names from different books.
14. Merge in Pete/Daron's ordinals to ACL2 when I get their sources.
15. Cause a clear warning when a bad assumption ("bad-ass") causes simplification to fail.
16. Document ER, ERROR, ILLEGAL, ERROR1, ...., and cross-link them.
17. Add acl2-books :doc topic and links to it.
18. [J] ACL2 home page organization: workshop papers vs. Books and Papers section.
19. Look at latest Debian package for ACL2. And, avoid loading TMP1.o in such.
20. Take rtl/rel1 and rtl/rel2 out of "make certify-books".
21. Update release.cmds (5) with instructions to run scripts build-linux, build-solaris, and build-ns.

VERY DESIRABLE TO DO

22. :DOC defun should explain that "governs" does not include IFs inside function calls.
23. Deal with Unix-style absolute pathnames that arise in Windows.
24. Allow more user control of evisceration during printing.
25. [J?] Allow break-rewrite stack inspection (using cw-gstack) at the top level.
26. Add "Used:" field to summary.
27. Fix make dependencies so that .acl2 file dependencies are appropriately included.
28. Cause an error if synp (syntaxp or bind-free) is applied to a let-bound variable.
29. Deal with issues involving book directories.
30. Avoid infinite loops caused when tracing functions that implement trace.
31. Add analogues of defund and defthmd, but enabling, so that redundant functions are enabled when book is included.
32. Update looking up of hyps for forward-chaining, and some :doc, to comprehend calls of equivalence relation.
33. Add guard documentation: guard proof obligations, translation of types to guards.
34. Fix mismatch in checking vs. storing :linear rules, related to ground terms.
35. [Ask J.] Fix possible bug in cw-gstack.
36. Add tutorial link on ACL2 home page pointing to our tutorials and ELM-ART.
37. Fix zp-big-n so that it's logically correct AND doesn't warn on compiling the *1* function.
38. [ChesKo may do this] Build ACL2 on CLISP/Windows.
39. [J] Fix an infinite loop in printing an error involving (@ brr-gstack).
40. Add Marktoberdorf work to the regression suite.
41. [J] Consider Bill Legato's ideas for improving fertilization.
42. Avoid allowing symbols with deceased packages to sneak in via stobjs and state globals.
43. Consider publishing timings for various lisps.
44. [J?] Revisit the Satriani hack, and/or implement :do-not-clausify hint.
45. [J?] Fix textbook solution files.
46. Allow :instructions inside :hints. This seems quite feasible, actually.
47. Print "(forced/immediate)" or "(case-split)", not just "(forced)".
48. Proof-checker issues, especially, macro commands in instructions.
49. Provide a way for users to set a default path for books.
50. Fix :pe to show actual book containing the form, and to eviscerate when necessary.
51. Make safe-mode more available, perhaps simply by advertising it.
52. [J] Fix performance issue with nu-rewriter.
53. Consider adding a bit more documentation for mfc-clause and such.
54. [Ask seminar] Fix warnings on missing compiled files when including arithmetic books.
55. [Ask J.] Reconsider when defconst should be redundant in light of redefinition.
56. [Ask J.] Deal with issue that rewrite rules can be illegal because of evaluation by translate ("constant folding").
57. Avoid leaving functions traced when WET call is aborted.

HOPE TO DO

58. Avoid the saving of strings into small images by defdoc.
59. Avoid needless WET message.
60. [J] Fix guard problems for << in finite-set-theory books.
61. Improve avoiding the printing of successive identical goals, and avoid untranslate with printing off.
62. [J?] Consider Vernon's improvements for better space and time efficiency in theory manipulation.
63. Make set-case-split-limitations apply to defun processing.
64. Add time$ so that one can time in the ACL2 loop.
65. [Ask in seminar.] Consider enabling :induction runes automatically when ":induct term" is supplied.
66. Avoid silencing of proof of :theorem specified in :use hint.
67. Give users control over the functions printed by theory warnings.
68. Disable some built-in functions or create an appropriate theory for doing so.
69. Lispworks doesn't seem to handle (good-bye) properly.
70. [Any volunteers?] Modify Allegro tracing to avoid deprecated "advise" feature.
71. Make it easy to avoid raw mode reporting of possible multiple values.
72. Show which terms are forcibly expanded during proofs by induction.
73. Modify proof-checker's DV macro to understand LOGXOR and some other macros.
74. Consider strengthening relieve-hyp to rewrite twice because of geneqv issues.
75. Consider adding more rules for defequiv to avoid proof failures for obvious thms.
76. Consider disallowing ubt-fn in definitions.
77. Improve consistency in errors caused by unnecessary defcong events.
78. Warn when :MONITORing or changing world when inside the brr wormhole.
79. Disallow invalid tracing options in Allegro.
80. Cause error or warning on loop-stopper when it doesn't apply.
81. Add ACL2 Workshop 2002 at "Submit Documents" button at http://citeseer.nj.nec.com/cs.
82. [Any volunteers?] Implement queries for skip-proofs/defaxioms in current session.
83. Warn on bad combination of forward-chaining and type-prescription rules.
84. Consider handling state like other stobjs, where guard is always augmented.
85. Use immediate-force-modep so that proof-checker's BASH does not create forcing rounds.
86. Consider efficiency improvements for hiding during Allegro-based tracing.
87. Document how hints are inherited and perhaps improve how this is done.
88. [Does Robert need this for var-fn-count?] Introduce flag functions automatically for mutual-recursion, or manually for var-fn-count.
89. Avoid odd loop involving specious simplification and elimination.
90. Modify (unsigned-byte 29) in the nu-rewriter code in order to use MCL fixnums.
91. Fix :doc bdd-algorithm as needed.
92. :Bdd hints can fail silently in a way that is confusing to the user.
93. The fmt functions drop right-square-brackets with ~& (but not ~x, e.g.).
94. Speed up failed book certifications.

MIGHT DO

95. Allow evaluation during type-set, in particular relieving of hyps.
96. Fix printing of symbols with very long names.
97. Consider doing more profiling.
98. Print nice errors when trace is called instead of trace$, etc.
99. Find a way to avoid loops, perhaps by writing appropriate :doc, caused by introduction of unnormalized terms by linear arithmetic and bind-free.
100. Fix time triples: either fix under-reporting, or come up with a clear story.
101. Make :ubt automatically untrace where appropriate.
102. Improve performance of FN-COUNT-EVG-REC.
103. Improve (pstack t) and (pstack :all) for ACL2 users (as opposed to developers).
104. Advertise break-on-error when errors are printed.
105. Improve documentation on case-split vs. force.
106. [Any volunteers?] Consider speeding up Sandip et. al's 2003 workshop contribution.
107. Add documentation showing how to use :induct hints.
108. Implement a clear test for when "make regression" has fully succeeded.
109. Perahps avoid rolling back the world for LD on certain aborts, e.g. from inside break-rewrite.
110. Improve prover output when HIDE is introduced because of constrained subroutine call.
111. Improve heuristics that avoid tail-biting.
112. Create summary page for the most common proof-checker commands.
113. Warn on recursive calls in :exec arg to mbe, at least outside defexec.
114. Make it possible to include lots of distributed books together.
115. Provide an event for reordering rules (Dave Greve says he'd find this useful.).
116. [Raise priority?] Allow user to specify a channel or file for cw.
117. Improve handling of ignored variables to avoid compiler warnings.
118. Add :DOC EFFICIENCY under :DOC PROGRAMMING, based in part on Rob's notes.
119. [J] Allow :rewrite rules that rewrite calls of NOT.
120. Write blurb for Franz web site.
121. Speed up monitoring definitions from large mutual-recursion nests.
122. Print an informational message when normalization of a defun isn't a no-op.
123. Consider rules realp-+, rationalp-+, etc., and whether or not they should be enabled.
124. [Lower priority?] Improve fixnum support in CLISP?
125. [Any volunteers?] Fix processing of user-defined documentation.
126. [Any volunteers?] Try proclaiming in other lisps (not just GCL).
127. [Any volunteers?] Extend nonrec fn warning for :rewrite rules from nonrec defs to arbitrary enabled :rewrite rules.
128. [Lower priority?] Support inlining of function calls.
129. Consider releasing Matt's pretty-printer.
130. Add proof-checker documentation, say from the tutorial.
131. Loosen requirements involving free vars for functional instantiation.
132. Improve appearance of proofs by putting generated symbols in appropriate packages.
133. [Rob is doing this.] Consider stobj-related improvements suggested by Rob, especially under-the-hood macros.
134. Improve structure of released books/ directory.
135. Remove portcullis requirement of undoing a certify-book before a corresponding include-book.
136. [Any volunteers?] Fix rtl/rel3 for nonstd, as it is not currently part of the nonstd regression suite.

FUTURE RELEASES AFTER 2.8

137. Allow :expand hints to work on :definition rules.
138. Support compiled files of *1* functions through book certification.
139. Consider namespace issues (example: built-in name int=) [probably downgrade or omit].
140. Consider binding vars with equality hyps for :forward-chaining rules, as with :rewrite rules.
141. Improve equality reasoning: strengthen it, and avoid certain loops.
142. Ignore hints for purposes of redundancy of encapsulate.
143. Consider adding to :doc defun a discussion of how ACL2 guesses measures.
144. Make it easy to set default hints like :do-not '(generalize) without interfering with hints provided by the user.
145. Consider using resolution for forward chaining and perhaps other things.
146. Improve termination proofs with built-in-clause rules for cadr etc.
147. Disallow supplying hints for the same goal more than once.
148. Maybe disallow multiple :expand hints from computed hints (already done for explicit hints).
149. [Rob?] Improve the records book(s), in particular with some new rules.
150. Improve assume-true-false to note x as a consp when (car x) or (cdr x) is non-nil.
151. Make union-equal and other functions tail-recursive, perhaps using defexec.
152. Extend match-free-error handling to more rule classes.
153. Implement minor releases.
154. Support connections with separate tools.
155. Save the proof output into a data structure that can be printed later.
156. Write a dead code tool.
157. Add a warning for :forward-chaining rules that cannot possibly fire.
158. Have LD change the package permanently, and allow defpkg in books.
159. Figure out a way to load a book's compiled file when the book has already been included.
160. Improve type-prescription system for understanding multiple-valued returns.
161. Consider adding forward-chaining conclusions to the clause.
162. Improve rewrite failure reports by :brr when a free variable is involved.
163. Consider speeding up zp.
164. [Any volunteers?] Consider sorting :doc topics in case-insensitive way.
165. Report functions responsible for case splitting, and consider speeding up preprocess-clause.
166. Improve efficiency of accumulated-persistence; maybe always leave it partially on?
167. Consider dealing with non-rewritten terms introduced by bind-free, at least in :doc.
168. Improve efficiency of some proof-checker built-in commands.
169. Allow package reincarnation.
170. Make Rob's new simplifier ready when he's ready.
171. Add more aggressive proof heuristics or at least "wizard" warnings.
172. Make match-free more flexible.
173. Allow more advanced hint control, e.g., time limits.
174. Connect user-specified backchain limit with bdd package.
175. Consider incorporating books/arithmetic-2 (or arithmetic-4??) into nonstd.
176. Speed up irrelevant formal checking.
177. Add user-defined memoization to ACL2.
178. Allow stobj names in macros, not to be used as stobjs.
179. [Lower priority?] Extend/improve local-stobjs by introducing local-stores.
180. Consider loading acl2r.lisp in acl2.lisp to avoid potential problems.
181. [Any volunteers?] Check that "make" is GNU make.
182. Develop FAQ.
183. Allow macroexpansion of arguments to a macro, to support inside-out macroexpansion.
184. Implement ACL2-modified trace/untrace for clisp as exist already for GCL and Allegro.

LONG-TERM

185. Make defevaluator executable.
186. Consider default of t for :otf-flg.
187. Consider avoiding forcing in certain cases involving linear arithmetic.
188. Allow user-defined pattern-matching for one-way unification.
189. Avoid problematic interaction between :brr and proof-checker.
190. For certify-book, allow local incompatibility check before proessing events.
191. Add some form of AC matching, or maybe just commutative matching.
192. Allow for execution of constrained functions.
193. Provide direct hooks into saving the system.
194. Further ideas for output inhibition: certification and hints.
195. Allow in ACL2 easy user-settability of print-length, print-downcase, etc.
196. Add hash tables to ACL2.
197. Write pattern-matching macro for ACL2.
198. Improve theory handling in proof-checker.
199. Enhance demos by using tools (e.g., proof trees).
200. Move documentation out of sources, etc.
201. [Any volunteers?] Double-check speed of Windows printing.
202. Implement appending to files by print routines.
203. Mechanize checks that built-in defaxioms follow from the logic.
204. Extend accumulated-persistence to meta and linear rules.
205. Extract singly-recursive functions from mutual-recursion nests.
206. Improve performance perhaps by using a vector for multiple values instead of a list.
207. Implement a defalias event or :rule-classes :alias, for rule sharing.
208. Consider allowing include-book in (encapsulate () ...).
209. Check uses of ~x vs. ~p in fmt strings.
210. Check that make handles calculus outline files properly.
211. Check for use of ~ilc where ~il is better.
212. Consider defun-std and *1* issue for nonstd.
213. Check that file protections are OK for distribution.
214. Bunches of remaining non-standard analysis issues.
215. Allow conjunctive triggers for :forward-chaining rules.
216. Implement hash-cons.
217. Revisit congruence relations with hypotheses or third argument.
218. Consider making in-local-flg untouchable, or the like.
219. Maintain notion of ACL2 home directory even for Windows.
220. Support user-directed generalization.
221. Consider a particular improvement to search-type-alist.