[CakeML] CakeML

[Magnus Myreen]

Is there a command for building everything, even including the HOL
light formalisations and the translator examples? -- Magnus

On 28 September 2015 at 12:16, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> As pointed out in the README, only one step is required: you can just call
> Holmake in x86-64/wrapper and it will build everything including the
> executable.
>
> On 28 September 2015 at 20:08, Magnus Myreen <magnus.myreen at gmail.com>
> wrote:
>>
>> Hi Thibault (and CakeML users),
>>
>> A stable version lives under a branch called version1. Download
>> it using:
>>
>>   git clone https://github.com/CakeML/cakeml.git -b version1
>>
>> Then you can build (almost) all of the theories by doing:
>>
>>   cd cakeml/x86-64/
>>   Holmake x64_replTheory.uo
>>
>> The commands above will build the verified x86-64 implementation
>> of the CakeML read-eval-print loop. The Unix executable is produced
>> by the following additional commands:
>>
>>   cd wrapper/
>>   make
>>
>> Note that you will need the very latest development version of
>> HOL4 (from github) to build the version1 branch above.
>>
>> I'm CCing this to the CakeML users mailing list.
>>
>> Cheers,
>> Magnus
>>
>> On 28 September 2015 at 09:50, Gauthier, Thibault
>> <Thibault.Gauthier at uibk.ac.at> wrote:
>> > Hello Magnus,
>> >
>> > I would like to redo the experiments for CakeML as i could only export
>> > 185
>> > out of 232 theories last time, can you point to me to a stable version?
>> > Is
>> > running Holmake in every subdirectory, then loaded every theory in some
>> > compatible order ok? If there is a nicer way to do so, could you point
>> > it
>> > out to me?
>> >
>> > Thank you,
>> > Best wishes,
>> >
>> >
>> > Thibault
>>
>> _______________________________________________
>> Users mailing list
>> Users at cakeml.org
>> https://lists.cakeml.org/listinfo/users
>
>