[CakeML] cakeML build fails
konrad.slind at gmail.com
Thu Jan 16 19:49:16 UTC 2014
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.
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.
> 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...
More information about the Users