[acl2/acl2] e831c2: Fixed over-aggressive checking for untouchable fun...

0 views
Skip to first unread message

GitHub

unread,
Aug 23, 2016, 6:24:11 AM8/23/16
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: e831c273ac6d2a36eb55e24182d671b9dcc56b63
https://github.com/acl2/acl2/commit/e831c273ac6d2a36eb55e24182d671b9dcc56b63
Author: Matt Kaufmann <kauf...@Matts-MBP.attlocal.net>
Date: 2016-08-23 (Tue, 23 Aug 2016)

Changed paths:
M acl2-check.lisp
M acl2-fns.lisp
M acl2.lisp
M axioms.lisp
M basis-a.lisp
M books/misc/check-acl2-exports.lisp
M books/std/strings/pretty.lisp
M books/std/util/maybe-defthm.lisp
M books/system/doc/acl2-doc.lisp
M books/system/subcor-var.lisp
M books/xdoc/spellcheck.lisp
M boot-strap-pass-2.lisp
M defthm.lisp
M interface-raw.lisp
M ld.lisp
M other-events.lisp
M proof-builder-b.lisp
M tau.lisp
M translate.lisp

Log Message:
-----------
Fixed over-aggressive checking for untouchable functions that ignored the state global, temp-touchable-fns. Fixed a bug for when LD is called with :standard-co and :proofs-co representing the same file. Improved error message for call of undefined symbol. Remove-lambdas no longer puts terms in quote-normal form. Accept and print #\Return.

Quoting :doc note-7-3:

Checking for untouchable functions was too aggressive in some cases,
in particular for [defattach] and for macro calls that yield
[events], because such checks failed to take into account for
[state] global temp-touchable-fns. (See [remove-untouchable] for
relevant background.) Those checks have been fixed.

The documentation for [ld] specified that ``If [standard-co] and
[proofs-co] are equal strings, only one channel to that file is
opened and is used for both.'' This was only the case when
proofs-co was a canonical absolute (full) pathname. This has been
fixed; now, the criterion is that standard-co and proofs-co are
strings that represent the same file.

The error message for a call of a undefined symbol now mentions
defined symbols in other packages with the same name, in case that
is what the user intended. The message also points to a new
documentation topic, near-misses, which provides a way (using
certain books) to find approximate matches that are defined. Thanks
to Jared Davis for suggesting such a change.

ACL2 now accepts #\Return as legal notation for the character with
[char-code] 13, and it prints that character as #\Return rather
than moving the cursor (e.g., to the beginning of the line). Thanks
to Alessandro Coglio, Eric McCarthy, and Eric Smith for requesting
this change, to help with the printing of failed subgoals that
mention this character.

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

; Remove-lambdas no longer puts terms into quote-normal form, although it still
; preserves quote-normal form (i.e., the result is in quote-normal if the input
; is). Thanks to Eric Smith for suggesting such a change. Note that
; remove-lambdas is now a guard-verified :logic mode function.

NOTE: I wonder if atom-size, defined in books/std/strings/pretty.lisp,
is really just ACL2 source function flsz-atom. I haven't checked.


GitHub

unread,
Aug 23, 2016, 6:27:48 AM8/23/16
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages