<div dir="ltr">developers/regression-test.sh<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 28 September 2015 at 20:20, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Is there a command for building everything, even including the HOL<br>
light formalisations and the translator examples? -- Magnus<br>
<div class="HOEnZb"><div class="h5"><br>
On 28 September 2015 at 12:16, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br>
> As pointed out in the README, only one step is required: you can just call<br>
> Holmake in x86-64/wrapper and it will build everything including the<br>
> executable.<br>
><br>
> On 28 September 2015 at 20:08, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com">magnus.myreen@gmail.com</a>><br>
> wrote:<br>
>><br>
>> Hi Thibault (and CakeML users),<br>
>><br>
>> A stable version lives under a branch called version1. Download<br>
>> it using:<br>
>><br>
>>   git clone <a href="https://github.com/CakeML/cakeml.git" rel="noreferrer" target="_blank">https://github.com/CakeML/cakeml.git</a> -b version1<br>
>><br>
>> Then you can build (almost) all of the theories by doing:<br>
>><br>
>>   cd cakeml/x86-64/<br>
>>   Holmake x64_replTheory.uo<br>
>><br>
>> The commands above will build the verified x86-64 implementation<br>
>> of the CakeML read-eval-print loop. The Unix executable is produced<br>
>> by the following additional commands:<br>
>><br>
>>   cd wrapper/<br>
>>   make<br>
>><br>
>> Note that you will need the very latest development version of<br>
>> HOL4 (from github) to build the version1 branch above.<br>
>><br>
>> I'm CCing this to the CakeML users mailing list.<br>
>><br>
>> Cheers,<br>
>> Magnus<br>
>><br>
>> On 28 September 2015 at 09:50, Gauthier, Thibault<br>
>> <<a href="mailto:Thibault.Gauthier@uibk.ac.at">Thibault.Gauthier@uibk.ac.at</a>> wrote:<br>
>> > Hello Magnus,<br>
>> ><br>
>> > I would like to redo the experiments for CakeML as i could only export<br>
>> > 185<br>
>> > out of 232 theories last time, can you point to me to a stable version?<br>
>> > Is<br>
>> > running Holmake in every subdirectory, then loaded every theory in some<br>
>> > compatible order ok? If there is a nicer way to do so, could you point<br>
>> > it<br>
>> > out to me?<br>
>> ><br>
>> > Thank you,<br>
>> > Best wishes,<br>
>> ><br>
>> ><br>
>> > Thibault<br>
>><br>
>> _______________________________________________<br>
>> Users mailing list<br>
>> <a href="mailto:Users@cakeml.org">Users@cakeml.org</a><br>
>> <a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
><br>
><br>
</div></div></blockquote></div><br></div>