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