[isabelle-dev] HOL-Analysis instability -- Isabelle/jEdit

Makarius makarius at sketis.net
Wed Dec 4 20:14:08 CET 2019


On 03/12/2019 21:16, Makarius wrote:
> On 03/12/2019 19:34, Manuel Eberl wrote:
>>
>> 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).
> 
> This is unrelated. I am presently bisecting the history to find out where it
> occurs first.

Thanks for keeping an eye on the fine points of our PIDE game engine. The
problem was introduced 2 weeks ago when maximizing the throughput of headless
PIDE, but it tends to block interactive PIDE. See now the following change:

changeset:   71230:dafa5fce70f1
user:        wenzelm
date:        Wed Dec 04 19:40:22 2019 +0100
files:       src/Pure/Concurrent/consumer_thread.scala
description:
clarified messages streaming (again, amending 5ea3ed3c52b3): avoid too many
small messages stacking up, e.g. when loading HOL-Analysis.Analysis.thy into
Isabelle/jEdit;


	Makarius


More information about the isabelle-dev mailing list