[CakeML-dev] Bootstrapped compiler preview

[Magnus Myreen]

Hi Konrad,

The sources only exist in AST format at the moment. At some point, we
had a way of pretty printing AST into concrete syntax, but I'm not
sure where that machinery lives nowadays or whether it produces
readable concrete syntax for large programs.

I believe the full AST for the bootstrapped compiler is in the
constant called `entire_program` which is defined in the following
script:

https://github.com/CakeML/cakeml/blob/master/compiler/bootstrap/translation/compiler_x64ProgScript.sml#L176

Unfortunately, this term is not shown in the script and it's not easy
to explore interactively either.

Cheers,
Magnus

On 12 March 2017 at 18:22, Konrad Slind <konrad.slind at gmail.com> wrote:
> 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
>
>
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>