[isabelle-dev] Sum_of_Squares_Remote.thy dropout

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Feb 21 20:13:48 CET 2014


Referring to isabelle hg id eb07b0acbebc:

> haftmann at lxbroy10:~/data/isabelle/master$ ISABELLE_FULL_TEST=true isabelle build HOL-Library
> Running HOL-Library ...
> 
> 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
> *** At command "by" (line 19 of "~~/src/HOL/Library/Sum_of_Squares_Remote.thy")
> *** Prover failed: error submitting job
> *** At command "by" (line 19 of "~~/src/HOL/Library/Sum_of_Squares_Remote.thy")
> *** Prover failed: error submitting job
> *** At command "by" (line 22 of "~~/src/HOL/Library/Sum_of_Squares_Remote.thy")
> *** Prover failed: error submitting job
> *** At command "by" (line 16 of "~~/src/HOL/Library/Sum_of_Squares_Remote.thy")
> *** Prover failed: error submitting job
> *** At command "by" (line 25 of "~~/src/HOL/Library/Sum_of_Squares_Remote.thy")
> *** Prover failed: error submitting job
> *** At command "by" (line 13 of "~~/src/HOL/Library/Sum_of_Squares_Remote.thy")
> *** Prover failed: error submitting job
> *** At command "by" (line 31 of "~~/src/HOL/Library/Sum_of_Squares_Remote.thy")
> *** Prover failed: error submitting job
> *** At command "by" (line 34 of "~~/src/HOL/Library/Sum_of_Squares_Remote.thy")
> *** Prover failed: error submitting job
> *** At command "by" (line 28 of "~~/src/HOL/Library/Sum_of_Squares_Remote.thy")
> Unfinished session(s): HOL-Library
> 0:07:48 elapsed time, 0:19:43 cpu time, factor 2.52

Three weeks ago a run with ISABELLE_FULL_TEST=true used to be succesful.
 Any ideas what could have changed?

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140221/8856ad02/attachment.asc>


More information about the isabelle-dev mailing list