On 20 Oct 2016, at 18:01, David Matthews <David.Matthews at prolingua.co.uk> wrote:
On 20/10/2016 12:14, Rob Arthan wrote:
During interactive development of a proof script it is usual to try things out repeatedly with frequent evaluations of minor variants of an attempted proof step until you find one that works. It is ls also perfectly possible for a user to develop a ProofPower database the way people develop spreadsheets and SQL databases, incrementally adding things over a prolonged period of time. It is not clear to me how bad the impact would be in these use cases. Is there a way to find out how much memory is occupied by compiled code? If so, then I could try some experiments to quantify the impact.
On 19 Oct 2016, at 12:34, David Matthews <David.Matthews at prolingua.co.uk> wrote: The new mechanism for handling pieces of code deals with most of the issues apart from the question of garbage collection. I was really trying to get a feeling for how serious this was. From the comments on the mailing list it looks as though this is something that is wanted so I'll try and see if I can find a solution.
And thank you for thinking of us!
If it makes the solution easier, I don?t think there is any need to include garbage collection for code in the on-the-fly garbage collection. I think it would be fine to implement it either as an ML function on its own or built into PolyML.SaveState.saveChild (and friends) and PolyML.export.
Just one point. There is only a leak for redefinitions of functions while they are in local memory. If you load a saved state, redefine a function in it and then save a new state then the old code will be replaced with the new code, just as before.
That sounds very promising. Is it also the case that space for code that was only generated to calculate the value of a top level binding will be reclaimed when you save state or export an object file? E.g., the code generated for the right-hand side of the following binding.
val fact10 = let fun f i = if i <= 0 then 1 else i * f(i-1) in f 10 end;
If so, then the only one of my use cases that might have a problem is interactive development. I strongly suspect this is not going to be significant in practice. As I said, if there is a way to see how much memory is occupied by compiled code, I could do some experiments to see if my suspicion is correct.
Regards,
Rob.