Irvin
Irvin
There a bunch of these `drule = old_drule` That is confusing I don't think that it would be worth it to fix proofs to use the new drule and just...
Compilers like Haskell support the notion of join points. Join points are continuations. See examples like this ``` fun x = let y () = z in ... y() ```...
This issue is about optimizing the multiplication const in wordLang. Note that pancake does this for known power of 2 [1] but it can be done smarter. see example llvm[2]....
Cakeml does not optimize compilation of code that divides by a const into multiplication by magic number. See https://ridiculousfish.com/blog/posts/labor-of-division-episode-iii.html for a more information on how to calculate said magic number.
As in title. Right now loading that Library is extremely slow.
We should be using the upstream HOL json implementation added here https://github.com/HOL-Theorem-Prover/HOL/pull/1403
CakeML currently does not have a deforestation pass. We would probably improve on benchmarks once this is implemented.
It would be nice for cakeml to support heap images providing similar functionality to polyml heaps where you can save a heap state to disk and load the heap state.
I don't really have a strong use case for this. My main goal is for this is that it would improve explorer output and proofs by moving the builtin functions...
As stated in the title. The plan is to port over benchmarks from ocaml/sandmark and haskell/nofib. The benchmarks will be stored in a separate repository under the cakeml namespace.