Re: [isabelle-dev] Build failure in slow sessions
On 24/02/17 14:24, Makarius wrote: > On 22/02/17 10:14, Lars Hupel wrote: >> >> 11:07:25.458 Iptables_Semantics_Examples: theory >> Analyze_Synology_Diskstation >> 19:01:48.518 Run out of store - interrupting threads >> >> So, nothing happens for a while and then we get an out of memory error. >> Note that the "slow" sessions are executed on 64 bit with an abundance >> of memory. > > More now I have switched back to Poly/ML 5.6 (18f3d341f8c0), until I > find time to look what is really going on there. See also http://lists.inf.ed.ac.uk/pipermail/polyml/2017-February/001978.html http://lists.inf.ed.ac.uk/pipermail/polyml/2017-February/001980.html http://lists.inf.ed.ac.uk/pipermail/polyml/2017-March/001981.html The conclusion of this thread is that we skip Poly/ML 5.7 and David Matthews looks again later. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Build failure in slow sessions
On 22/02/17 10:14, Lars Hupel wrote: > > 11:07:25.458 Iptables_Semantics_Examples: theory > Analyze_Synology_Diskstation > 19:01:48.518 Run out of store - interrupting threads > > So, nothing happens for a while and then we get an out of memory error. > Note that the "slow" sessions are executed on 64 bit with an abundance > of memory. More now I have switched back to Poly/ML 5.6 (18f3d341f8c0), until I find time to look what is really going on there. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Build failure in slow sessions
Dear developers, there have been some failures in the last two runs of the slow sessions: https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/349/ https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/348/ (Relevant changesets are listed there.) Unfortunately there have been no emails because for some reason, they ran into the "hard" timeout as imposed by Jenkins. I will investigate why they haven't been aborted the proper way. What seems interesting are those two consecutive lines of log: 11:07:25.458 Iptables_Semantics_Examples: theory Analyze_Synology_Diskstation 19:01:48.518 Run out of store - interrupting threads (timestamps are elapsed time) So, nothing happens for a while and then we get an out of memory error. Note that the "slow" sessions are executed on 64 bit with an abundance of memory. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
