[isabelle-dev] Sum of Squares server down?

Tobias Nipkow nipkow at in.tum.de
Fri Sep 12 08:14:05 CEST 2014


Just for the record, the server was not down. This may have merely been a
timeout problem.

Tobias

On 11/09/2014 14:05, Jasmin Christian Blanchette wrote:
> Hi all,
> 
> It appears that the Sum of Squares server is down. This makes the build of the "HOL-Library" session diverge, at least on my machine, when "ISABELLE_FULL_TESTS" is enabled. In addition, it appears to be at the source of the Isatest failures on "mac-poly-M4" and "mac-poly-M8". What's the procedure in such cases?
> 
> Also, would there be a way to change this code so that it skips the tests when the server is not available? I spent literally hours trying to find out why "isabelle build -b HOL-Library" was getting nowhere today for me (my first suspicions were Poly/ML's memory and thread handling).
> 
> Thanks,
> 
> Jasmin
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 



More information about the isabelle-dev mailing list