<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On 5 April 2017 at 11:14, Lars Hupel <span dir="ltr"><<a href="mailto:hupel@in.tum.de" target="_blank">hupel@in.tum.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Ramana,<br>
<span class=""><br>
> I think (4) is better in the long run too. The TCB is smaller than (2).<br>
> Isabelle already ships with binaries, so I think it would make sense to<br>
> include a verified CakeML binary for this functionality.<br>
<br>
</span>so, would it be possible to get a binary from somewhere? (Either with a<br>
CakeML parser or sexp syntax.)<br></blockquote><div><br></div><div>A preliminary binary with the CakeML parser can be downloaded here:<br><a href="https://cakeml.org/cake-32b749c3.S.tar.gz">https://cakeml.org/cake-32b749c3.S.tar.gz</a><br><br></div><div>To build it, one needs the file basis/basis_ffi.c from the repository, then run:<br></div><div>gcc -o cake basis_ffi.c cake-32b749c3.S<br><br></div><div>If you feed the resulting executable source code on standard input, it will produce another .S file on standard output which can be built using the same recipe (i.e. linked with basis_ffi.c using gcc).<br></div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<span class=""><br>
> The fromSexpTheory doesn't seem to depend on much except astTheory (which<br>
> you already would have a copy of from your Lem -> Isabelle translation of<br>
> the CakeML semantics), and simpleSexpTheory (of which it only depends on<br>
> the sexp datatype - you could define that yourself in Isabelle manually<br>
> very simply). There is some work on importing OpenTheory packages into<br>
> Isabelle here:<br>
> <a href="https://github.com/xrchz/isabelle-opentheory" rel="noreferrer" target="_blank">https://github.com/xrchz/<wbr>isabelle-opentheory</a><br>
><br>
> To record the fromSexpTheory into OpenTheory format, I think you just need<br>
> to build it in the otknl.<br>
<br>
</span>I'm not sure I know what that means or how I would do that. </blockquote><div><br></div><div>It's quite an involved process unfortunately. At a high level, the idea is as follows. One can record the definitions and proofs in a theory, at the level of primitive inferences, in HOL4 and replay them in Isabelle/HOL. This is one method of transporting a formal development from one system to the other.<br><br>If you build a copy of HOL4 using the -otknl flag to bin/build, it uses the proof-recording version of the HOL4 kernel and I think it will generated OpenTheory articles for many of the standard library theories automatically. (One wrinkle with using this for CakeML I just realised is that the proof-recording kernel has slightly different generated-names behaviour than the standard kernel and CakeML is only known to build on the latter.)<br><br></div><div>What's your timeline for this project, and would you be interested in working on producing an OpenTheory export of parts of CakeML with my guidance?<br><br></div><div>Another approach would be to manually port the encoder/decoder definitions, which might be more expedient but less satisfying and reusable.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Is there a<br>
reason why the sexp encoders/decorders are not specified in Lem?<br>
<br></blockquote><div><br></div><div>They're not part of the semantics. There's overhead to using Lem, and there aren't formal guarantees that it produces the same semantics in multiple systems (although I believe a fair amount of work has gone into ensuring that is usually the case).<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Cheers<br>
<span class="HOEnZb"><font color="#888888">Lars<br>
</font></span></blockquote></div><br></div></div>