<div dir="ltr"><div><div><div>New version, now with stderr support, at <a href="https://cakeml.org/cake-32b749c3.S.tar.gz" target="_blank">https://cakeml.org/cake-<wbr>32b749c3.S.tar.gz</a><br><br></div>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...<br></div>Here are the kinds of things that could involve:<br></div><div>- make tarball contain basis_ffi.c in addition to the cake.S, and include a Makefile to build cake from these<br></div><div>- use a version numbering scheme that includes something less opaque than commit SHAs (dates?)<br></div><div>- make a releases page on the website which lists downloads to various versions of this tarball<br></div><div>- make a wrapper (maybe a recipe in the Makefile) for linking the result of the compiler with basis_ffi.o<br></div><div><br></div><div>For reference, here are the tarballs currently available for download:<br>cake-32b749c3.S.tar.gz<br>cake-3684c1cd.S.tar.gz<br>cake-389d340f.S.tar.gz<br>cake-a95f62c3.S.tar.gz<br>cake-bf676999.S.tar.gz<br>grep-b75523fe.tar.gz<br>cakeml-v1-beta.zip<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 14 March 2017 at 03:37, Konrad Slind <span dir="ltr"><<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Thanks! That is very useful. I was trying the grep without the surrounding .* padding<div>and getting nothing.</div><span class="m_-9028341199882092530HOEnZb"><font color="#888888"><div><br></div><div>Konrad.</div><div><br></div></font></span></div><div class="m_-9028341199882092530HOEnZb"><div class="m_-9028341199882092530h5"><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Mar 12, 2017 at 4:53 PM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Konrad,<br>
<br>
The source code for the grep program is in the file<br>
characteristic/examples/grepPr<wbr>ogScript.sml.<br>
<br>
The HOL function that does the matching is here:<br>
<a href="https://github.com/CakeML/cakeml/blob/master/characteristic/examples/grepProgScript.sml#L213" rel="noreferrer" target="_blank">https://github.com/CakeML/cake<wbr>ml/blob/master/characteristic/<wbr>examples/grepProgScript.sml#L2<wbr>13</a><br>
<br>
The main program, which is parsed to AST from source syntax inside the<br>
logic, is here:<br>
<a href="https://github.com/CakeML/cakeml/blob/master/characteristic/examples/grepProgScript.sml#L599" rel="noreferrer" target="_blank">https://github.com/CakeML/cake<wbr>ml/blob/master/characteristic/<wbr>examples/grepProgScript.sml#L5<wbr>99</a><br>
(it refers to some other functions that are either parsed or defined<br>
in that file.)<br>
<br>
The regexp parser, which is in<br>
$HOLDIR/examples/formal-langua<wbr>ges/regular/regexp_parserScrip<wbr>t.sml,<br>
currently supports concatenation, alternation (|), repetition (*),<br>
digit set (\d), anything (.), and limited (no ranges, complements, or<br>
escapes) charsets ([...]). The usage for cake_grep is<br>
<br>
cake_grep <regexp_string> <filename> <filename>...<br>
<br>
The regexep is applied, as is, to the whole of each line in each file<br>
(not including the newline character). We might want to change it to<br>
automatically surround it with ".*"s to allow matches anywhere inside<br>
lines.<br>
<br>
The intended semantics (against which the program is verified) is<br>
defined in grepProg also:<br>
<a href="https://github.com/CakeML/cakeml/blob/master/characteristic/examples/grepProgScript.sml#L630" rel="noreferrer" target="_blank">https://github.com/CakeML/cake<wbr>ml/blob/master/characteristic/<wbr>examples/grepProgScript.sml#L6<wbr>30</a><br>
(that function computes the string to be printed on stdout).<br>
<br>
Cheers,<br>
Ramana<br>
<div class="m_-9028341199882092530m_8829565783883367375HOEnZb"><div class="m_-9028341199882092530m_8829565783883367375h5"><br>
On 13 March 2017 at 04:35, Konrad Slind <<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>> wrote:<br>
> What about the source HOL functions for the matcher? (If that's how the AST<br>
> was obtained.)<br>
><br>
> Also, I haven't been able to (on a cursory effort) get a match, probably<br>
> because I don't know<br>
> the expected syntax of a call to this grep. Any clues?<br>
><br>
> Thanks,<br>
> Konrad.<br>
><br>
><br>
><br>
> On Sun, Mar 12, 2017 at 12:32 PM, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>><br>
> wrote:<br>
>><br>
>> Hi Konrad,<br>
>><br>
>> The sources only exist in AST format at the moment. At some point, we<br>
>> had a way of pretty printing AST into concrete syntax, but I'm not<br>
>> sure where that machinery lives nowadays or whether it produces<br>
>> readable concrete syntax for large programs.<br>
>><br>
>> I believe the full AST for the bootstrapped compiler is in the<br>
>> constant called `entire_program` which is defined in the following<br>
>> script:<br>
>><br>
>><br>
>> <a href="https://github.com/CakeML/cakeml/blob/master/compiler/bootstrap/translation/compiler_x64ProgScript.sml#L176" rel="noreferrer" target="_blank">https://github.com/CakeML/cake<wbr>ml/blob/master/compiler/bootst<wbr>rap/translation/compiler_x64Pr<wbr>ogScript.sml#L176</a><br>
>><br>
>> Unfortunately, this term is not shown in the script and it's not easy<br>
>> to explore interactively either.<br>
>><br>
>> Cheers,<br>
>> Magnus<br>
>><br>
>> On 12 March 2017 at 18:22, Konrad Slind <<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>> wrote:<br>
>> > Nice! Is it possible to see the source from which this is generated?<br>
>> ><br>
>> > Thanks,<br>
>> > Konrad.<br>
>> ><br>
>> ><br>
>> > On Fri, Mar 10, 2017 at 12:31 AM, Ramana Kumar<br>
>> > <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>><br>
>> > wrote:<br>
>> >><br>
>> >> I've also put up the .S file for a version of grep in CakeML:<br>
>> >> <a href="https://cakeml.org/grep-b75523fe.tar.gz" rel="noreferrer" target="_blank">https://cakeml.org/grep-b75523<wbr>fe.tar.gz</a><br>
>> >><br>
>> >> You can compile it the same way as the others:<br>
>> >> gcc -o cake_grep basis_ffi.c grep.S<br>
>> >><br>
>> >> It works, but it's pretty slow compared to the GNU version in C... and<br>
>> >> of course has fewer features too... apart from the theorem (actually,<br>
>> >> I still need to produce the theorem about the machine code, as opposed<br>
>> >> to just about the source code).<br>
>> >><br>
>> >> On 5 March 2017 at 11:26, Scott Owens <<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>> wrote:<br>
>> >> > Thanks for this. I tried it out on the quicksort algorithm that I’ve<br>
>> >> > been working on verifying. It runs about 1/3 faster than with the<br>
>> >> > more naive<br>
>> >> > partitioning algorithm from our benchmarks. It also takes about 10<br>
>> >> > seconds<br>
>> >> > to compile, which isn’t great, but not shameful either. With a little<br>
>> >> > more<br>
>> >> > packaging, we could make this a beta release of v2 and put it on the<br>
>> >> > web<br>
>> >> > page.<br>
>> >> ><br>
>> >> > Scott<br>
>> >> ><br>
>> >> >> On 2017/03/04, at 23:12, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>><br>
>> >> >> wrote:<br>
>> >> >><br>
>> >> >> Hi CakeML developers,<br>
>> >> >><br>
>> >> >> I've put the result you could obtain by running the compiler<br>
>> >> >> bootstrap<br>
>> >> >> on a recent commit (389d340f) online here:<br>
>> >> >> <a href="https://cakeml.org/cake-389d340f.S.tar.gz" rel="noreferrer" target="_blank">https://cakeml.org/cake-389d34<wbr>0f.S.tar.gz</a>, so you can try it without<br>
>> >> >> having to build it if you want.<br>
>> >> >><br>
>> >> >> This version contains basis library modules including FileIO<br>
>> >> >> (actually<br>
>> >> >> only read-only) and CharIO, whose contents you can glean by looking<br>
>> >> >> at<br>
>> >> >> basis/mlfileioProgScript.sml and basis/mlcharioProgScript.sml etc.<br>
>> >> >><br>
>> >> >> Here's an example of how to use it. You need the basis_ffi.c file<br>
>> >> >> available from basis/basis_ffi.c in the repo (preferably the one at<br>
>> >> >> commit 389d340f, but I think it hasn't changed on master since<br>
>> >> >> then).<br>
>> >> >><br>
>> >> >> $ tar -xvzf cake-389d340f.S.tar.gz<br>
>> >> >> $ gcc -o cake basis_ffi.c cake-389d340f.S<br>
>> >> >> # Example: a CakeML program that prints the first char in the .S<br>
>> >> >> file<br>
>> >> >> $ ./cake > result.S<br>
>> >> >> val f = FileIO.openIn("cake-389d340f.S<wbr>");<br>
>> >> >> val SOME c = FileIO.fgetc f;<br>
>> >> >> CharIO.write c;<br>
>> >> >> <CTRL-D><br>
>> >> >> $ gcc -o result basis_ffi.c result.S<br>
>> >> >> $ ./result<br>
>> >> >> # prints '#'<br>
>> >> >><br>
>> >> >> Have fun!<br>
>> >> >> Ramana<br>
>> >> >><br>
>> >> >> ______________________________<wbr>_________________<br>
>> >> >> Developers mailing list<br>
>> >> >> <a href="mailto:Developers@cakeml.org" target="_blank">Developers@cakeml.org</a><br>
>> >> >> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/developers</a><br>
>> >> ><br>
>> >> > ______________________________<wbr>_________________<br>
>> >> > Developers mailing list<br>
>> >> > <a href="mailto:Developers@cakeml.org" target="_blank">Developers@cakeml.org</a><br>
>> >> > <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/developers</a><br>
>> >><br>
>> >> ______________________________<wbr>_________________<br>
>> >> Developers mailing list<br>
>> >> <a href="mailto:Developers@cakeml.org" target="_blank">Developers@cakeml.org</a><br>
>> >> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/developers</a><br>
>> ><br>
>> ><br>
>> ><br>
>> > ______________________________<wbr>_________________<br>
>> > Developers mailing list<br>
>> > <a href="mailto:Developers@cakeml.org" target="_blank">Developers@cakeml.org</a><br>
>> > <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/developers</a><br>
>> ><br>
><br>
><br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div></div>