[CakeML-dev] Using CF

Magnus Myreen magnus.myreen at gmail.com
Wed Feb 15 11:59:54 UTC 2017


There are plenty of examples under cakeml/basis on the basis branch,
some of which might already have propagated to env-refactor. There are
also examples under cakeml/characteristic/examples.

I've just now pushed a patch that gets the translator built again with
Holmake --fast on the env-refactor branch. I don't know if
cakeml/characteristic builds.

Cheers,
Magnus


On 15 February 2017 at 12:52, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> I’d like to work on some simple algorithmic verification (quicksort or the like) using CF, just to get familiar with how it works. Can anyone point me to what HOL and CakeML commits I should be using to get a working CF? Also, where are the existing examples, so that I can not duplicate any, and also see how to get started.
>
> Scott
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers



More information about the Developers mailing list