[CakeML] Monadic translation and in-logic compilation

Anthony Fox Anthony.Fox at arm.com
Thu Jun 28 13:07:51 UTC 2018


Thanks Magnus,

I had spotted the code under cakeml/examples? What I’d like to know is:


  1.  Do you have to verify a CF style app theorem if you just want to run (via compilation) translated code?
  2.  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?

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.
Cheers,
Anthony

From: Magnus Myreen <magnus.myreen at gmail.com>
Date: Thursday, 28 June 2018 at 06:04
To: Anthony Fox <Anthony.Fox at arm.com>, "users at cakeml.org" <users at cakeml.org>
Subject: Re: [CakeML] Monadic translation and in-logic compilation

Hi Anthony,

Good to hear from you!

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.

(Sorry for not being more informative. I don’t have my laptop with me at present.)

Cheers,
Magnus


On Thu, 28 Jun 2018 at 00:26, Anthony Fox <Anthony.Fox at arm.com<mailto:Anthony.Fox at arm.com>> wrote:
The directory

   cakeml/translator/monadic/examples

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).

The compile succeeds and produces a hello.S file. I then compile this with:

$ cc -o hello ${CAKEML}/basis/basis_ffi.c hello.S

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.

Thanks,
Anthony


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.
_______________________________________________
Users mailing list
Users at cakeml.org
https://lists.cakeml.org/listinfo/users
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20180628/2933b86b/attachment.html>


More information about the Users mailing list