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
ML_exception_trace.
> 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_PLATFORM=x86-linux
ML_HOME="$HOME/lib/polyml/${ML_PLATFORM}"
ML_SYSTEM=polyml-5.6.1
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.
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
