Re: [isabelle-dev] Nonterminating AFP build

2016-05-12 Thread 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 1

Re: [isabelle-dev] Nonterminating AFP build

2016-05-12 Thread Tobias Nipkow
This requires Johannes' expertise, but he is away for a few days. Tobias On 12/05/2016 12:58, 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:

Re: [isabelle-dev] Nonterminating AFP build

2016-05-12 Thread Lawrence Paulson
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 wrote: > > It has no timeout, sorry, that was my fault. Now set to 300 seconds. > > We don’t need

Re: [isabelle-dev] Nonterminating AFP build

2016-05-12 Thread Lawrence Paulson
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 do

Re: [isabelle-dev] Nonterminating AFP build

2016-05-12 Thread Makarius
On 11/05/16 22:58, Lars Hupel wrote: > In order to avoid these problems in the future, I'll implement job > timeouts in Jenkins. The isatest setup has a global timeout here: http://isabelle.in.tum.de/repos/isabelle/file/5a5beb3dbe7e/Admin/isatest/isatest-makeall#l95 It is also possible to use a

Re: [isabelle-dev] Nonterminating AFP build

2016-05-11 Thread Gerwin Klein
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 chan

[isabelle-dev] Nonterminating AFP build

2016-05-11 Thread Lars Hupel
Isabelle/8326aa594273 AFP/ffea2c11f257 We appear to have an issue with nonterminating builds. See here: . I had to manually kill the running poly process. I'm not quite sure which session causes it, but it's possibly Randomised_