[isabelle-dev] Possible non-determinism in HOL-ODE-Numerics
Lars Hupel
hupel at in.tum.de
Thu May 10 20:23:46 CEST 2018
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
More information about the isabelle-dev
mailing list