document, and possibly rethink, HOLHEAP policy #62

xrchz opened this Issue Aug 18, 2015 · 4 comments


None yet

3 participants

xrchz commented Aug 18, 2015

CakeML currently creates many Poly/ML heaps (one in most directories), building on previous heaps. The exact contents of each heap is a bit random, since there is no well-understood policy on what should be listed. Similarly for the parent heap, when present.

As I understand it, the point of heaps is to trade space for time. The point of this issue is to reevaluate our use of heaps, to pick a policy that is likely to save us the most time for common workflows on the repository, and to document that policy (probably at

@mn200 mn200 was assigned by xrchz Aug 18, 2015
myreen commented Aug 22, 2015

When working with the compiler proofs in compiler1, compiler1/semantics and compiler1/proofs, I find it very useful to have heaps, but to exclude the files that I'm currently working on from the heaps. By excluding the currently changing files, Holmake doesn't rebuild the heaps and loading times are good all around.

xrchz commented Aug 27, 2015

Is it possible to somehow get Holmake to automatically detect which files are changing, to get this good behaviour without having to edit the Holmakefile? Is there some HOLHEAP policy that would give us that behaviour?

Maybe Holmake could be made to only update the heap when told (i.e., when we are done editing), but otherwise default back to reloading changing files (but reusing the heap for non-changing files).

mn200 commented Sep 1, 2015

If the files are already present in the heap, then reloading new versions of those same files over the top of them is not sure to work well.

@xrchz xrchz added a commit that referenced this issue Oct 22, 2015
@xrchz xrchz add heap to targets
I ran into some confusing problems with "lprefix_lubTheory has not been
declared". This is more motivation for #62.
@xrchz xrchz added a commit that referenced this issue Oct 22, 2015
@xrchz xrchz explicitly include preamble in reg_alloc/proofs/heap
again probably related to #62
xrchz commented May 19, 2016

One suggestion (from @tanyongkiam): everything should build without heaps, and heaps should therefore only be an optimisation.

@xrchz xrchz added a commit that referenced this issue Aug 19, 2016
@xrchz xrchz Add semanticsComputeLib to bootstrap/evaluation heap
Not sure if this is appropriate. See Issue #62.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment