[acl2/acl2] 828e96: Made efficiency improvement for certify-book; fixe...

1 view
Skip to first unread message

GitHub

unread,
Nov 26, 2015, 2:23:06 AM11/26/15
to acl2-...@googlegroups.com
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.


GitHub

unread,
Nov 26, 2015, 2:28:26 AM11/26/15
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages