[CakeML] CakeML

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Mon Sep 28 10:22:33 UTC 2015


developers/regression-test.sh

On 28 September 2015 at 20:20, Magnus Myreen <magnus.myreen at gmail.com>
wrote:

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


More information about the Users mailing list