<div>Hi Anthony,<br><br>Good to hear from you!<br><br>I suggest you look at the examples in cakeml/examples e.g. the hello example and how the program term is constructed there. I suspect you can do something very similar in your setting. Translator proved certificate theorems can be automatically turned into characteristic formulae (CF) style app theorems which I believe the hello example proved. Once you have such a theorem you can follow the work flow of the hello example.<br><br>(Sorry for not being more informative. I don’t have my laptop with me at present.)<br><br>Cheers,<br>Magnus</div><div dir="auto"><br></div><div dir="auto"><br><div class="gmail_quote" dir="auto"><div>On Thu, 28 Jun 2018 at 00:26, Anthony Fox <<a href="mailto:Anthony.Fox@arm.com">Anthony.Fox@arm.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">





<div lang="EN-GB" link="#0563C1" vlink="#954F72">
<div class="m_8988238469369123413WordSection1">
<p class="MsoNormal"><span style="font-size:11.0pt">The directory<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">   cakeml/translator/monadic/examples<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">provides some examples of translating monadic functions to CakeML. I would like to compile these in the logic and then run them, but I haven’t had much luck.  I’ve attached the hello world script that I came
 up with (command line and exception features will be needed eventually, which is why they’re included).<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">The compile succeeds and produces a hello.S file. I then compile this with:<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">$ cc -o hello ${CAKEML}/basis/basis_ffi.c hello.S<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Running the hello program produces no output and no error is reported. Can someone explain why this isn’t working? I suspect the problem might be in how I’m defining the program (val prog_tm = …)? I’m not
 sure what should be happening between translation and compilation.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Thanks,<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Anthony<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><u></u> <u></u></span></p>
</div>
IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose,
 or store or copy the information in any medium. Thank you.
</div>

_______________________________________________<br>
Users mailing list<br>
<a>Users@cakeml.org</a><br>
<a rel="noreferrer">https://lists.cakeml.org/listinfo/users</a><br>
</blockquote></div></div>