[acl2/acl2] 615ad6: Added function read-file-into-string. Made a smal...

4 views
Skip to first unread message

GitHub

unread,
Oct 4, 2015, 11:37:39 PM10/4/15
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 615ad62bd313cfcbd51a46dbe6e7112cecc782a2
https://github.com/acl2/acl2/commit/615ad62bd313cfcbd51a46dbe6e7112cecc782a2
Author: Matt Kaufmann <kauf...@Matts-MBP.attlocal.net>
Date: 2015-10-04 (Sun, 04 Oct 2015)

Changed paths:
M axioms.lisp
M books/system/doc/acl2-doc.lisp
M boot-strap-pass-2.lisp
M doc.lisp
M history-management.lisp
M other-events.lisp

Log Message:
-----------
Added function read-file-into-string. Made a small :doc mod and a small :pe mod.

Quoting :doc note-7-2:

Function [read-file-into-string] provides an efficient way to return
the contents of a file as a string, without returning an ACL2
[state].

Quoting comments in (defxdoc note-7-2 ...):

; Added :doc computed-hints as the primary parent of using-computed-hints.

; Fixed :pe so that for build-ins, a misleading comma is removed. For example,
; :PE INTEGERP no longer has the following confusing comma: "INTEGERP is built
; into ACL2, without a defining event." Thanks to Alessandro Coglio for
; suggesting this change.

; In support of new function read-file-into-string, eliminated the hypootheses
; of built-in rewrite rule assoc-add-pair.


GitHub

unread,
Oct 5, 2015, 8:37:30 AM10/5/15
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Jared C. Davis

unread,
Oct 5, 2015, 10:41:27 AM10/5/15
to acl2-books
Hi,

How can this be sound? Doesn't it violate functional equality if the
file system changes? I thought that was the whole point of the story
of file IO. Maybe you have some other story in mind.

Cheers,
Jared
> --
> --
> ACL2-books help:
> To post new messages: acl2-...@googlegroups.com
> To unsubscribe: acl2-books-...@googlegroups.com
> More options: http://groups.google.com/group/acl2-books?hl=en
>
> ---
> You received this message because you are subscribed to the Google Groups "acl2-books" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to acl2-books+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.



--
Jared C. Davis <ja...@cs.utexas.edu>
11410 Windermere Meadows
Austin, TX 78759
http://www.cs.utexas.edu/users/jared/

Matt Kaufmann

unread,
Oct 5, 2015, 11:05:21 AM10/5/15
to acl2-...@googlegroups.com, acl2-...@googlegroups.com
I thought about that. In short, I was thinking that we already assume
that the file system doesn't change out from under us (unless
explicitly changed by an ACL2 state-changing command). I'll think a
bit more about this, and I'll discuss this with J today. At worst we
can require a trust tag for the new utility.

So, probably more later....

Thanks --
-- Matt
> From: "Jared C. Davis" <jared....@gmail.com>
> Date: Mon, 5 Oct 2015 09:41:07 -0500
> Reply-To: acl2-...@googlegroups.com
> Mailing-list: list acl2-...@googlegroups.com; contact acl2-boo...@googlegroups.com
> X-Spam-Status: No, hits=-1.6 required=5.0 tests=BOGOFILTER_GOOD=-1.5,
> DKIM_ADSP_CUSTOM_MED=0.001,DKIM_SIGNED=0.1,DKIM_VALID=-0.1,
> FREEMAIL_FORGED_FROMDOMAIN=0.192,FREEMAIL_FROM=0.001,
> HEADER_FROM_DIFFERENT_DOMAINS=0.008,RCVD_IN_DNSWL_LOW=-0.3,
> RCVD_IN_MSPIKE_H2=-0.001,SPF_PASS=-0.001 autolearn=no autolearn_force=no

Matt Kaufmann

unread,
Oct 7, 2015, 10:46:30 AM10/7/15
to acl2-...@googlegroups.com
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
> Reply-To: acl2-...@googlegroups.com
> Mailing-list: list acl2-...@googlegroups.com; contact acl2-boo...@googlegroups.com
>
> I thought about that. In short, I was thinking that we already assume
> that the file system doesn't change out from under us (unless
> explicitly changed by an ACL2 state-changing command). I'll think a
> bit more about this, and I'll discuss this with J today. At worst we
> can require a trust tag for the new utility.
>
> So, probably more later....
>
> Thanks --
> -- Matt
> > From: "Jared C. Davis" <jared....@gmail.com>
> > Date: Mon, 5 Oct 2015 09:41:07 -0500
> > Reply-To: acl2-...@googlegroups.com
> > Mailing-list: list acl2-...@googlegroups.com; contact acl2-boo...@googlegroups.com
> >
Reply all
Reply to author
Forward
0 new messages