I have installed a copy of the software locally. Would be worth making this a 
component?

--lcp

> On 11 Sep 2014, at 13:07, Tobias Nipkow <nip...@in.tum.de> wrote:
> 
> 
> 
>> 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?
> 
> I will contact the service team as I have done once before.
> 
> Thanks
> Tobias
> 
>> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to