Quoting :doc note-6-5:

  The following changes can make it easier to include books that are
  uncertified or have corrupted compiled files. Thanks to Sol Swords
  for sending helpful, relevant examples and for subsequent
  discussions helping to lead to these changes.

    * It is no longer illegal to call set-compiler-enabled within [books].
      See [compilation], which shows how to do this in order to avoid
      loading the compiled file not only for a book specified by
      [include-book] but also for all books included under that book.
      Also see [compilation] for an analogous way to avoid loading
      .port files (see [uncertified-books]).
    * In situations where it is legal to include an uncertified book
      (typically, any time other than during [certify-book], ACL2
      nonetheless could fail to do so when an error occurred while
      reading a [certificate] file. ACL2 can now instead include the
      book successfully as an uncertified book.
    * When hard raw Lisp errors occur during loading of compiled files on
      behalf of an [include-book] event, that event can now complete
      successfully much as though the compiled file were simply
      missing.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1282 5d84a466-a78b-0930-a311-59b22171a541