<div dir="auto"><div>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.</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><div class="gmail_extra" dir="auto"><br><div class="gmail_quote">On 27 Mar 2017 16:44, "Hugo Férée" <<a href="mailto:H.Feree@kent.ac.uk">H.Feree@kent.ac.uk</a>> wrote:<br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Ramana,<br>
<div class="quoted-text"><br>
<br>
<br>
Le 27/03/2017 à 15:26, Ramana Kumar a écrit :<br>
> Hi all,<br>
><br>
> If you've been following the comments on this issue:<br>
><br>
> <a href="https://github.com/CakeML/cakeml/issues/255" rel="noreferrer" target="_blank">https://github.com/CakeML/<wbr>cakeml/issues/255</a><br>
><br>
> You may have noticed that there are some problems with our read only<br>
> file system model and its implementation in C. I'd like to open this<br>
> discussion up to more people, because I think maybe Hugo and I disagree<br>
> or have misunderstood each other.<br>
</div>I think we understood each other, it's just that I wanted to fix the<br>
issue illustrated by cat first.<br>
I pushed two 1-line commits:<br>
a) casts the char read by fgetc to int<br>
b) removes the EOF check in the ffi for fgetc because this check is done<br>
twice.<br>
<div class="quoted-text"><br>
><br>
> Specifically what I would like is comments on the following two items:<br>
><br>
> 1. Should we remove the isEof FFI call for the filesystem? For stdin we<br>
> removed this kind of call, because it's not natural in C, and instead<br>
> made getc return a status bit.<br>
</div>I agree. It would be somehow closer to the behaviour of fgetc in C.<br>
<div class="quoted-text">><br>
> 2. Can someone with a fresh pair of eyes check the correspondence<br>
> between the FFI model in rofsFFITheory and the C functions that are<br>
> supposed to implement it in basis_ffi.c? My impression is that Hugo's<br>
> latest changes break the correspondence.<br>
</div>b) probably broke that, yes. I'll make a "ffieof" branch to fix that.<br>
<div class="quoted-text">><br>
> An addendum to point 1, which I think Scott has advocated previously, is<br>
> should we move to a more uniform I/O model in which both file<br>
> descriptors and stream descriptors are treated the same? So putchar and<br>
> fputc could be modelled by exactly the same HOL function, for example.<br>
> (I think this requires a more substantial redesign of the FFI models.)<br>
</div>I agree. This would also be the case for writing to stderr.<br>
><br>
> Cheers,<br>
> Ramana<br>
><br>
><br>
> ______________________________<wbr>_________________<br>
> Developers mailing list<br>
> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
><br>
<br>
______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
</blockquote></div><br></div></div></div>