[acl2/acl2] 9df530: Quoting :doc note-7-2:

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 9df5301d8f1bef03e12fcb0dad542d219e8dd60d
https://github.com/acl2/acl2/commit/9df5301d8f1bef03e12fcb0dad542d219e8dd60d
Author: Matt Kaufmann <kauf...@horatio-168.cs.utexas.edu>
Date: 2015-11-20 (Fri, 20 Nov 2015)

Changed paths:
M axioms.lisp
M books/centaur/fty/tests/terms.lisp
M books/projects/sidekick/lookup.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/oracle-timelimit-tests.lisp
M books/xdoc/defxdoc-raw-impl.lsp
M books/xdoc/defxdoc-raw.lisp
M books/xdoc/save.lisp
M books/xdoc/top.lisp
M books/xdoc/unsound-eval-raw.lsp
M doc.lisp
M other-events.lisp
M translate.lisp

Log Message:
-----------
Quoting :doc note-7-2:

The utility [with-guard-checking] is now limited to forms that do not
reference the ACL2 [state]. A related new utility,
[with-guard-checking-error-triple], may be used for forms that
evaluate to [error-triple]s. For an example showing a bug when
with-guard-checking was applied to forms that access [state], see
the comment about ``with-guard-checking'' in Community Books file
synstem/doc/acl2-doc.lisp, in the form (defxdoc note-7-2 ...).

Infinite loops occurred for calls of (close-output-channel
*standard-co* state) after redirecting standard output using
set-standard-co. A clean error now occurs instead.

We fixed a bug in [state-global-let*] --- actually, in its supporting
system utility acl2-unwind-protect --- that allowed capture of a
lexical variable, temp, to produce bad results, for example as
follows.

(defun foo (temp state)
(declare (xargs :stobjs state :mode :program))
(state-global-let*
((x 3))
(pprogn
(fms "TEMP = ~x0~%X = ~x1~%" (list (cons #0 temp) (cons #1 (@ x)))
*standard-co* state nil)
(value nil))))
(foo 17 state) ; should show TEMP = 17 and X = 3, but caused Lisp error

Quoting a comment in (defxdoc note-7-2 ...):

; We improved the implementation of state-free-global-let* to avoid the
; potential for bad interaction with subsidiary calls of acl2-unwind-protect
; (in the scope of with-local-state, or called in raw Lisp). Now,
; state-free-global-let* pushes onto the *acl2-unwind-protect-stack*.

[Confession: I ran regression before updating recent change to
books/centaur/sv/svtv/decomp.lisp and re-running.]

[GitHub]

Branch: refs/heads/testing