Branch: refs/heads/master
Home:
https://github.com/acl2/acl2
Commit: 828e96eec69736fa3b9d9fcd282936d36d69445d
https://github.com/acl2/acl2/commit/828e96eec69736fa3b9d9fcd282936d36d69445d
Author: Matt Kaufmann <
kauf...@Matts-MBP.attlocal.net>
Date: 2015-11-26 (Thu, 26 Nov 2015)
Changed paths:
M books/system/doc/acl2-doc.lisp
M books/xdoc/top.lisp
M doc.lisp
M other-events.lisp
Log Message:
-----------
Made efficiency improvement for certify-book; fixed bad call of with-guard-checking-error-triple.
Quoting :doc note-7-2:
[Certify-book] is faster in some cases; for example, we found the
time required to certify a book whose only event is (include-book
"centaur/gl/gl" :dir :system) was reduced from 57 seconds to 10
seconds. (Implementation note: The change was to avoid installing
worlds in function defpkg-items. That had probably been done in
order to speed up calls of simple-translate-and-eval in
defpkg-items-rec, but that speed-up seems to be dwarfed by the
expense of extend-world1 in such cases.)
Also, changed call of with-guard-checking-error-triple to
acl2::with-guard-checking-error-triple in books/xdoc/top.lisp. It
wasn't caught at certification time because of how it sits under a
make-event.