[CakeML-dev] ROFS FFI

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Mon Mar 27 14:26:08 UTC 2017


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.

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.

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.

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.)

Cheers,
Ramana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170328/f7dcd24f/attachment.html>


More information about the Developers mailing list