Optimizing-build-time
How to use critpath.pl to profile your build, so that you can
focus your efforts on speeding up the most critical parts.
Alongside cert.pl is another script, critpath.pl, that
can be used to analyze the certification times for your files. When you are
dealing with a large collection of ACL2 books, this can be a useful tool for
seeing where to speed up your build.
Before using critpath.pl, you must tell cert.pl that you want it
to record certification times. This is done by setting the $TIME_CERT
environment variable. For instance, you might add the following to your
.bashrc or equivalent:
export TIME_CERT=yes
After setting this variable, you will need to recertify your books.
When cert.pl sees that $TIME_CERT is set, it writes out additional
.cert.time files that record how long each book took to certify. The
critpath.pl script then correlates these files with the dependencies among
your books to give you a report.
For instance, here is a report for the arithmetic-5/top book, circa
October 2013.
$ cd arithmetic-5
$ critpath.pl top.cert
Critical Path
File Cumulative Time Speedup Remove
top.cert 2.0 min 2.0 sec 2.0 sec 2.0 min
floor-mod/top.cert 2.0 min 1.8 sec 1.8 sec 1.7 min
floor-mod/logand.cert 1.9 min 33.7 sec 33.7 sec 37.0 sec
floor-mod/logand-helper.cert 1.4 min 7.1 sec 7.1 sec 7.1 sec
floor-mod/more-floor-mod.cert 1.2 min 16.7 sec 15.1 sec 15.1 sec
floor-mod/floor-mod.cert 58.1 sec 19.9 sec 19.9 sec 30.8 sec
...
The critical path is the longest chain of books in an unrealistically ideal
build environment with infinite CPUs to draw upon. The report shows what books
comprise the critical path, and how long each of them takes. It also shows
you:
- The speedup time for each book. This measures how much the critical
path could be reduced by speeding up the book, without affecting its
dependencies. A book with a large speedup time may be good candidate for
new hints to make proofs faster.
- The remove time for each book. This measures how much your build
would speed up if you didn't need to build this book at all. The remove
time should always exceed the speedup time. In some cases, it may be much
larger, since by removing a book we may also avoid needing to build some of the
books it depends on.
While the very simple usage shown above is often sufficient, the
critpath.pl script has a number of other options that may occasionally be
useful. See critpath.pl --help for details.
