[isabelle-dev] HOL-Analysis instability

[Manuel Eberl]

On a related note, HOL-Complex_Analysis ran for 3 hours before being
killed due to timeout on our Jenkins CI before. On my system it builds
in 30 seconds. No idea what's going on there.

On another probably unrelated note, whenever I open a theory with a lot
of dependencies in Isabelle/jEdit (e.g. HOL-Analysis.Analysis with only
the HOL image loaded), the entire Java process freezes up for about 5
minutes or more (no UI reaction to clicks etc). The theory panel is also
still blank at that point (except for the "Analysis" theory).

CPU load is very high on all cores during that time. Initially, it is
split roughly evenly between Java and Poly/ML (about 55% java and 45%
poly), but after 2–3 minutes, Poly/ML seems to idle and Java uses 100%
CPU, racking up 3 hours of CPU time. Memory usage seems fairly stable
throughout. Swap usage is zero.

After about 10 minutes, CPU usage drops to almost 0%, but the UI is
still unresponsive for quite a while after that (I usually just get
frustrated and abort, so I cannot say how long exactly – but I do think
it starts working again eventually).

In Isabelle2019, it was nowhere near this bad. The theories being loaded
and their progress were displayed almost immediately. The UI was a bit
slow to respond at times, but it did so in fractions of seconds (as
opposed to 15 minutes).

System specs: Arch Linux, isabelle-dev/6f8422385878, 12-core AMD Ryzen 9
3900X, 32 GB RAM, Poly/ML x86_64_32-linux

Cheers,

Manuel


On 03/12/2019 19:11, Fabian Immler wrote:
> I also saw this failure while building 3548d54ce3ee on lxcisa0 with the
> following command and ML_OPTIONS:
> isabelle build -v -a -X slow -j8 -othreads=8
> ML_OPTIONS="--minheap 1000 --maxheap 4000"
> 
> After the failure, another invocation of the same command built
> everything without problems.
> A wild guess: could be related to the fact that on the second attempt,
> HOL-Analysis was the only session being built, whereas on the first
> attempt there were lots of sessions (based on HOL) running in parallel.
> 
> Fabian
> 
> On 12/3/2019 11:34 AM, Manuel Eberl wrote:
>> There have been a lot of spurious build failures of HOL-Analysis in our
>> Jenkins CI [1,2] lately (cf. e.g. 6c208c2dca53). A quick glance at [3]
>> seems to paint a similar picture. Linear_Programming int he AFP also
>> fails spuriously. The error messages typically say
>>
>>    Run out of store - interrupting threads
>>    *** Interrupt
>>
>> When it does go through, it seems to go through with a reasonable amount
>> of time and memory. Also, this still seems to be happening after I split
>> off HOL-Complex_Analysis from HOL-Analysis, which amounts to a 10%
>> reduction in lines and elapsed time and 25% of GC time, so I would
>> assume that it lowers the memory requirements quite a bit.
>>
>> But if anything, it seems to have made it worse: It seems that
>> HOL-Analysis now fails almost every time. On my personal machine,
>> HOL-Analysis never fails to build.
>>
>> I have no idea how to track down a problem like this.
>>
>> Cheers,
>>
>> Manuel
>>
>> [1]:
>> https://ci.isabelle.systems/jenkins/job/isabelle-all/1553/consoleFull
>> [2]:
>> https://ci.isabelle.systems/jenkins/job/isabelle-all/1571/consoleFull
>> [3]: https://isabelle.sketis.net/devel/build_status/
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev