cakeml
cakeml copied to clipboard
CakeML
CakeML: A Verified Implementation of ML
Right now we always abort, but I think the system is in a state where raising a ML exception is possible. This would be particularly useful for a future REPL....
I don't have a great use case for this, but very big numbers are nice in demos and I'm not sure a verified implementation of Schönhage-Strassen exists right now.
This issue is about speeding up prototyping of code that is (to be) verified using the translator and/or CF. Currently, the process I used is roughly: 1. write HOL definitions...
Even with CML_HEAP_SIZE=60000 it fails with an out of heap error.
PolyML seems to scale poorly beyond about 4 threads; even the currently parallel parts of compilationLib cannot keep the current 8 cores busy, much less higher counts. For large projects...
It is somewhat annoying to work with the multi-100-MB JSON outputs generated when running the --explore compiler on itself. We could make those smaller by changing the displayLang to jsonLang...
We install the GC after register allocation and stack frame construction so that the GC can see a fully concrete stack. We would like to run complex instruction selection (#763)...
We could guarantee a certain amount of space to functions reached via an indirect call. For functions that use less than that amount of space, the amount they make available...
On Linux the easiest way for us to support runtime performance analysis is via the kernel statistical profiler, perf(1). perf can, on the symbols branch, be used to generate flat...
The greatest liability of the original and 2017 compiler explorers is that they depended on server code and therefore became unusable after the server code was no longer maintained -...