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