Command Line Arguments

There are two builds of the CakeML compiler. The 64-bit target version supports multiple different architectures. It should default to your native architecture, but you can also specify via the command line at compile time, e.g. cake --target=x86-64 < input.cml > output.S. The 32-bit target version only supports one architecture, which is ARMv6 (note that the ODROID-XU4 is ARMv7, a 32-bit architecture, backwards compatible with ARMv6. Therefore, we use the 32-bit target version of the CakeML compiler when targeting the ODROID). Since the 32-bit target version only supports one architecture, it does not recognize the target command line argument.

Other command line, compile-time options include inline_size, stack_size, and heap_size, which I assume do exactly what they sound like. Finally, there are two boolean options, sexp, and exclude-prelude. sexp affects the expectations of the structure of the input file. If true, cake will expect to see an s-expression. I am unsure what exclude-prelude does. It set to true in the data61 demo, but doesn't appear to affect the integration of CakeML into seL4 in my own examples.

What does appear to affect the integration of CakeML into seL4 are the stack_size and heap_size options. Raising them higher than around 50 breaks things, and the reason is currently unclear.