On 16/09/16 14:24, David Matthews wrote:
> I have now pushed a major update to git master which is the result of
> work going back to the beginning of the year.  It covers a number of
> areas but largely the code-generator and the run-time system interface.

This all sounds very interesting and ambitious. After 30 years it will
inevitably require subtle adjustments for Isabelle, but I am confident
that we can once again get to a new stage of performance and robustness.

> 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 leak?

I've heard that the JVM has only recently learned to do proper garbage
collection of dynamically loaded modules.

> It is no longer possible to get an exception trace so PolyML.exception_trace
> has no effect.  The debugger handles this much better anyway.

Luckily, we have already ML_exception_debugger to replace the old

> The system has had some basic testing but there are bound to be bugs in
> something as complex as this.  I'm also continuing to work on
> improvements.  When testing this it is essential to run "make compiler"
> at least once and generally twice to build the new compiler and then
> build the compiler itself with the new compiler.

I am presently testing Poly/ML 38879127481c and Isabelle 9aed2da07200
and ran into a compiler problem in src/Pure/unify.ML:

Exception- Fail "Exception- InternalError: chooseReg raised while
compiling" raised

To reproduce this, you need to update a local Isabelle repository clone
as usual:

  $ cd isabelle-repos

  $ hg pull -u

  $ ./bin/isabelle components -a

Use a local $HOME/.isabelle/etc/settings as usual like this:

ML_OPTIONS="-H 1500 --gcthreads 6"

It is important that the ML_HOME directory does *not* contain the old
libsha1.so that we usually include: it does not work with the new
Poly/ML and can be ignored for the moment.

Now you can invoke "./bin/isabelle build Pure" and it should run until
the above compiler failure.


polyml mailing list

Reply via email to