Hi, Jared --
OK, I've thought some more about the issue you raised for the new
function read-file-into-string, and discussed it with J. NICE CATCH!
So I've just now pushed some changes (commit
adb84c213c6383066859bb8b6d7262c2f83ea350) to avoid that problem by
causing an error in the -- probably rare -- cases that it could occur.
User-level documentation is now in :doc read-file-into-string (I plan
to update the manual on the web later today, but for now, with the
latest ACL2, that :doc can be executed in the loop), and some
lower-level documentation is in a comment in raw Lisp variable
*read-file-alist*.
More on the new utility read-file-into-string:
It seems that read-file-as-string (from
books/std/io/read-file-characters.lisp) takes at least 60 times longer
than read-file-into-string. For example, on my Mac:
ACL2 !>(time$ (mv-let (val state) (read-file-as-string "saved_acl2.dx86cl64" state) (value (length val))))
; (EV-REC *RETURN-LAST-ARG3* ...) took
; 15.52 seconds realtime, 15.53 seconds runtime
; (3,162,450,624 bytes allocated).
131768560
ACL2 !>(time$ (length (read-file-into-string "saved_acl2.dx86cl64" state)))
; (EV-REC *RETURN-LAST-ARG3* ...) took
; 0.25 seconds realtime, 0.25 seconds runtime
; (527,078,832 bytes allocated).
131768560
ACL2 !>
So I think it might be good to add links from the :doc for
read-file-characters and read-file-as-string to read-file-into-string,
which (happily) doesn't return state. In fact, you might want to
reimplement read-file-as-string with a call to read-file-into-string.
Thanks by the way for the excellent suggestion to look into memory
mapped IO in CCL. I did, but that seemed to produce a vector that
wasn't obviously (to me, at least) coerceable to a string.
-- Matt
> Date: Mon, 5 Oct 2015 10:05:20 -0500
> From: Matt Kaufmann <
kauf...@cs.utexas.edu>
> CC:
acl2-...@googlegroups.com