Thanks for your patch. I've integrated it and pushed it to github.
I was wondering how finalisation should this interact with saving state? Should the state of the finalizers be restored when loadState is called? That is what will happen with the code as it currently is but it is possible to change that so that the state is not affected by loadState by using "non-overwritable" references.
That's an interesting question. If there is a case for using a finalizable value on resources whose state is entirely captured in the mutable and immutable store, then the finalizable state should probably be restored. Most uses I've seen are for C pointers which wouldn't be available in a new session but this is already a limitation of vols. At the moment I can't think of a reason to use non-overwritable refs.
I thought some more about this and ran some tests. I've now made it an non-overwritable reference. I would expect that finalisation would only make sense for external state so it is better to have the finaliser list unaffected by SaveState.loadState. The following examples now do what I would expect: Session 1: let open Finalizable val z = new () in addFinalizer(z, fn () => print "Saver final\n"); PolyML.SaveState.saveState "saved"; touch z end; Prints "Saver final" on exit.
Session 2: let open Finalizable val z = new () in addFinalizer(z, fn () => print "Loader final\n"); PolyML.SaveState.loadState "saved"; touch z end; Prints "Loader final" on exit.
The only other changes I'm thinking about are: 1. Introducing a "touch" primitive for long-term security in case a future update to the optimiser means that the current "touch" becomes a no-op. 2. Simplifying the Weak structure by removing everything except the "weak" function. weakSignal and weakLock were really intended to allow users to write their own finalisation code but if we have finalisers provided they're probably unnecessary. There would obviously have to be a way to wake up the finaliser thread. Currently it's integrated with the signal handler thread in a non-obvious way.
David