[CakeML-dev] Adding FileIO to basis
tanyongkiam at gmail.com
Wed Mar 1 00:46:53 UTC 2017
Is it possible to do it in a branch off from arrayProg for now, while we
try and speedup the bootstrap?
array ---- FileIO --- basis2
The bootstrap can continue using basis so we get roughly the same timing
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>
> 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 :)
> Developers mailing list
> Developers at cakeml.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Developers