[acl2/acl2] 9c7116: Eliminated some error noise from magic-ev-fncall. ...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 9c71167c616bf7617b139de8fe0fd2f28b44ac44
https://github.com/acl2/acl2/commit/9c71167c616bf7617b139de8fe0fd2f28b44ac44
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2018-04-19 (Thu, 19 Apr 2018)

Changed paths:
M books/projects/translators/l3-to-acl2/Makefile
M books/system/doc/acl2-doc.lisp
M defuns.lisp
M doc.lisp
M history-management.lisp
M other-events.lisp

Log Message:
-----------
Eliminated some error noise from magic-ev-fncall. Fixed typos in :doc magic-ev-fncall and a source code comment. Avoid remaking l3-to-acl2-books. Added source comment on the Shift from Governors to Rulers.

Quoting :doc note-8-1:

The function [magic-ev-fncall] sometimes printed a message in the
error case in addition to returning that message. It now only
returns that message. Thanks to Sol Swords for bringing to our
attention that certification of a community book,
books/projects/x86isa/proofs/popcount/popcount.lisp, was printing a
warning about "Meta-level function Problem" for thousands of lines.

Fixed typos in :doc magic-ev-fncall.

Fixed typo found by J in a comment in induction-machine-for-fn1.

Fixed books/projects/translators/l3-to-acl2/Makefile so that it
doesn't needlessly recertify l3-to-acl2 books.

Added source code comment contributed by J, "Essay on the Shift from
Governors to Rulers".

[GitHub]

Branch: refs/heads/testing