<div dir="ltr"><div><div><div><div><div><div>Is it possible to do it in a branch off from arrayProg for now, while we try and speedup the bootstrap?<br><br></div>So<br><br>...<br>|<br></div>array ---- FileIO --- basis2<br></div>|<br></div>basis<br><br></div>The bootstrap can continue using basis so we get roughly the same timing properties.<br><br></div>I guess the FFI instantiation is blocking this.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 28, 2017 at 7:19 PM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello all,<br>
<br>
I am going to move the FileIO module (currently defined between<br>
catfileSystemTheory and catTheory) into the basis library. This is<br>
because the read-only file system defined there is likely to be useful<br>
for multiple upcoming examples.<br>
<br>
However I want to record some downsides and future work. The main<br>
issue is that the basis program will become a little bigger,<br>
exacerbating existing problems with compilation and bootstrap times.<br>
The other issue is that this defers the question of how to do modular<br>
FFI oracles, since for ease of getting something working quickly I<br>
will just add the read-only filesystem FFI functions to the basis<br>
oracle and FFI.<br>
<br>
If you have a better plan for FileIO that would mean moving it into<br>
the basis for now is a bad idea, let me know. And better yet, write it<br>
up on the wiki or an issue or something so we can coordinate on<br>
implementing it :)<br>
<br>
Cheers,<br>
Ramana<br>
<br>
______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
</blockquote></div><br></div>