On 23/09/2016 17:35, Makarius wrote:
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.
I've run tests with the 64-bit version and also the byte-code interpreted version. They both completed successfully so I suspect a problem with the code-generator. It would be very useful to be able to pin this down. I had a look with gdb at the hanging state and it looks as though there are various threads waiting on a mutex.
Regards, David