[CakeML] CakeML

Magnus Myreen magnus.myreen at gmail.com
Mon Sep 28 10:08:55 UTC 2015


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



More information about the Users mailing list