Extend misc/untranslate-patterns to be aware of std/util/define's untranslate preprocessor
merge
Merge commit '28456273e8683c1077b5347cdaa7e042f6433188' into HEAD
Added new value :ignore-certs for include-book keyword :uncertified-okp.

Quoting :doc note-7-0:

  A new value for [include-book] keyword argument :uncertified-okp is
  :ignore-certs, which specifies that all certificate files are to be
  ignored during inclusion of this book and all of its sub-books. See
  [include-book]. Thanks to Sol Swords for requesting this feature.

Changed the message about "Reading .port file" to an Observation, so
that it can be turned off.

Improved an include-book error message by distinguishing the case of
being under certify-book.
Merge
fancy viewer improvements for smart quotes
Minor doc updates and synched doc.lisp.
Replaced a couple of congruence rule errors with warnings.  Updated :doc coerce about string construction.

Quoting :doc note-7-0:

  We replaced an error with a warning for cases where a classic
  [congruence] rule is unnecessary. Thanks to Jared Davis for sending
  us an example suggesting the need for a change. (See ACL2 source
  function chk-acceptable-congruence-rule for his example and more
  explanation.)

Also, updated :doc coerce with a logical note about viewing coerce as
the constructor for strings.
Fixed a brr error that had been caused by undefining HELP when removing legacy :doc support.

Details:

Added back a trivial HELP command (which was removed when removing
legacy :doc support), to avoid break-rewrite error; and it's a good
idea anyhow.  (Technical explanation: the error was caused by the
attempt to set up a ld-keyword-alias binding :standard-help in the brr
wormhole to the help macro, which no longer existed.)
smartquote and other minor patches for IE
Merge branch 'smartquote'
Merge
Fixed handling of errors inside the break-rewrite loop and other wormholes.

Quoting :doc note-7-0:

  We have cleaned up handling of interrupts and aborts when inside the
  [break-rewrite] loop, or indeed any [wormhole]. Thanks to David
  Russinoff for bringing to our attention a case in which ACL2 quit a
  proof with ``Aborting due to an interrupt'' when in fact no
  interrupts had taken place. Here is an example where that no longer
  happens but did, previously. (For a different example, see the
  comment in the ACL2 sources definition of macro
  bind-acl2-time-limit.)

    (defun foo (x) (cons x x))
    (brr t)
    (monitor '(:definition foo) t)
    (thm (equal (foo y) z))
    (defun h (x) (declare (xargs :mode :program)) (car x))
    ; Raw Lisp error:
    (h 3)
    ; Previously, unexpected proof abort "due to interrupt":
    (thm (equal (append (append x y) x y) (append x y x y)))
Use the new :ignore-certs option for more build consistency in the special two-pass books like std/strings/defs-program.
Dramatically improved efficiency of the dmr utility.

  The [dmr] utility has been made much more efficient, yielding a
  performance penalty of perhaps 10% instead of perhaps more than a
  factor of 30 (3000%).

Also made trivial comment changes and eliminated *saved-deep-gstack*,
which wasn't used.

After consulting with David Rager, I tried to ensure proper dmr
functionality for ACL2(p).
Merge
Fixed bug in interaction of :a! with proof-checker and :brr.

  When aborting with :[a!] inside the [break-rewrite] loop from within
  the [proof-checker], a raw Lisp error could subsequently occur
  saying, ``Attempt to execute *wormhole-cleanup-form* twice!''. This
  has been fixed. Here is an example that formerly caused that
  behavior.

    (defthm silly (implies (null x) (equal (append x y) y)))
    (defconst *c* (make-list 10))
    :brr t
    :monitor (:rewrite silly) t
    (verify (equal (append x (append *c* y)) (append y (append *c* x))))
    bash
    :go
    :a!
    bash ; formerly caused error

Technical note: The fix was to re-work the way that one remains in the
proof-checker after a lisp error.

Note: As usual, I ran a regression before checking in, but there was
initially a failure for the book centaur/misc/alist-equiv, as follows:

  Error:  Fault during read of memory address #x0

Subsequent certification attempts succeeded.  I'm pretty confident
that this was just a CCL (Version 1.11-dev-r16288M-trunk) glitch.
Synched doc.lisp
Incorporated improvements from J, for memsum and for many memoization code comments.

J has completed his review of source file memoize-raw.lisp, and I am
incorporating (with only minor revisions) his changes, which include
many comment improvements and these two fixes to memsum:

- Memsum had printed "?%" instead of "100%".

- Quoting :doc note-7-0, in the section, "Several changes been made to
  function memoization":

    * The output from [memsum] on the line ``Time of all outermost calls''
      no longer includes a percentage, which had been at best
      misleading and at worse nonsensical. Suppose for example that f
      calls g, which does all the work. Then memsum had reported 50%
      of the ``Time of all outermost calls'' for each of f and g,
      even though 100% of the time was spent under each.
Incorporated additions from J for history of hash consing.