[Top][All Lists]

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

Re: Beyond release

From: Clément Pit--Claudel
Subject: Re: Beyond release
Date: Mon, 27 Jun 2016 11:52:01 -0400
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

On 2016-06-27 11:33, Andreas Röhler wrote:
> 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?

Yes: Makarius wrote: "While it is technically feasible to connect Proof General 
to Isabelle/Scala/PIDE in some imitation of the old TTY mode, I personally 
don't believe that there are serious adherents to Emacs still around to do 

>> 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?

Does Makarius know Emacs Lisp?

>> 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.

Interesting. I don't know about these things, but I never saw them them 
mentioned (especially the last ones) outside of emacs-devel.

Attachment: signature.asc
Description: OpenPGP digital signature

reply via email to

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