Improve-book
Suggest improvements for a book.
General Form:
(improve-book bookname
&key
:dir ; default :cbd
:print ; default :brief
)
Inputs:
bookname — (required)
The name of the book to improve, with or without the .lisp extension.
:dir — default :cbd
The directory of the book, where :cbd indicates the cbd.
:print — default :brief
How much to print: nil, :brief, t, or :verbose.
Description:
Improve-book tries many things to improve a book and its contents. It prints suggestions for the user to consider, but does not actually change the book.
To apply improve-book to some book FOO, start ACL2 in the directory that contains FOO. The ACL2 session should contain as few events as possible. FOO may need to be certified so that improve-book can load its portcullis commands. Then do:
(include-book "kestrel/helpers/improve-book" :dir :system)
(improve-book "FOO")
Improvements at the book level include including dropping include-books and local events.
Improvements to defthms include dropping :hints, dropping or weaking hypotheses, and disabling slow rules.
Improvements to defuns include various things checked by our Linter tool.
Support for additional kinds of events, such as define, mutual-recursion, and nested events, is in-progress.
Note that all suggestions made by improve-book are independent. There is no guarantee that multiple suggested changes can be made together.
Subtopics
- Speed-up-event
- Suggest ways to speed up an event.
- Improve-books
- Suggest improvements for all books in a directory, but not in subdirectories.
- Improve-books-in-subtree
- Suggest improvements for all books in a directory, including subdirectories.
