cakeml
cakeml copied to clipboard
CakeML
CakeML: A Verified Implementation of ML
32-bit riscv (riscv32) implementations are fairly popular with amateurs and have some potential relevance in embedded computers, but our current "riscv" target only supports 64-bits. I have zero interest in...
Under the measurement conditions of #793 the third largest function in a 32-bit-targeting compiler is to_word32Prog_word_bignum_generated_bignum_stubs (595812 bytes). Since this is executed once per compile, it's a reasonable candidate for...
This issue is about setting up an alternative pathway to call into CakeML-generated code from C/C++. Right now, the default exporter only allows running CakeML code as the "main" function....
(all estimates assume #754 #774 #789 have already happened) * ag32, arm7: These are already quite immediate friendly, most header words fit in a 15-16 bit immediate field. * x64:...
* ag32: appears to be optimal. * arm7: We generate 12-byte sequences to load from the instruction stream for everything outside a 12-bit mov immediate range. But since we depend...
COUNT_LIST is a fairly hot function in the current compiler (a different issue, but let's pretend it's desired). It is compiled with bignum support, but a human can easily see...
As the compiler improves, we may wish to try to market it to users of SML binary compilers. Currently, CakeML requires its own syntax, which such users generally do not...
A REPL is more useful if you can abort things that are taking too long. This is immediate if you have threads (you can model an interrupted thread as never...
Except for the bootstraps, most of the directories have phases where only a few low-memory jobs are running and they could usefully be folded together. However, we still want to...
Old SPARC had an instruction which added or subtracted two numbers, but raised an exception if the low two bits of either input were nonzero or if the result overflowed....