[isabelle-dev] Sum_of_Squares_Remote.thy dropout

Makarius makarius at sketis.net
Wed Mar 5 15:59:42 CET 2014


On Fri, 21 Feb 2014, Florian Haftmann wrote:

> Referring to isabelle hg id eb07b0acbebc:
>
>> HOL-Library FAILED
>> (see also /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.1_x86-linux/log/HOL-Library)
>>
>> *** At command "by" (line 22 of "~~/src/HOL/Library/Sum_of_Squares_Remote.thy")
>> ### Error: error submitting job
>> *** Prover failed: error submitting job

The problem has disappeared some days ago.  Did the CSDP server recover 
spontaneously, or has anybody kicked it?  How does that work?


 	Makarius


More information about the isabelle-dev mailing list