[acl2/acl2] 616035: Added a book for dealing with filenames that are n...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 61603599d4c6e4c42db2fb24bfa4ce3c3dbbc4f5
https://github.com/acl2/acl2/commit/61603599d4c6e4c42db2fb24bfa4ce3c3dbbc4f5
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2016-07-29 (Fri, 29 Jul 2016)

Changed paths:
M acl2-fns.lisp
M acl2-init.lisp
M axioms.lisp
M basis-a.lisp
A books/kestrel/utilities/non-ascii-pathnames-raw.lsp
A books/kestrel/utilities/non-ascii-pathnames.acl2
A books/kestrel/utilities/non-ascii-pathnames.lisp
M books/kestrel/utilities/top.lisp
M books/system/doc/acl2-doc.lisp
M interface-raw.lisp
M other-events.lisp

Log Message:
-----------
Added a book for dealing with filenames that are not valid ACL2 strings, and in support of that, improved how ACL2 deals with strings that come from outside ACL2.

Quoting :doc note-7-3:

The utility [getenv$] now causes an error if the value it would
otherwise return is not an ACL2 string, for example because it
contains a character whose [char-code] exceeds 255. Many other
changes, less visible to the user, have been made in how ACL2 deals
with strings that come from outside ACL2, in particular, file names
(see the related item just above).

The new book, books/kestrel/utilities/non-ascii-pathnames.lisp, has
some documentation at the top in the form of Lisp comments. Xdoc
documentation may come later.

[GitHub]

Branch: refs/heads/testing