[CakeML] Monadic translation and in-logic compilation

[Anthony Fox]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20180627/ef6c6f5d/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: hello_compileScript.sml
Type: application/octet-stream
Size: 8421 bytes
Desc: hello_compileScript.sml
URL: <https://lists.cakeml.org/pipermail/users/attachments/20180627/ef6c6f5d/attachment.obj>