[CakeML-dev] Bootstrapped compiler preview

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Fri Mar 24 00:24:34 UTC 2017


New version, now with stderr support, at https://cakeml.org/cake-
32b749c3.S.tar.gz

I haven't got around to packaging these releases up nicely. If anyone else
wants to try doing that, feel free. I might get to it eventually...
Here are the kinds of things that could involve:
- make tarball contain basis_ffi.c in addition to the cake.S, and include a
Makefile to build cake from these
- use a version numbering scheme that includes something less opaque than
commit SHAs (dates?)
- make a releases page on the website which lists downloads to various
versions of this tarball
- make a wrapper (maybe a recipe in the Makefile) for linking the result of
the compiler with basis_ffi.o

For reference, here are the tarballs currently available for download:
cake-32b749c3.S.tar.gz
cake-3684c1cd.S.tar.gz
cake-389d340f.S.tar.gz
cake-a95f62c3.S.tar.gz
cake-bf676999.S.tar.gz
grep-b75523fe.tar.gz
cakeml-v1-beta.zip

On 14 March 2017 at 03:37, Konrad Slind <konrad.slind at gmail.com> wrote:

> Thanks! That is very useful. I was trying the grep without the surrounding
> .* padding
> and getting nothing.
>
> Konrad.
>
>
> On Sun, Mar 12, 2017 at 4:53 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
> wrote:
>
>> Hi Konrad,
>>
>> The source code for the grep program is in the file
>> characteristic/examples/grepProgScript.sml.
>>
>> The HOL function that does the matching is here:
>> https://github.com/CakeML/cakeml/blob/master/characteristic/
>> examples/grepProgScript.sml#L213
>>
>> The main program, which is parsed to AST from source syntax inside the
>> logic, is here:
>> https://github.com/CakeML/cakeml/blob/master/characteristic/
>> examples/grepProgScript.sml#L599
>> (it refers to some other functions that are either parsed or defined
>> in that file.)
>>
>> The regexp parser, which is in
>> $HOLDIR/examples/formal-languages/regular/regexp_parserScript.sml,
>> currently supports concatenation, alternation (|), repetition (*),
>> digit set (\d), anything (.), and limited (no ranges, complements, or
>> escapes) charsets ([...]). The usage for cake_grep is
>>
>> cake_grep <regexp_string> <filename> <filename>...
>>
>> The regexep is applied, as is, to the whole of each line in each file
>> (not including the newline character). We might want to change it to
>> automatically surround it with ".*"s to allow matches anywhere inside
>> lines.
>>
>> The intended semantics (against which the program is verified) is
>> defined in grepProg also:
>> https://github.com/CakeML/cakeml/blob/master/characteristic/
>> examples/grepProgScript.sml#L630
>> (that function computes the string to be printed on stdout).
>>
>> Cheers,
>> Ramana
>>
>> On 13 March 2017 at 04:35, Konrad Slind <konrad.slind at gmail.com> wrote:
>> > What about the source HOL functions for the matcher? (If that's how the
>> AST
>> > was obtained.)
>> >
>> > Also, I haven't been able to (on a cursory effort) get a match, probably
>> > because I don't know
>> > the expected syntax of a call to this grep. Any clues?
>> >
>> > Thanks,
>> > Konrad.
>> >
>> >
>> >
>> > On Sun, Mar 12, 2017 at 12:32 PM, Magnus Myreen <
>> magnus.myreen at gmail.com>
>> > wrote:
>> >>
>> >> 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/bootst
>> rap/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
>> >> >
>> >
>> >
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170324/b5fe618e/attachment.html>


More information about the Developers mailing list