[CakeML-dev] ROFS FFI

[Ramana Kumar]

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.

On 27 Mar 2017 16:44, "Hugo Férée" <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
>
> 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
>

_______________________________________________
Developers mailing list
Developers at cakeml.org
https://lists.cakeml.org/listinfo/developers
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170328/94320e8d/attachment.html>