> 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
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
On 23/06/18 19:16, Makarius wrote:
> On 22/06/18 16:33, Lars Hupel wrote:
>>
>> They fail spuriously (except for the last one, which fails reproducibly)
>> when running with a total of 64 or even 128 worker threads:
>>
>> None of this happens when using a total of just 32 worker threads.
>>
>> Maka
On 22/06/18 16:33, Lars Hupel wrote:
>
> They fail spuriously (except for the last one, which fails reproducibly)
> when running with a total of 64 or even 128 worker threads:
>
> None of this happens when using a total of just 32 worker threads.
>
> Makarius, David, this probably requires anoth
> 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 (2 threads, 25.039s elapsed time,
> 44.46
>> So far it looks good, but we still need to test all of AFP.
>
> I will do that today and report my findings.
The machine has been busy since yesterday running the distribution and
the AFP (except for slow) multiple times using different parameters.
The distribution is working fine.
But there
David has worked rather quickly and produced the following commit:
https://github.com/polyml/polyml/commit/86c52cbd8f6d
I have updated the polyml component accordingly in
Isabelle/1b8457cc4de8.
So far it looks good, but we still need to test all of AFP.
I will do that today and report my fin
On 18/06/18 22:38, Makarius wrote:
> On 18/06/18 21:30, Lars Hupel wrote:
>>
>> The precise invocation is:
>>
>> $ ./isabelle/bin/isabelle build -cbv -a -o threads=2 -j 16
>>
>> - The "poly" process gets stuck at 100% CPU load and keeps calling "mmap"
>> - When trying to build the nonterminating se
On 18/06/18 21:30, Lars Hupel wrote:
>
> the good news is that we have just received new hardware (Dual Epyc 7601).
>
> The bad news is that a current development snapshot
> (Isabelle/410818a69ee3) exhibits a problem on this hardware. In
> particular, the session HOL-Corec_Examples doesn't appear
Dear list,
the good news is that we have just received new hardware (Dual Epyc
7601).
The bad news is that a current development snapshot
(Isabelle/410818a69ee3) exhibits a problem on this hardware. In
particular, the session HOL-Corec_Examples doesn't appear to terminate.
$ cat .isabelle/
10 matches
Mail list logo
