cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

Support heap images for cakeml.

Open ordinarymath opened this issue 11 months ago • 3 comments

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.

ordinarymath avatar Feb 05 '25 03:02 ordinarymath

Allowing candle to use this would be explicit goal.

ordinarymath avatar Feb 05 '25 03:02 ordinarymath

What if anything would you want to be verified about this?

xrchz avatar Feb 05 '25 07:02 xrchz

It would a proof of equivalence between

  1. run candle and "build" the base library. Export the heap state. Create a new instance of cakeml pass it the heap state as a param and continue.
  2. run candle and "build the base library"

ordinarymath avatar Feb 05 '25 07:02 ordinarymath