[CakeML-dev] ROFS FFI

[Ramana Kumar]

Ah cool! Thanks for explaining that.

On 27 Mar 2017 19:01, "Hugo Férée" <H.Feree at kent.ac.uk> wrote:

>
>
> Le 27/03/2017 à 17:45, Ramana Kumar a écrit :
> > OK great! Thanks Hugo for looking into this on the new branch and moving
> > towards removing the eof FFI call. I also think that's the right way to
> go.
> >
> > By the way I'm curious about what was wrong with the C code when #255
> > was open. I don't think we identified a discrepancy between the FFI
> > model and the implementation, which is a little disturbing.
> That's apparently a very common C mistake: fgetc outputs an int, which
> can represent a char, or EOF. And EOF is encoded as -1, so if you cast
> this into a char, EOF becomes 255. Thus, (c = fgetc(...)) == EOF becomes
> true when the genuine 255 char is read.
>
> >
> > On 27 Mar 2017 16:44, "Hugo Férée" <H.Feree at kent.ac.uk
> > <mailto:H.Feree at kent.ac.uk>> wrote:
> >
> >     Hi Ramana,
> >
> >
> >
> >     Le 27/03/2017 à 15:26, Ramana Kumar a écrit :
> >     > Hi all,
> >     >
> >     > If you've been following the comments on this issue:
> >     >
> >     > https://github.com/CakeML/cakeml/issues/255
> >     <https://github.com/CakeML/cakeml/issues/255>
> >     >
> >     > You may have noticed that there are some problems with our read
> only
> >     > file system model and its implementation in C. I'd like to open
> this
> >     > discussion up to more people, because I think maybe Hugo and I
> >     disagree
> >     > or have misunderstood each other.
> >     I think we understood each other, it's just that I wanted to fix the
> >     issue illustrated by cat first.
> >     I pushed two 1-line commits:
> >     a) casts the char read by fgetc to int
> >     b) removes the EOF check in the ffi for fgetc because this check is
> done
> >     twice.
> >
> >     >
> >     > Specifically what I would like is comments on the following two
> items:
> >     >
> >     > 1. Should we remove the isEof FFI call for the filesystem? For
> >     stdin we
> >     > removed this kind of call, because it's not natural in C, and
> instead
> >     > made getc return a status bit.
> >     I agree. It would be somehow closer to the behaviour of fgetc in C.
> >     >
> >     > 2. Can someone with a fresh pair of eyes check the correspondence
> >     > between the FFI model in rofsFFITheory and the C functions that are
> >     > supposed to implement it in basis_ffi.c? My impression is that
> Hugo's
> >     > latest changes break the correspondence.
> >     b) probably broke that, yes. I'll make a "ffieof" branch to fix that.
> >     >
> >     > An addendum to point 1, which I think Scott has advocated
> >     previously, is
> >     > should we move to a more uniform I/O model in which both file
> >     > descriptors and stream descriptors are treated the same? So
> >     putchar and
> >     > fputc could be modelled by exactly the same HOL function, for
> example.
> >     > (I think this requires a more substantial redesign of the FFI
> models.)
> >     I agree. This would also be the case for writing to stderr.
> >     >
> >     > Cheers,
> >     > Ramana
> >     >
> >     >
> >     > _______________________________________________
> >     > Developers mailing list
> >     > Developers at cakeml.org <mailto:Developers at cakeml.org>
> >     > https://lists.cakeml.org/listinfo/developers
> >     <https://lists.cakeml.org/listinfo/developers>
> >     >
> >
> >     _______________________________________________
> >     Developers mailing list
> >     Developers at cakeml.org <mailto:Developers at cakeml.org>
> >     https://lists.cakeml.org/listinfo/developers
> >     <https://lists.cakeml.org/listinfo/developers>
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170328/8c0c919e/attachment-0001.html>