Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-08 Thread Thomas Sewell
Thanks Makarius. A few of us at NICTA have ported this change to our various versions of Isabelle and begun playing with it. It seems to improve the situation sometimes, though we haven't yet got a feel for when in particular it helps. In fact, we haven't really understood what the change

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-08 Thread Makarius
On Thu, 8 May 2014, Thomas Sewell wrote: If I knew a proper way to reduce the priority (or to pre-empt) worker threads for that, I would do it. But it probably needs some work by David Matthews on the ML thread infrastructure. Consider me an unashamed pragmatist. The important point is

[isabelle-dev] Isabelle root access

2014-05-08 Thread Makarius
On Thu, 8 May 2014, mta-proj wrote: die Gruppe isabelle, in der Sie Mitglied sind, wurde mit desharna,fleury erweitert Membership of the isabelle Unix group means full root access to many administrative resources. Usually neither the one who grants the rights nor the one who receives them

Re: [isabelle-dev] Isabelle root access

2014-05-08 Thread Jasmin Christian Blanchette
Hi Makarius, Am 08.05.2014 um 12:32 schrieb Makarius makar...@sketis.net: On Thu, 8 May 2014, mta-proj wrote: die Gruppe isabelle, in der Sie Mitglied sind, wurde mit desharna,fleury erweitert Membership of the isabelle Unix group means full root access to many administrative

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-08 Thread David Matthews
On 08/05/2014 11:25, Makarius wrote: On Thu, 8 May 2014, Thomas Sewell wrote: If I knew a proper way to reduce the priority (or to pre-empt) worker threads for that, I would do it. But it probably needs some work by David Matthews on the ML thread infrastructure. Preempting long-running