On 20/09/16 14:15, David Matthews wrote:
> On 19/09/2016 21:15, Makarius wrote:
>>> The handling of return addresses from functions has been simplified. A
>>> consequence of this is that when pieces of code are compiled they are
>>> stored in a separate area of memory rather than in the general heap and
>>> not garbage-collected.
>> Does that mean that run-time (re)compilation is a now potential memory
>> I've heard that the JVM has only recently learned to do proper garbage
>> collection of dynamically loaded modules.
> Yes. I can't see a way round it at the moment. It would be difficult
> to produce an example where the only reference to the code of a function
> was through the return address but it could happen if a thread started
> to execute a function contained in a reference and then the reference
> was overwritten.
> 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.
That reminds me a bit of OCaml.
I have always considered it one of the big assets of Poly/ML that fully
native compilation can be performed at run-time, without any difference
to off-line compiled code.
Just a few weeks ago, I explained that to an audience that only knew
boring static compilation in the manner of cc.
My understanding of an LCF-style proof assistant is that compilation and
execution of the program can happen continuously all the time: new code
is added (to implement tools and packages), then new definitions and
proofs are performed, this is repeated indefinitely.
This is also the deeper reason, why we could never use Mlton. (Another
reason is that compilation needs to be fast, in order to be able to
develop all these fine tools interactively.)
Since Isabelle manages the invocation of the Poly/ML compiler itself, we
can probably easily cope with that either way: keeping full compilation
or degrading to interpretation. Although, I would probably just keep
compilation let memory fill up in regular applications: not so much code
is loaded after the main HOL image is finished.
I do wonder how the classic LCF-style proof assistants would cope with
that, notably ProofPower and HOL4.
polyml mailing list