Merge branch 'master'.

axioms.lisp

@@ -13347,6 +13347,7 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
     (proofs-co . acl2-output-channel::standard-character-output-0)
     (protect-memoize-statistics . nil)
     (raw-arity-alist . nil)
+    (raw-guard-warningp . nil)
     (raw-include-book-dir!-alist . :ignore)
     (raw-include-book-dir-alist . :ignore)
     (raw-proof-format . nil)

books/acl2s/cgen/top.lisp

@@ -239,6 +239,9 @@ package.</p>
 "
  )
 
+#!ACL2
+(defpointer counter-example-generation cgen)
+
 (defxdoc cgen::flush
   :parents (acl2::cgen)
   :short "Flush/Reset the Cgen state globals to sane values."

books/doc/relnotes.lisp

@@ -347,6 +347,10 @@
  model-specific field. A more complete model of segment address translation has
  been added.</p>
 
+ <h4>AVR ISA</h4>
+ Julien Schmaltz and Peter Schwabes' AVR ISA model has been contributed in book
+ \"projects/avr-isa\".
+  
  <h4>Miscellaneous Books</h4>
 
  <p>The book \"clause-processors/use-by-hint\" now contains an additional

books/system/doc/acl2-doc.lisp

@@ -33686,6 +33686,42 @@ current fast alists."
  guard-quick-reference).  For a discussion of the use of proof to verify the
  absence of guard violations, see @(see verify-guards).</p>")
 
+(defxdoc guard-checking-inhibited
+  :parents (evaluation guard)
+  :short "Evaluating ACL2 expressions"
+  :long "<p>ACL2 sometimes omits the checking of @(see guard)s on recursive
+ calls of functions.  This omission is signaled by a message like the one shown
+ below.</p>
+
+ @({
+ ACL2 !>(factorial 3)
+
+ ACL2 Warning [Guards] in TOP-LEVEL:  Guard-checking will be inhibited
+ for some recursive calls for FACTORIAL and perhaps other functions;
+ see :DOC guard-checking-inhibited.
+
+ 6
+ ACL2 !>
+ })
+
+ <p>More precisely, the warning is printed only when guard-checking is the
+ default, @('t') (see @(see set-guard-checking)) and guards are not verified
+ for the indicated function.  No further such message is printed (for any
+ function) before the next top-level form is submitted.</p>
+
+ <p>To check guards on all recursive calls:</p>
+
+ @({
+ (set-guard-checking :all)
+ })
+
+ <p>To leave the current behavior unchanged except for inhibiting such
+ messages:</p>
+
+ @({
+ (set-guard-checking :nowarn)
+ })")
+
 (defxdoc guard-debug
   :parents (guard debugging)
   :short "Generate markers to indicate sources of @(see guard) proof obligations"
@@ -76488,6 +76524,14 @@ it."
 ; some error messages related to :do-not-induct.  Thanks to a query from Eric
 ; Smith that led to these changes.
 
+; Cleaned up handling of raw-guard-warningp, including: now a state global
+; instead of a Lisp special, modified warning message, added :doc
+; guard-checking-inhibited, and cleared raw-guard-warningp in a simple way for
+; each top level form (in ld-read-eval-print).
+
+; The problem with ev-fncall-w (not a function) was really a problem with
+; raw-ev-fncall, which has been fixed.
+
   :parents (release-notes)
   :short "ACL2 Version  7.5 (xxx, 20xx) Notes"
   :long "<p>NOTE!  New users can ignore these release notes, because the @(see
@@ -76751,6 +76795,23 @@ it."
  especially for his contributions to a fix through helpful conversations and by
  providing code and examples.</p>
 
+ <p>The built-in evaluator functions for ACL2 relied on a system function,
+ @('ev-fncall-w'), that was not a function!  We do not see how to exploit this
+ oddity to prove @('nil'), since @('ev-fncall-w') is guaranteed never to be in
+ @(see logic) mode.  However, it is clearly undesirable.  In the following
+ example, the two @('ev-fncall-w') calls gave different answers on the same
+ inputs &mdash; @('(mv nil 7)') and @('(mv nil 12)') &mdash; but now the second
+ call results in an error.</p>
+
+ @({
+ (defun foo (x y) (+ x y))
+ (assign old-w (w state))
+ (ev-fncall-w 'foo '(3 4) (@ old-w) nil nil nil t nil)
+ (u)
+ (defun foo (x y) (* x y))
+ (ev-fncall-w 'foo '(3 4) (@ old-w) nil nil nil t nil)
+ })
+
  <p>The check for the requisite theorems supporting a @(tsee defabsstobj) event
  included a case where the check was too weak, and it also could cause an
  unexpected assertion.  The first of these could probably cause unsoundness.

books/xdoc/top.lisp

@@ -470,20 +470,30 @@
       (concatenate-symbol-names (list ,@args))
       mksym-package-symbol)))
 
-; Moved from acl2-doc.lisp to make it more widely available
 (defmacro defpointer (from to &optional keyword-p)
-  `(defxdoc ,from
-     :parents (pointers)
-     :short ,(concatenate 'string
-                          "See @(see "
-                          (acl2::string-downcase (symbol-name to))
-                          ")"
-                          (if keyword-p
-                              (concatenate 'string
-                                           " for keyword @(':"
-                                           (acl2::string-downcase (symbol-name from))
-                                           "').")
-                            "."))))
+  (declare (xargs :guard (and (symbolp from) (symbolp to))))
+  (let ((from-pkg  (acl2::string-downcase (symbol-package-name from)))
+        (from-name (acl2::string-downcase (symbol-name         from)))
+        (to-pkg    (acl2::string-downcase (symbol-package-name to)))
+        (to-name   (acl2::string-downcase (symbol-name         to))))
+    `(defxdoc ,from
+       :parents (pointers)
+       :short ,(concatenate
+                'string
+                "See <see topic='@(url "
+                to-pkg "::" to-name
+                ")'>"
+                (if (equal to-pkg from-pkg)
+                    to-name
+                  (concatenate 'string to-pkg "::" to-name))
+                "</see>"
+                (if keyword-p
+                    (concatenate
+                     'string
+                     " for information about the keyword @(':"
+                     from-name
+                     "').")
+                  ".")))))
 
 
 (defun add-resource-directory-fn (dirname fullpath world)

books/xdoc/topics.lisp

@@ -406,6 +406,8 @@ an example table:</p>
 images and icons, but this is currently awkward.  In the future, we may add
 other tags that users request.</p>")
 
+(defpointer syntax markup)
+
 
 (defxdoc preprocessor
   :short "In addition to its @(see markup) language, XDOC includes a
@@ -1746,7 +1748,7 @@ terminal with @(':doc') or in the ACL2-Doc Emacs viewer.</p>")
   :long "<p>Examples:</p>
 
 @({
-    (defpointer acl2 acl2-sedan)
+    (defpointer acl2s acl2-sedan)
     (defpointer guard-hints xargs t)
 })
 
@@ -1759,7 +1761,15 @@ terminal with @(':doc') or in the ACL2-Doc Emacs viewer.</p>")
 <p>This is a simple macro that expands to a @(see defxdoc) form.  It introduces
 a new @(see xdoc) topic, @('new-topic'), that merely links to
 @('target-topic').  The new topic will only be listed under @(see
-pointers).</p>")
+pointers).</p>
+
+<p>A common practice when documenting keyword symbols is to create a
+doc topic in in the \"ACL2\" package or some other relevant package,
+rather than the \"KEYWORD\" package to which the keyword symbol
+rightfully belongs.  In keeping with this practice, the @('keywordp')
+argument to @('defpointer'), if non-nil, adds a clarification that the
+doc topic is really about the keyword symbol with the same name as
+@('new-topic'), rather than @('new-topic') itself.</p>")
 
 
 (defxdoc add-resource-directory

defuns.lisp

@@ -1825,7 +1825,9 @@
 
 ; Sol Swords sent an example in which a clause-processor failed during a
 ; termination proof.  That problem goes away if we install the world, which we
-; do by making the following binding.
+; do by making the following binding.  This seems particularly important now
+; that raw-ev-fncall calls chk-raw-ev-fncall to ensure that the world is
+; (essentially) installed.
 
                        t ; formerly big-mutrec
                        wrld1))

doc.lisp

@@ -28429,7 +28429,13 @@ Subtopics
   [guards-and-evaluation], for a discussion of guards and their
   connection to evaluation.  Advanced system hackers who want to see
   the executable-counterpart definition for f may invoke (trace!
-  (oneify-cltl-code :native t)) before defining f in ACL2.")
+  (oneify-cltl-code :native t)) before defining f in ACL2.
+
+
+Subtopics
+
+  [Guard-checking-inhibited]
+      Evaluating ACL2 expressions")
  (EVALUATOR-RESTRICTIONS
   (META)
   "Some restrictions on the use of evaluators in meta-level rules
@@ -36705,6 +36711,9 @@ Subtopics
   [Extra-info]
       Sources of measure or guard proof obligations
 
+  [Guard-checking-inhibited]
+      Evaluating ACL2 expressions
+
   [Guard-debug]
       Generate markers to indicate sources of [guard] proof obligations
 
@@ -36796,6 +36805,37 @@ Subtopics
 
   [With-guard-checking-event]
       Suppress or enable guard-checking for an event form")
+ (GUARD-CHECKING-INHIBITED
+  (EVALUATION GUARD)
+  "Evaluating ACL2 expressions
+
+  ACL2 sometimes omits the checking of [guard]s on recursive calls of
+  functions.  This omission is signaled by a message like the one
+  shown below.
+
+    ACL2 !>(factorial 3)
+
+    ACL2 Warning [Guards] in TOP-LEVEL:  Guard-checking will be inhibited
+    for some recursive calls for FACTORIAL and perhaps other functions;
+    see :DOC guard-checking-inhibited.
+
+    6
+    ACL2 !>
+
+  More precisely, the warning is printed only when guard-checking is
+  the default, t (see [set-guard-checking]) and guards are not
+  verified for the indicated function.  No further such message is
+  printed (for any function) before the next top-level form is
+  submitted.
+
+  To check guards on all recursive calls:
+
+    (set-guard-checking :all)
+
+  To leave the current behavior unchanged except for inhibiting such
+  messages:
+
+    (set-guard-checking :nowarn)")
  (GUARD-DEBUG
   (GUARD DEBUGGING)
   "Generate markers to indicate sources of [guard] proof obligations
@@ -75452,6 +75492,21 @@ Bug Fixes
   especially for his contributions to a fix through helpful
   conversations and by providing code and examples.
 
+  The built-in evaluator functions for ACL2 relied on a system
+  function, ev-fncall-w, that was not a function!  We do not see how
+  to exploit this oddity to prove nil, since ev-fncall-w is
+  guaranteed never to be in [logic] mode.  However, it is clearly
+  undesirable.  In the following example, the two ev-fncall-w calls
+  gave different answers on the same inputs --- (mv nil 7) and (mv
+  nil 12) --- but now the second call results in an error.
+
+    (defun foo (x y) (+ x y))
+    (assign old-w (w state))
+    (ev-fncall-w 'foo '(3 4) (@ old-w) nil nil nil t nil)
+    (u)
+    (defun foo (x y) (* x y))
+    (ev-fncall-w 'foo '(3 4) (@ old-w) nil nil nil t nil)
+
   The check for the requisite theorems supporting a [defabsstobj] event
   included a case where the check was too weak, and it also could
   cause an unexpected assertion.  The first of these could probably

futures-raw.lisp

@@ -1208,7 +1208,7 @@
 
 ; Parallelism no-fix: we have considered causing child threads to inherit
 ; ld-specials from their parents, or even other state globals such as
-; *ev-shortcut-okp* and *raw-guard-warningp*, as the following comment from
+; *ev-shortcut-okp* and raw-guard-warningp, as the following comment from
 ; David Rager suggests.  But this now seems too difficult to justify that
 ; effort, and we do not feel obligated to do so; see the "IMPORTANT NOTE" in
 ; :doc parallelism.

history-management.lisp

@@ -3547,6 +3547,7 @@
          (t (f-put-global 'current-package "ACL2" state))))
   #-acl2-loop-only
   (cond ((live-state-p state)
+         (setf (car *fncall-cache*) nil)
          (cond ((and *wormholep*
                      (not (eq wrld (w *the-live-state*))))
                 (push-wormhole-undo-formi 'cloaked-set-w! (w *the-live-state*)
@@ -13213,7 +13214,7 @@
 
   (declare (ignorable chk-boot-strap-fns-flg)) ; suppress irrelevance warning
   (er-let*@par
-   ((runic-value (eval-theory-expr expr ctx wrld state)))
+   ((runic-value (eval-theory-expr@par expr ctx wrld state)))
    (let* ((warning-disabled-p (warning-disabled-p "Theory"))
           (ens (ens state)))
      (prog2$

interface-raw.lisp

@@ -1616,17 +1616,14 @@
                            (t nil))))
               (get-declared-stobjs (cdr edcls)))))
 
-(defun-one-output warn-for-guard-body (fn)
-  (assert$ (boundp '*raw-guard-warningp*)
-           (setq *raw-guard-warningp* nil))
-  (let ((state *the-live-state*))
-    (warning$ 'top-level "Guards"
-              "Guard-checking will be inhibited on recursive calls of the ~
-               executable-counterpart (i.e., in the ACL2 logic) of ~x0.  To ~
-               check guards on all recursive calls:~%  (set-guard-checking ~
-               :all)~%To leave behavior unchanged except for inhibiting this ~
-               message:~%  (set-guard-checking :nowarn)"
-              fn)))
+(defun maybe-warn-for-guard-body (fn state)
+  (assert$ (f-get-global 'raw-guard-warningp state)
+           (pprogn (f-put-global 'raw-guard-warningp nil state)
+                   (warning$ 'top-level "Guards"
+                             "Guard-checking will be inhibited for some ~
+                              recursive calls, including ~x0; see :DOC ~
+                              guard-checking-inhibited."
+                             fn))))
 
 (defun-one-output create-live-user-stobjp-test (stobjs)
   (if (endp stobjs)
@@ -2358,9 +2355,10 @@
                            (return-from ,*1*fn ,*1*body)))))
                 (and (and labels-can-miss-guard
                           (not trace-rec-for-none)) ; else skip labels form
-                     `((when (and *raw-guard-warningp*
+                     `((when (and (f-get-global 'raw-guard-warningp
+                                                *the-live-state*)
                                   (eq ,guard-checking-on-form t))
-                         (warn-for-guard-body ',fn))))))
+                         (maybe-warn-for-guard-body ',fn *the-live-state*))))))
               (*1*-body-forms
                (cond ((eq defun-mode :program)
                       (append

ld.lisp

@@ -1058,6 +1058,7 @@
           (pprogn (f-put-global 'trace-level 0 state)
                   (print-deferred-ttag-notes-summary state)))
          (t state))
+   (f-put-global 'raw-guard-warningp t state)
    (mv-let
     (col state)
     (if (and (eql (f-get-global 'in-verify-flg state) 1)