[CakeML] Build problems

[Ramana Kumar]

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

On 6 April 2017 at 08:17, Lars Hupel <hupel at in.tum.de> wrote:

> Hi Ramana,
>
> > A preliminary binary with the CakeML parser can be downloaded here:
> > https://cakeml.org/cake-32b749c3.S.tar.gz
> >
> > To build it, one needs the file basis/basis_ffi.c from the repository,
> then
> > run:
> > gcc -o cake basis_ffi.c cake-32b749c3.S
> >
> > If you feed the resulting executable source code on standard input, it
> will
> > produce another .S file on standard output which can be built using the
> > same recipe (i.e. linked with basis_ffi.c using gcc).
>
> thanks, that seems to have worked. Excuse the possibly stupid question,
> but how do I make the generated program print something? I poked around
> the FFI things but couldn't find anything that would compile with the
> bootstrapped compiler.
>
> Cheers
> Lars
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20170406/ba4d426f/attachment.html>