Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing



On Thu, 8 Jan 2015, Makarius wrote:

The relevant bit is "Thread creation failed", though, which is produced by the Poly/ML runtime system, when the system function pthread_create fails (according to libpolyml/processes.cpp).

In other words, we are back to the usual guess of insufficient resources -- unless your application was unexpectedly tiny.

It should be explicitly noted that stack space was already sucessfully allocated -- there is a different exception for that: "Unable to allocate thread stack".

This might be of concern to David Matthews, the man behind Poly/ML.

I just want to point out, that Isabelle/ML can quite easily cope with a situation, where Thread.fork may sporadically fail due to resource problems, in a way where exceptions won't crash the system infrastructure. It will be done like that in the next Isabelle release.

Until then the same procedure as everytime: tangible problem reports lead to eventual resolution; non-tangible or secret problems will remain indefinitely.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.