|
|
|---|
|
|
|
|---|
Prioritizing: When to Make Changes
It may be tempting to enhance ACL2 whenever an intriguing idea comes along for making an improvement. There is something to be said for doing so: the immediate motivation may make the work fun and lead to good results.
SUMMARY THAT SHOULD SUFFICE: Fix bugs, prioritize what will actually be used, and beware of massive regression failures. Changes can be extremely valuable, and can also be substantially more work than predicted.
But there can be drawbacks to taking on every opportunity to make an improvement. Heuristic improvements can be very difficult to work out without breaking, or slowing down, the regression suite. A change may inadvertently break something. Changes may be much more time-consuming than expected, and may take time away from other more important changes to be made. Below we explore some aspects of prioritizing development tasks.
Bug fixes are generally a priority, especially (of course) if they impact soundness. Enough said?
It has been observed that many ideas for improvements that may seem helpful are actually not very helpful to anyone actually using ACL2. It is therefore usually a good idea to prioritize changes that either accommodate specific requests from a user, or at the least can be seen as having significant positive impact on users. It is very easy to think a new feature will be useful, but with the result that it's rarely or ever used, yet it complicates the source base. A feature you consider might be close to being useful, but by waiting for a specific request, you can perhaps get substantially more insight about what would truly be useful, thus refining your initial idea for that feature.
The ACL2 community-books provide a well-established set of
libraries, as well as a useful set of regression tests. Changes to ACL2 may
cause some failures when certifying these books. Often these are easy to fix,
for example by modifying theory hints or by changing subgoal
names on hints. Changes may also impact ACL2(p) or ACL2(r), which are
probably tested significantly less frequently. More worrisome is the
potential impact on private repositories, for example proprietary (not public)
sets of books at companies. There can also be slowdowns, which can be
debugged by running the tool
NEXT SECTION: developers-guide-evaluation