[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