[CakeML-dev] Adding FileIO to basis

[Yong Kiam]

Is it possible to do it in a branch off from arrayProg for now, while we
try and speedup the bootstrap?

So

...
|
array ---- FileIO --- basis2
|
basis

The bootstrap can continue using basis so we get roughly the same timing
properties.

I guess the FFI instantiation is blocking this.

On Tue, Feb 28, 2017 at 7:19 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> 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
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170228/d8274f1e/attachment.html>