[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