[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Beyond release

From: Andreas Röhler
Subject: Re: Beyond release
Date: Mon, 27 Jun 2016 17:33:22 +0200
User-agent: Mozilla/5.0 (X11; Linux i686; rv:45.0) Gecko/20100101 Icedove/45.1.0

On 27.06.2016 16:18, Clément Pit--Claudel wrote:
On 2016-06-27 05:58, Andreas Röhler wrote:
To make clear, that's not just a personal view, please consider the
withdraw of advanced and promising theorem prover Isabelle/HOL, which
doesn't longer support Emacs, while relying on it before. BTW that
withdraw was in time, before John took over and AFAIU caused by a
policy, which hopefully is abandoned now.
I think that's an incorrect characterisation (see statements that Makarius made 
on the Proof General mailing list).

That's where my conclusions are from. Any precise spot to tell otherwise?

AFAICT, Isabelle moved to jEdit because that's what the authors liked 
programming in

That's interesting. Maybe that would also worth being reflected. So extending in Java should be easier than in Emacs Lisp? How could it came to this?

, and because they didn't particularly care about Emacs support — which did 
cause some frustration in the Isabelle community, btw.

What elements make you think Emacs policies had anything to do with it?

There are several. Think alone the matter of slowness, mentioned again and again in bug-reports and development. AFAIU these slowness is caused by bugs and design flaws, not by Emacs Lisp as such. The introduction of circular dependencies WRT syntax-ppss probably deserves being mentioned in this context. Propertize functions are encouraged to call syntax-ppss while syntax-ppss itself propertizes.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]