Re: [isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

2018-05-11 Thread Makarius 
On 11/05/18 14:12, Lars Hupel wrote:
>> Last known good state is:
>>
>> Isabelle/7e349d1e3c95
>> AFP/c3cfeceda7a0
> 
> We're back to normal now, as of
> 
> Isabelle/58c9231c2937
> AFP/79f64c92d5ae

Great. I had already started some experiments, but they were inconclusive.

Just for the record, the relevant point seems to be

changeset:   9230:b0febe244fbc
user:paulson 
date:Fri May 11 12:12:01 2018 +0100
files:
thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics.thy
description:
fix to nonterminating proof


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

2018-05-11 Thread Lars Hupel 
> Last known good state is:
> 
> Isabelle/7e349d1e3c95
> AFP/c3cfeceda7a0

We're back to normal now, as of

Isabelle/58c9231c2937
AFP/79f64c92d5ae
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

2018-05-11 Thread Lars Hupel 
(I meant "non-termination", of course, not "non-determinism".)

> Even if it'll terminate eventually (I'll keep it running for a bit
> longer), it surely is a sign of a performance degradation.

This run (threads=8) confirms that HOL-ODE-Numerics doesn't terminate
within 2 elapsed hours:

https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/754/consoleFull
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

2018-05-10 Thread Lars Hupel 

Isabelle/763f5a8f3f7f
AFP/2b0fc2365a6e

I'm unable to build the HOL-ODE-Numerics sessions. Usually, it takes 
about ~1 hour of CPU time (0:45 on lxcisa*).


It's been running for almost 2 CPU hours now on lxcisa0 (threads=10) and 
over 1:30 CPU hours on my i7 (threads=8). It also doesn't appear to 
terminate with threads=2. I'm unsure what's causing it.


Even if it'll terminate eventually (I'll keep it running for a bit 
longer), it surely is a sign of a performance degradation.


Last known good state is:

Isabelle/7e349d1e3c95
AFP/c3cfeceda7a0
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev