[polyml] Update to code-generator and run-time system interface

On 22/09/16 16:50, David Matthews wrote:

On 19/09/2016 21:15, Makarius wrote:

...

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

I've pushed a fix and it no longer fails here. It appears to finish compiling and then hang.

Somehow our ML threads get entangled or deadlocked.

For now, it can be built like this:

isabelle build -o threads=1 Pure

Maybe I should make this the default for the bootstrap: with that already running, it is much easier to work with Isabelle/ML using the Prover IDE.

I will look again later, if I can find anything on my side of the multithreading implementation.

Makarius