[CakeML-dev] Bootstrapped compiler preview

[Konrad Slind]

Nice! Is it possible to see the source from which this is generated?

Thanks,
Konrad.


On Fri, Mar 10, 2017 at 12:31 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> I've also put up the .S file for a version of grep in CakeML:
> https://cakeml.org/grep-b75523fe.tar.gz
>
> 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
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170312/26945aed/attachment.html>