[acl2/acl2] adb84c: Order stobj declarations first for guard generatio...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: adb84c213c6383066859bb8b6d7262c2f83ea350
https://github.com/acl2/acl2/commit/adb84c213c6383066859bb8b6d7262c2f83ea350
Author: Matt Kaufmann <kauf...@Matts-MBP.attlocal.net>
Date: 2015-10-07 (Wed, 07 Oct 2015)

Changed paths:
M axioms.lisp
M basis-a.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M other-events.lisp
M translate.lisp

Log Message:
-----------
Order stobj declarations first for guard generation, even for more than one declare form. Add checks to guarantee that read-file-into-string is truly a function.

Quoting :doc note-7-2:

For [guard] proof obligations, all conjuncts from [stobj]
declarations (supplied as :stobjs keywords in [xargs] declarations)
preceded all other conjuncts (i.e., from [type] declarations or
[xargs] :guard declarations). Previously, this was only true within
a given [declare] form. Thanks to Dave Greve for bringing this
issue to our attention.

Also, made two fixes for recent addition of function
read-file-into-string:

- Thanks to feedback from Jared, added checks to guarantee that
read-file-into-string is truly a function (also, technically,
close-input-channel). This solution is described in a comment in
the definition of the new variable *read-file-alist*.

- Added call of close-input-channel in the #+acl2-loop-only (logic)
definition of read-file-into-string2.

[GitHub]

Branch: refs/heads/testing