[CakeML-dev] ROFS FFI

[Hugo Férée]

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
> 
> 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
> https://lists.cakeml.org/listinfo/developers
>