[acl2/acl2] 18fbc3: Fixed the definition of the writeable-files field ...

[MattKaufmann]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 18fbc3e9580973784491f75eb7b62baa8f25db99
https://github.com/acl2/acl2/commit/18fbc3e9580973784491f75eb7b62baa8f25db99
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M axioms.lisp
M books/demos/brr-free-variables-log.txt
M books/kestrel/file-io-light/channels.lisp
M books/kestrel/file-io-light/close-output-channel.lisp
M books/kestrel/file-io-light/open-channels-p.lisp
M books/kestrel/file-io-light/read-byte-dollar.lisp
M books/kestrel/file-io-light/read-char-dollar.lisp
M books/kestrel/file-io-light/read-object.lisp
A books/kestrel/utilities/bind-to-bool.lisp
M books/kestrel/utilities/state.lisp
M books/kestrel/utilities/top.lisp
M books/std/io/base.lisp
M books/system/doc/acl2-doc.lisp
M books/system/update-state.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Fixed the definition of the writeable-files field of state, which was causing (state-p1 *default-state*) to be false after yesterday's bug fix.

Quoting :DOC note-8-8, where only the "Moreover" part is new:

Fixed a soundness bug in the macro channel-to-string, which is used
in functions like [fms-to-string] (see [printing-to-strings]).
Thanks to Grant Jurgensen for reporting this bug and providing a
helpful analysis of it. The fix is to the constant
*default-state*. In particular, the following is no longer
provable by ACL2.

(equal (car (open-output-channel :string :character *default-state*))
nil)

Moreover, our fix required modifying several functions related to
I/O, often to add an output-p argument that is true when
considering output (which allows for a channel of type :character
with ``filename'' :string) but false when considering input.
Thanks to Aakash Koneru for pointing us in the direction of these
changes.

Passed "make proofs" and "make devel-check" in addition to the usual
"make regression-everything".



To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/testing