> 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). _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
