[isabelle-dev] CakeML compiler in the AFP

Lars Hupel hupel at in.tum.de
Fri Sep 21 14:49:37 CEST 2018

> Just a side-remark: Fabian Immler has started with some experiments to
> use HOL4 with CakeML inside Isabelle. You should keep in contact with
> him about progress and possibilities.

Of course. I'm aware and we're emailing back and forth.

But this is to some extent orthogonal to Fabian's efforts. This is about
packaging the already-bootstrapped CakeML compiler. If Fabian's work
will eventually be able to produce such an artifact too, all the better!
But when it does, we'll still want to have it as a packaged component,
because bootstrapping takes ages (~ 2 days).

More information about the isabelle-dev mailing list