> On 20 Oct 2016, at 18:01, David Matthews <david.matth...@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.matth...@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. _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
