<div dir="ltr">I think there's a function called "print" predefined in the basis library, which takes a string, and also "CharIO.write" which takes a character. (The exact functions in the basis for I/O may change a little in later versions..)<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 6 April 2017 at 08:17, Lars Hupel <span dir="ltr"><<a href="mailto:hupel@in.tum.de" target="_blank">hupel@in.tum.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Ramana,<br>
<span class=""><br>
> A preliminary binary with the CakeML parser can be downloaded here:<br>
> <a href="https://cakeml.org/cake-32b749c3.S.tar.gz" rel="noreferrer" target="_blank">https://cakeml.org/cake-<wbr>32b749c3.S.tar.gz</a><br>
><br>
> To build it, one needs the file basis/basis_ffi.c from the repository, then<br>
> run:<br>
> gcc -o cake basis_ffi.c cake-32b749c3.S<br>
><br>
> If you feed the resulting executable source code on standard input, it will<br>
> produce another .S file on standard output which can be built using the<br>
> same recipe (i.e. linked with basis_ffi.c using gcc).<br>
<br>
</span>thanks, that seems to have worked. Excuse the possibly stupid question,<br>
but how do I make the generated program print something? I poked around<br>
the FFI things but couldn't find anything that would compile with the<br>
bootstrapped compiler.<br>
<br>
Cheers<br>
<span class="HOEnZb"><font color="#888888">Lars<br>
</font></span></blockquote></div><br></div>