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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to