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
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
