There are multiple failures in PMF_OF_List. It looks like the behaviour of simplification has changed concerning the functions ennreal and ereal. Larry
> On 12 May 2016, at 11:39, Lawrence Paulson <l...@cam.ac.uk> wrote: > > It has no timeout, sorry, that was my fault. Now set to 300 seconds. > > We don’t need a global timeout, but why not a default timeout? We could set > up to the median runtime. Actually I think our typical value of 600 seconds > is much too high, considering that a loop in a common library could make > dozens of entries run forever. > Larry > >> On 11 May 2016, at 23:58, Gerwin Klein <gerwin.kl...@nicta.com.au> wrote: >> >> If it doesn’t have a timeout set, then that’s a mistake and should be fixed. >> It’d be good to have protection for all builds, not only through Jenkins. >> >> We’ve avoided a global timeout so far, because it’d have to be fairly long, >> i.e. if you have a few entries that don’t terminate because of a change in >> Isabelle for instance, you might very quickly be looking at multiple days. >> >> Might still be a good idea to add one anyway as an additional safety net. >> >> Cheers, >> Gerwin >> >> >> >>> On 12.05.2016, at 06:58, Lars Hupel <hu...@in.tum.de> wrote: >>> >>> Isabelle/8326aa594273 >>> AFP/ffea2c11f257 >>> >>> We appear to have an issue with nonterminating builds. See here: >>> <https://ci.isabelle.systems/jenkins/job/afp-repo-afp/189/consoleFull>. >>> I had to manually kill the running poly process. I'm not quite sure >>> which session causes it, but it's possibly Randomised_Social_Choice. I >>> was under the assumption that all AFP sessions had timeouts set – >>> apparently this is not the case. >>> >>> In order to avoid these problems in the future, I'll implement job >>> timeouts in Jenkins. >>> >>> Cheers >>> Lars >>> _______________________________________________ >>> isabelle-dev mailing list >>> isabelle-...@in.tum.de >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> >> >> ________________________________ >> >> The information in this e-mail may be confidential and subject to legal >> professional privilege and/or copyright. National ICT Australia Limited >> accepts no liability for any damage caused by this email or its attachments. >> _______________________________________________ >> 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
