[CakeML-dev] Bootstrapped compiler preview

[Scott Owens]

Thanks for this. I tried it out on the quicksort algorithm that I’ve been working on verifying. It runs about 1/3 faster than with the more naive partitioning algorithm from our benchmarks. It also takes about 10 seconds to compile, which isn’t great, but not shameful either. With a little more packaging, we could make this a beta release of v2 and put it on the web page.

Scott

> On 2017/03/04, at 23:12, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 
> Hi CakeML developers,
> 
> I've put the result you could obtain by running the compiler bootstrap
> on a recent commit (389d340f) online here:
> https://cakeml.org/cake-389d340f.S.tar.gz, so you can try it without
> having to build it if you want.
> 
> This version contains basis library modules including FileIO (actually
> only read-only) and CharIO, whose contents you can glean by looking at
> basis/mlfileioProgScript.sml and basis/mlcharioProgScript.sml etc.
> 
> Here's an example of how to use it. You need the basis_ffi.c file
> available from basis/basis_ffi.c in the repo (preferably the one at
> commit 389d340f, but I think it hasn't changed on master since then).
> 
> $ tar -xvzf cake-389d340f.S.tar.gz
> $ gcc -o cake basis_ffi.c cake-389d340f.S
> # Example: a CakeML program that prints the first char in the .S file
> $ ./cake > result.S
> val f = FileIO.openIn("cake-389d340f.S");
> val SOME c = FileIO.fgetc f;
> CharIO.write c;
> <CTRL-D>
> $ gcc -o result basis_ffi.c result.S
> $ ./result
> # prints '#'
> 
> Have fun!
> Ramana
> 
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers