> On 17 Oct 2016, at 20:38, Makarius <[email protected]> wrote: > > On 20/09/16 14:15, David Matthews wrote: >> ... >> Currently, there is a leak because each top-level expression is compiled >> down to machine code even though the code is only executed once. My >> plan is to avoid that by interpreting the top-level rather than fully >> compiling it. > > ... > I do wonder how the classic LCF-style proof assistants would cope with > that, notably ProofPower and HOL4.
Thanks for thinking of us! The ProofPower model is of incremental development of a database containing both data and functions to process it held in a persistent object store as provided in Poly/ML by the PolyML.SaveState structure. A great deal of the data will comprise syntax trees (proved theorems) that have each been calculated by evaluating a large ML expression (a proof) that is executed just once. Most users will keep all the source files they used to build a database and will be prepared to rebuild from scratch quite frequently. I suspect that this use case won’t be badly affected by the leak - presumably the leak will be roughly proportional to the size of the proof scripts (and so it will be megabytes rather than gigabytes). 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 <[email protected]> > 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. Regards, Rob. _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
