[CakeML] Build problems
Ramana.Kumar at cl.cam.ac.uk
Thu Apr 6 07:50:46 UTC 2017
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
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,
> > run:
> > gcc -o cake basis_ffi.c cake-32b749c3.S
> > If you feed the resulting executable source code on standard input, it
> > 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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Users