18 Oct
2016
18 Oct
'16
1:43 p.m.
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.
Makarius