[isabelle-dev] CakeML compiler in the AFP

[Lars Hupel]

> 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).