[CakeML-dev] Bootstrapped compiler preview

[Ramana Kumar]

An updated .S file for the compiler is available:
https://cakeml.org/cake-bf676999.S.tar.gz

I haven't packaged any of this up yet or added a page/link on the
website. If anyone else wants to do that please feel free :)

The .S file above has Int.toString in the basis library.

On 13 March 2017 at 08:55, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> Oh the parser also supports characters (escaped if necessary) standing
> for themselves.
>
> On 13 March 2017 at 08:53, 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
>>>> >
>>>
>>>