<div dir="auto">Ah cool! Thanks for explaining that.</div><div class="gmail_extra"><br><div class="gmail_quote">On 27 Mar 2017 19:01, "Hugo Férée" <<a href="mailto:H.Feree@kent.ac.uk">H.Feree@kent.ac.uk</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
<br>
Le 27/03/2017 à 17:45, Ramana Kumar a écrit :<br>
> OK great! Thanks Hugo for looking into this on the new branch and moving<br>
> towards removing the eof FFI call. I also think that's the right way to go.<br>
><br>
> By the way I'm curious about what was wrong with the C code when #255<br>
> was open. I don't think we identified a discrepancy between the FFI<br>
> model and the implementation, which is a little disturbing.<br>
That's apparently a very common C mistake: fgetc outputs an int, which<br>
can represent a char, or EOF. And EOF is encoded as -1, so if you cast<br>
this into a char, EOF becomes 255. Thus, (c = fgetc(...)) == EOF becomes<br>
true when the genuine 255 char is read.<br>
<br>
><br>
> On 27 Mar 2017 16:44, "Hugo Férée" <<a href="mailto:H.Feree@kent.ac.uk">H.Feree@kent.ac.uk</a><br>
> <mailto:<a href="mailto:H.Feree@kent.ac.uk">H.Feree@kent.ac.uk</a>>> wrote:<br>
><br>
>     Hi Ramana,<br>
><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>
>     <<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<br>
>     disagree<br>
>     > or have misunderstood each other.<br>
>     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>
><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<br>
>     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>
>     I agree. It would be somehow closer to the behaviour of fgetc in C.<br>
>     ><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>
>     b) probably broke that, yes. I'll make a "ffieof" branch to fix that.<br>
>     ><br>
>     > An addendum to point 1, which I think Scott has advocated<br>
>     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<br>
>     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>
>     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> <mailto:<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>
>     <<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> <mailto:<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>
>     <<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a>><br>
><br>
><br>
</blockquote></div></div>