<div dir="ltr"><div><div><div><div><div><div>Hi all,<br><br></div>If you've been following the comments on this issue:<br><br><a href="https://github.com/CakeML/cakeml/issues/255">https://github.com/CakeML/cakeml/issues/255</a><br><br></div>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.<br><br></div>Specifically what I would like is comments on the following two items:<br><br></div>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.<br><br></div>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.<br><br></div><div>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.)<br><br></div><div>Cheers,<br></div><div>Ramana<br></div></div>