[CakeML] CakeML

[Ramana Kumar]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20150928/606de9d0/attachment.html>