>> 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 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.468s cpu time, 2.451s GC time, factor 1.78) *** Timeout Median_Of_Medians_Selection FAILED The timeout for this session is 50 seconds. So I assume that this is again a problem where the session itself runs through fine, but something after that is not working well. I'll send an update when I have more data points. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
