[isabelle-dev] CakeML compiler in the AFP

[Makarius]

On 20/09/18 11:02, Lars Hupel wrote:
> 
> I would do so without writing this to the list, but there are some
> obstacles. The major obstacle being that the CakeML compiler is not in
> fact a piece of ML code, but a large assembly artifact (65 MB
> uncompressed) that needs to be linked to some FFI code [0]. Hence, it
> requires a C compilation toolchain including "make" [1].
> 
> I see two ways forward:
> 
> 1) It becomes a component.
>    a) ... in Isabelle (optional)
>    b) ... in the AFP (optional?)
> 
> 2) The compressed artifact (~ 2 MB with xz) is committed to the AFP and
> compiled on-the-fly.

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

It should be clear that committing big blobs to a Source Code Management
system is conceptually wrong. It was common practice for SVN, but that
is long past. For Isabelle we have an established concept of
"components" for artifacts that are somehow non-source (e.g.
hol-light-bundle-0.5-126) and often platform-specific.

So if something needs to be compiled for a particular platform, the
component provides the result for all possible platforms for our
high-end users (see also Isabelle/Admin/PLATFORMS), which are not
expected to have low-level development tools around (make, cc, ...).

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.

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.


	Makarius