[isabelle-dev] Nonterminating AFP build

[Johannes Hölzl]

I will take care of it next week.

  - Johannes

On Do, 2016-05-12 at 11:58 +0100, Lawrence Paulson wrote:
> 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 <lp15 at 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.Klein at 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 <hupel at 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/conso
> > > > leFull>.
> > > > 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-dev at 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-dev at in.tum.de
> > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
> > > abelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev