[CakeML] Monadic translation and in-logic compilation

Magnus Myreen magnus.myreen at gmail.com
Thu Jun 28 18:14:40 UTC 2018


Hi Anthony,

I unfortunately can’t open the sml file on my phone. (I don’t have my
laptop with me on here holiday..)

1) currently yes, but it shouldn’t be the case in the future

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.

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.

Cheers,
Magnus

On Thu, 28 Jun 2018 at 16:07, Anthony Fox <Anthony.Fox at arm.com> wrote:

> 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> 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/54c89eef/attachment-0001.html>


More information about the Users mailing list