[CakeML] cakeML build fails

[Konrad Slind]

Thanks Ramana.

I moved to a bigger machine and now a simple "make"
in the top level of vml seems to complete successfully.
I am not sure what that means, i.e., what has actually been
built and proved, but I will browse the sources a bit to see what
I can find out before asking more questions.

Konrad.



On Wed, Jan 15, 2014 at 8:52 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>wrote:

> On Tue, Jan 14, 2014 at 12:51 PM, Magnus Myreen
> <magnus.myreen at cl.cam.ac.uk> wrote:
> >> 2. I just invoked "make" in the top level. What is the invocation if I
> >> wanted to avoid
> >>     the memory-expensive bootstrap?
> >
> > You'll need to replace
> >
> > vml/bootstrap/compileReplDecsScript.sml
> >
> > with
> >
> > vml/bootstrap/compileReplDecsCheatScript.sml
> >
> > and also delete "Cheat" in the second line in the file, i.e. the
> > new_theory command.
>
> I've added a script to automate this process.
> Use
>   cd vml/bootstrap; ./toggle-cheat.sh
> to toggle between the setup to run the real bootstrap and the one to
> run the cheated version.
>
> >> 2a. The build needs lem. This should be mentioned.
> >
> > Yes, lem is required for silly Holmake reasons.
>
> I have attempted to make this false by tweaking the Holmakefiles.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20140116/dfb113d5/attachment.html>