[CakeML-dev] Adding FileIO to basis

[Ramana Kumar]

Yeah the FFI instantiation makes it harder to work with such a fork in
the basis libraries.

What are the concrete plans for speeding up the bootstrap? I have
implemented the app_list change, and I should be able to send you the
.S file for it for testing in about 8 hours (when I get home, because
it's on my laptop, presuming it didn't get killed...).

I'm happy to do the FileIO stuff on a different branch though. I
suggest that speeding up the bootstrap happens on master, which I hope
to merge the basis branch (as it is, without FileIO) into soon.

On 1 March 2017 at 11:46, Yong Kiam <tanyongkiam at gmail.com> wrote:
> 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
>
>