[isabelle-dev] CakeML compiler in the AFP

[Lars Hupel]

> What is the meaning for "optional?" for AFP?

We don't have any established process for additional components in the
AFP. The question is, should this go into "$AFP_BASE/etc/components" or not?

> I've briefly tried cake-x64-64 on Linux, Mac OS X 10.10, and Cygwin 64
> from https://isabelle.sketis.net/cygwin_2018 -- only the latter causes
> some odd problems in the first attempt ("./cake.exe: cannot execute
> binary file: Exec format error"); it might disappear after some more
> tinkering. In the worst case, such an optional tool is not available for
> Windows users.

Ramana has informed me that the .S file makes some assumptions about
Unix-y behaviour. So it's not surprising to at least one person. Michael
Norrish reported that it works on WSL.

> Providing the already compiled binaries via some component also avoids
> the still open problem of Isabelle sessions that write to the
> file-system as a side-effect: recall that we are in the process to
> eliminate that an turn it into managed "exports" instead, but that does
> not quite fit with executables.

Combined with the other arguments, there seems to be no good reason to
not have it as a component. I'll try to get this done.