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.

books/system/doc/acl2-doc.lisp

@@ -71374,6 +71374,14 @@ it."
 
  </ul>
 
+ <p>@(csee 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.)</p>
+
  <h3>Bug Fixes</h3>
 
  <p>The use of @(tsee set-deferred-ttag-notes) during @(tsee make-event)

books/xdoc/top.lisp

@@ -156,7 +156,8 @@
          (colon-xdoc-init)
          (make-event
           (b* (((mv & all-xdoc-topics state)
-                (with-guard-checking-error-triple t (all-xdoc-topics state)))
+                (acl2::with-guard-checking-error-triple
+                 t (all-xdoc-topics state)))
                ((mv & & state) (colon-xdoc-fn ',name all-xdoc-topics state)))
             (value '(value-triple :invisible))))))))
 

doc.lisp

@@ -70145,6 +70145,15 @@ Heuristic and Efficiency Improvements
       it to be rare that an encapsulate event that was formerly
       redundant is no longer redundant.
 
+  [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.)
+
 
 Bug Fixes
 

other-events.lisp

@@ -9433,18 +9433,14 @@
     (state-global-let*
      ((inhibit-output-lst (cons 'error
                                 (f-get-global 'inhibit-output-lst state))))
-     (let ((saved-w (w state)))
-       (pprogn
-        (set-w! w state)
-        (mv-let
-         (erp val state)
-         (defpkg-items-rec new-kpa old-kpa
-           (f-get-global 'system-books-dir state)
-           ctx w state nil)
-         (assert$
-          (null erp)
-          (pprogn (set-w! saved-w state)
-                  (value val))))))))
+     (mv-let
+       (erp val state)
+       (defpkg-items-rec new-kpa old-kpa
+         (f-get-global 'system-books-dir state)
+         ctx w state nil)
+       (assert$
+        (null erp)
+        (value val)))))
    (t (value nil))))
 
 (defun new-defpkg-list2 (imports all-defpkg-items acc seen)