[CakeML] cakeML build fails

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Thu Jan 16 02:52:10 UTC 2014


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.



More information about the Users mailing list