<div dir="ltr"><div><div><div>Thanks Ramana.<br><br></div>I moved to a bigger machine and now a simple "make"<br>in the top level of vml seems to complete successfully. <br>I am not sure what that means, i.e., what has actually been<br>
</div><div>built and proved, but I will browse the sources a bit to see what <br>I can find out before asking more questions.<br><br></div><div>Konrad.<br><br></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">
On Wed, Jan 15, 2014 at 8:52 PM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">On Tue, Jan 14, 2014 at 12:51 PM, Magnus Myreen<br>
<<a href="mailto:magnus.myreen@cl.cam.ac.uk">magnus.myreen@cl.cam.ac.uk</a>> wrote:<br>
>> 2. I just invoked "make" in the top level. What is the invocation if I<br>
>> wanted to avoid<br>
>>     the memory-expensive bootstrap?<br>
><br>
> You'll need to replace<br>
><br>
> vml/bootstrap/compileReplDecsScript.sml<br>
><br>
> with<br>
><br>
> vml/bootstrap/compileReplDecsCheatScript.sml<br>
><br>
> and also delete "Cheat" in the second line in the file, i.e. the<br>
> new_theory command.<br>
<br>
</div>I've added a script to automate this process.<br>
Use<br>
  cd vml/bootstrap; ./toggle-cheat.sh<br>
to toggle between the setup to run the real bootstrap and the one to<br>
run the cheated version.<br>
<div class="im"><br>
>> 2a. The build needs lem. This should be mentioned.<br>
><br>
> Yes, lem is required for silly Holmake reasons.<br>
<br>
</div>I have attempted to make this false by tweaking the Holmakefiles.<br>
</blockquote></div><br></div>