[isabelle-dev] Bad session structure

2018-06-25 Thread Lawrence Paulson
I still get this upon start-up. Any idea why? ebdd5508f386+ tip Larry Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Priority_Queue_Braun.Priority_Queue_Braun") (line 7 of "/Users/lp15/isabelle/af

Re: [isabelle-dev] Bad session structure

2018-06-25 Thread Tobias Nipkow
This is because of a name change in the distribution. The AFP has been updated some 10 minutes later but your test run still saw the old version. It should work now. Tobias On 25/06/2018 15:25, Lawrence Paulson wrote: I still get this upon start-up. Any idea why? ebdd5508f386+ tip Larry Ca

Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

2018-06-25 Thread Makarius
On 22/06/18 16:33, Lars Hupel wrote: >> But there are still (spurious) issues with some AFP sessions. With high >> contention (a total of 64 worker threads at the same time, e.g. with >> threads=2 and -j 32), some sessions will run into suspicious timeouts: >> >> Timing Median_Of_Medians_Selection

[isabelle-dev] LRZ outage

2018-06-25 Thread Lars Hupel
Dear users of the LRZ servers, there appear to be some network and/or capacity problems at LRZ right now, which is also why the "nightly" job failed just now. I hope this will be resolved soon. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.t

Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

2018-06-25 Thread Lars Hupel
> I think it works properly now, see Isabelle/f0f83ce0badd + AFP/f7e9efc65d82. Thanks for that. I'll proceed with the systems integration process of that machine now. > I usually measure the CPU time, multiply it by 2, and take the ceiling > towards the next multiple of 300. In principle this mai