Removed HIDE from *blacklisted-apply$-fns* in the source definition and in projects/apply-model-2/apply-prim.lisp. Fixed failure in making devel-check. Added missing entry in *acl2-broken-links-alist* for recently added reference to :doc consideration.

J has pointed out that removal of HIDE from *blacklisted-apply$-fns*
may be useful for rewriting inside lambdas, where tameness of terms is
relevant.

Successfully completed the usual "everything" regression.  But also,
successfully completed "make devel-check" after modifying the macro
IO?, to avoid a guard proof failure for the form (verify-termination
warning1-cw) in books/system/bind-macro-args.lisp when using a
#+acl2-devel build (see comments in source definition of (defconst
*system-verify-guards-alist* ...) if interested).

Author: MattKaufmann

apply-prim.lisp

@@ -258,7 +258,6 @@
 ; the ttag and untouchable restrictions already prevent warrants.
 
    '(SYNP                                      ; bad
-     HIDE                                      ; stupid
      WORMHOLE1                                 ; restricts arguments
      WORMHOLE-EVAL                             ; restricts arguments
      SYS-CALL                                  ; bad -- requires trust tag

basis-a.lisp

@@ -5655,10 +5655,12 @@
                               (equal vars '(summary ctx alist str))
                               '(lambda (whs)
                                  (cond
-                                  ((and (member-string-equal
+                                  ((and summary
+                                        (member-string-equal
                                          summary
                                          *tracked-warning-summaries*)
-                                        (alistp (wormhole-data whs)))
+                                        (standard-string-alistp
+                                         (wormhole-data whs)))
                                    (let ((expln (list ctx alist str))
                                          (entry (or (assoc-string-equal
                                                      summary

books/projects/apply-model-2/apply-prim.lisp

@@ -106,7 +106,6 @@
 ; the ttag and untouchable restrictions already prevent warrants.
 
    '(SYNP                                      ; bad
-     HIDE                                      ; stupid
      WORMHOLE1                                 ; restricts arguments
      WORMHOLE-EVAL                             ; restricts arguments
      SYS-CALL                                  ; bad -- requires trust tag
@@ -517,6 +516,11 @@
 ;                                           (:executable-counterpart break$))))
 ;       :rule-classes ((:meta :trigger-fns (apply$-prim)))))
 
+    (local
+     (defthm hide-is-identity
+       (equal (hide x) x)
+       :hints (("Goal" :expand ((hide x))))))
+
     (defthm apply$-prim-meta-fn-correct
       (equal (apply$-prim-meta-fn-ev term alist)
              (apply$-prim-meta-fn-ev (meta-apply$-prim term)

books/projects/apply/base.lisp

@@ -458,6 +458,11 @@
                   (apply$-lambda fn args)))
   :hints (("Goal" :use apply$-lambda-takes-arity-args)))
 
+(local
+ (defthm hide-is-identity
+   (equal (hide x) x)
+   :hints (("Goal" :expand ((hide x))))))
+
 (defthm apply$-prim-takes-arity-args
   (implies (apply$-primp fn)
            (equal (apply$-prim fn args)
@@ -472,6 +477,7 @@
                                cdr-cons
                                hons-get
                                (:executable-counterpart hons-assoc-equal)
+                               hide-is-identity
                                )))
   :rule-classes nil)
 

books/system/apply/apply-prim.lisp

@@ -277,6 +277,11 @@
 ;       :hints (("Goal" :in-theory (disable (:executable-counterpart break$))))
 ;       :rule-classes ((:meta :trigger-fns (apply$-prim)))))
 
+    (local
+     (defthm hide-is-identity
+       (equal (hide x) x)
+       :hints (("Goal" :expand ((hide x))))))
+
     (defthm apply$-prim-meta-fn-correct
       (equal (apply$-prim-meta-fn-ev term alist)
              (apply$-prim-meta-fn-ev (meta-apply$-prim term)

books/system/doc/acl2-doc.lisp

@@ -73,6 +73,7 @@
     (BUILD::CERT.PL "[books]/build/doc.lisp")
     (BUILD::CERT_PARAM "[books]/build/doc.lisp")
     (CGEN "[books]/acl2s/cgen/top.lisp")
+    (CONSIDERATION "[books]/hints/consider-hint.lisp")
     (STD::DEFAGGREGATE "[books]/std/util/defaggregate.lisp")
     (DEFCONSTS "[books]/std/util/defconsts.lisp")
     (DEFDATA "[books]/acl2s/defdata/top.lisp")
@@ -86469,6 +86470,9 @@ it."
 ; initialized with a constant.  This seemed potentially important given the
 ; item below about destructively modifying a quoted constant in *fncall-cache*.
 
+; Added comments and checks regarding *blacklisted-apply$-fns*, and removed
+; HIDE from that list.
+
   :parents (release-notes)
   :short "ACL2 Version  8.4 (xxx, 20xx) Notes"
   :long "<p>NOTE!  New users can ignore these release notes, because the @(see

doc.lisp

@@ -14519,6 +14519,7 @@ Subtopics
        (build::cert.pl \"[books]/build/doc.lisp\")
        (build::cert_param \"[books]/build/doc.lisp\")
        (cgen \"[books]/acl2s/cgen/top.lisp\")
+       (consideration \"[books]/hints/consider-hint.lisp\")
        (std::defaggregate \"[books]/std/util/defaggregate.lisp\")
        (defconsts \"[books]/std/util/defconsts.lisp\")
        (defdata \"[books]/acl2s/defdata/top.lisp\")
@@ -43161,7 +43162,7 @@ Subtopics
   [custom-keyword-hints]) and even more general ``computed hints''
   for the advanced user (see [computed-hints]).  Not documented in
   this topic are such hints implemented in books; for an example of
-  so-called :consider hints, see consideration.
+  so-called :consider hints, see [consideration].
 
   Only the first hint applicable to a goal, as specified in the
   user-supplied list of :hints followed by the default hints (see

doc/acl2-code-size.txt

@@ -1,14 +1,14 @@
 Source files (not including doc.lisp):
 ------------------------------------
   CODE LINES:
-  143984 lines,   6408577 characters
+  143985 lines,   6408626 characters
   COMMENT LINES:
    80678 lines,   4864738 characters
   BLANK LINES:
    33802 lines,     33802 characters
   TOTAL:
-  258464 lines,  11307117 characters
+  258465 lines,  11307166 characters
 ------------------------------------
 Documentation (file books/system/doc/acl2-doc.lisp):
-  131104 lines,   5792590 characters
+  131108 lines,   5792745 characters
 ------------------------------------