[acl2/acl2] 5c03ce: Fixed defun redundancy to accommodate differences ...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 5c03ce5d99f6b5daa45c8f470930c453eec58392
https://github.com/acl2/acl2/commit/5c03ce5d99f6b5daa45c8f470930c453eec58392
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2018-01-10 (Wed, 10 Jan 2018)

Changed paths:
M GNUmakefile
M books/arithmetic/nat-listp.lisp
M books/arithmetic/rational-listp.lisp
M books/std/io/base.lisp
M books/system/doc/acl2-doc.lisp
M defuns.lisp
M doc.lisp

Log Message:
-----------
Fixed defun redundancy to accommodate differences on whether state is declared a stobj. Eliminated deprecated "make" target, "clean". Removed a few documentation BOZOs. Fixed :doc topics std/io/open-output-channel and std/io/open-input-channel to avoid claiming that hard Lisp errors can occur.

Quoting :doc note-8-1:

We improved redundancy checking for [defun] forms so that it is not
sensitive to whether [state] has a :stobj declaration.

The "clean" target of "make" has been deprecated since ACl2 Version
7.4 (released in March, 2017). Its replacement is target
"clean-lite"; or, use target "clean-all" (or equivalently,
"distclean") if you want a more thorough cleaning.

Regarding the redundancy fix mentioned above, here's a new clause
about defun forms in :doc redundant-events:

5. The [stobj]s declared by the two definitions are allowed to disagree
on state: one can declare state among its declared :stobj
values while the other does not, regardless of whether or not
[set-state-ok] has been evaluated. That is, they only need to
agree on the user-defined stobjs.

Thanks to Keshav Kini for pointing out that :doc
std/io/open-output-channel mentions (erroneously) that hard Lisp
errors can occur.


Commit: 4ae5f6b921905ba6d27c7afd789b93c5d6b81d39
https://github.com/acl2/acl2/commit/4ae5f6b921905ba6d27c7afd789b93c5d6b81d39
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2018-01-10 (Wed, 10 Jan 2018)

Changed paths:
M books/doc/relnotes.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp

Log Message:
-----------
Merge


Compare: https://github.com/acl2/acl2/compare/aff263c0b7ce...4ae5f6b92190

[GitHub]

Branch: refs/heads/testing

[Matt Kaufmann]

Hi acl2-books,

I did a search in the documentation for BOZO (or bozo) and found a
bunch of occurrences (many dozens). I wonder if it would be best to
change these so that they make sense to users who don't know that
"BOZO" means something like "A problem to be considered:"; or perhaps
BOZO could be a topic and its occurrences could be links.

My most recent commit (below) dealt with just a few that I was
particularly concerned about.

It would be great if anyone(s) would deal with some other BOZOs. It
would be particularly nice to remove the one about quicklisp in
NOTE-7-0-BOOKS, which to me seems particularly egregious since anyone
might read that topic, not just someone reading the more specialized
topics that typically contain BOZOs.

By the way, I'm not complaining -- I'm pretty sure those BOZOs are
there because someone wrote tons of documentation and wanted to keep
moving, rather than to deal with every little issue. And it's great
that those issues are documented (i.e., with those BOZOs). But if
someone(s) cared to clean up some of them, so much the better.

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

> [1:text/plain Hide]

> --