[CakeML-dev] Adding FileIO to basis

[Ramana Kumar]

Hello all,

I am going to move the FileIO module (currently defined between
catfileSystemTheory and catTheory) into the basis library. This is
because the read-only file system defined there is likely to be useful
for multiple upcoming examples.

However I want to record some downsides and future work. The main
issue is that the basis program will become a little bigger,
exacerbating existing problems with compilation and bootstrap times.
The other issue is that this defers the question of how to do modular
FFI oracles, since for ease of getting something working quickly I
will just add the read-only filesystem FFI functions to the basis
oracle and FFI.

If you have a better plan for FileIO that would mean moving it into
the basis for now is a bad idea, let me know. And better yet, write it
up on the wiki or an issue or something so we can coordinate on
implementing it :)

Cheers,
Ramana