[isabelle-dev] CakeML compiler in the AFP

[Makarius]

On 20/09/18 14:19, Lars Hupel wrote:
> 
> 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.

WSL still does not quite work with Isabelle2017, Isabelle2018: oddly it
is the Z3 component that causes problems. It will hopefully work at some
point in the near future.

For now it merely means that this component is really optional, and does
not work with Windows.


	Makarius