[CakeML-dev] Bootstrapped compiler preview

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Fri Mar 10 06:31:09 UTC 2017

I've also put up the .S file for a version of grep in CakeML:

You can compile it the same way as the others:
gcc -o cake_grep basis_ffi.c grep.S

It works, but it's pretty slow compared to the GNU version in C... and
of course has fewer features too... apart from the theorem (actually,
I still need to produce the theorem about the machine code, as opposed
to just about the source code).

On 5 March 2017 at 11:26, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> 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
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers

More information about the Developers mailing list