[acl2/acl2] a9160d: Cleaned up error output, for example from macros l...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: a9160dfff43c23933d983301340aedfe9da030aa
https://github.com/acl2/acl2/commit/a9160dfff43c23933d983301340aedfe9da030aa
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2017-06-19 (Mon, 19 Jun 2017)

Changed paths:
M axioms.lisp
M books/kestrel/apt/restrict.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M history-management.lisp
M other-events.lisp

Log Message:
-----------
Cleaned up error output, for example from macros like define.

Quoting :doc note-7-5:

When suppressing output of all types other than error --- see
[set-inhibit-output-lst] --- then errors may be reported with
considerably less noise than before, because of the following
changes. Thanke to Eric Smith and Alessandro Coglio for helpful
discussions.

* Reporting of errors by [encapsulate], [progn], and [progn!] is now
considered output of type summary, not of type error.
* When a call of [make-event] specifies keyword :on-behalf-of with
value quiet or quiet!, the concluding error is generally
suppressed; see [make-event-details].
* A failed call of [progn] no longer prints "PROGN failed!"; similary
for [progn!].

Also, I modified books/kestrel/apt/restrict.lisp by adding
:on-behalf-of :quiet to its make-event calls, which eliminates some
noise for failures of the RESTRICT transformation.

I suspect that with these changes I can improve the output of
defsection. So far it's identical for the tests under "Error
Reporting Tests" in books/xdoc/tests/defsection-tests.lisp. If anyone
who uses defsection (directly or indirectly via macros) asks me to
make such an improvement, I'll consider doing so; just send me
examples of what you'd like to see when there is or isn't an error.

[GitHub]

Branch: refs/heads/testing

[Matt Kaufmann]

Hi --

Just a heads-up: You'll should probably clean before certifying books
after this morning's commit/push; anyhow, I found that to be
necessary. (I ran a clean "everything" regression before pushing the
change, but then in another directory I tried that without cleaning
first, and I got failures.)

-- Matt
GitHub <nor...@github.com> writes:

> [1:text/plain Hide]

> --
> --
> ACL2-books help:
> To post new messages: acl2-...@googlegroups.com
> To unsubscribe: acl2-books-...@googlegroups.com
> More options: http://groups.google.com/group/acl2-books?hl=en
>
> ---
> You received this message because you are subscribed to the Google Groups "acl2-books" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to acl2-books+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.