<div>Hi Anthony,<br><br>I unfortunately can’t open the sml file on my phone. (I don’t have my laptop with me on here holiday..)<br><br>1) currently yes, but it shouldn’t be the case in the future<br><br>2) without having seen the code, I suspect yes the code you extracted might not have a call to the main function. In the examples some automation adds such a call to the main function and stores the code term in a constant called whole_program.<br><br><div dir="auto">The non-monadic translator is very good for producing pure CakeML code from HOL functions. You can call these translator-generated functions from CF verified code. This is probably the currently recommended route for what you want to achieve. The diff example combines translator and CF.</div><br>Cheers,<br>Magnus</div><div><br><div class="gmail_quote"><div>On Thu, 28 Jun 2018 at 16:07, 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="blue" vlink="purple">
<div class="m_-8438884198617016704WordSection1">
<p class="MsoNormal">Thanks Magnus,<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">I had spotted the code under cakeml/examples? What I’d like to know is:<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<ol style="margin-top:0cm" start="1" type="1">
<li class="m_-8438884198617016704MsoListParagraph" style="margin-left:0cm">Do you have to verify a CF style app theorem if you just want to run (via compilation) translated code?<u></u><u></u></li><li class="m_-8438884198617016704MsoListParagraph" style="margin-left:0cm">What is wrong with what I tried, i.e. using the monadic translator with IO calls? Is it missing a top-level call to “hello” or is something else wrong?<u></u><u></u></li></ol>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">I just want to wrap a simple command line interface around a HOL4 function (as an alternative to EVAL). What’s the quickest route for that? The command line and function behaviour might be quite complex, but I don’t really need to verify
it with pre- and post-conditions (it looks like that can be quite involved). As far as I can tell, the compile examples under cakeml/examples all required a reasonable amount of manual effort.<u></u><u></u></p>
<p class="MsoNormal"><u></u><u></u></p>
<p class="MsoNormal">Cheers,<u></u><u></u></p>
<p class="MsoNormal">Anthony<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<div style="border:none;border-top:solid #b5c4df 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:12.0pt;color:black">From: </span></b><span style="font-size:12.0pt;color:black">Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>><br>
<b>Date: </b>Thursday, 28 June 2018 at 06:04<br>
<b>To: </b>Anthony Fox <<a href="mailto:Anthony.Fox@arm.com" target="_blank">Anthony.Fox@arm.com</a>>, "<a href="mailto:users@cakeml.org" target="_blank">users@cakeml.org</a>" <<a href="mailto:users@cakeml.org" target="_blank">users@cakeml.org</a>><br>
<b>Subject: </b>Re: [CakeML] Monadic translation and in-logic compilation<u></u><u></u></span></p>
</div></div></div><div lang="EN-GB" link="blue" vlink="purple"><div class="m_-8438884198617016704WordSection1">
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal">On Thu, 28 Jun 2018 at 00:26, Anthony Fox <<a href="mailto:Anthony.Fox@arm.com" target="_blank">Anthony.Fox@arm.com</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal">The directory<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal"> cakeml/translator/monadic/examples<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">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></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">The compile succeeds and produces a hello.S file. I then compile this with:<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">$ cc -o hello ${CAKEML}/basis/basis_ffi.c hello.S<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">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></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">Thanks,<u></u><u></u></p>
<p class="MsoNormal">Anthony<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<p class="MsoNormal">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.
<u></u><u></u></p>
</div>
<p class="MsoNormal">_______________________________________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org" target="_blank">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" target="_blank">https://lists.cakeml.org/listinfo/users</a><u></u><u></u></p>
</blockquote>
</div>
</div>
</div></div><div lang="EN-GB" link="blue" vlink="purple">
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></blockquote></div></div>