On 17/10/16 23:58, David Matthews wrote:
> Although the lack of garbage collection of code would mean that
> repeatedly defining the same function would be a memory leak I would be
> surprised if it was a serious problem. Is it likely that one would
> repeatedly redefine the same function within a particular session?
This happens all the time in IDE interaction: things are compiled,
edited, re-compiled; thus old this become inaccessible.
You introduced that principle yourself many years ago, by providing the
very nice PolyML.Compiler interface.
That is one of the big assets of Poly/ML and consequently of Isabelle/ML.
polyml mailing list