[CakeML-dev] Bootstrapped compiler preview

Konrad Slind konrad.slind at gmail.com
Mon Mar 13 16:37:32 UTC 2017


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/
> 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
> >> >
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170313/a292baa4/attachment.html>


More information about the Developers mailing list