Beyond release

Beyond release

[Andreas Röhler]

Hi Emacs,

while the release of Emacs 25 is pending and not everyone is involved 
fixing remaining bugs, it might be time to reflect what to do afterward.

What about establishing a structured TODO - structured according to 
importance and difficulty?

While Emacs is my editor of choice, it has some serious --and mostly 
unnecessary-- flaws.

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. "policy" means here: how to 
design code and how to deal with bugs.

The most simple but far reaching bug IMO is the inconsistence of 
beginning-of-defun introduced by open-paren-in-column-0-is-defun-start 
and related. It not only makes Emacs Lisp editing somehow 
non-professional, it also affects python.el and seems spread its 
inconsistency beyond, making people believe such things are normal.


Cheers,

Andreas

Re: Beyond release

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 798 bytes --]

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).
AFAICT, Isabelle moved to jEdit because that's what the authors liked programming in, 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?
Clément.


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: Beyond release

[Andreas Röhler]

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.

Re: Beyond release

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 1871 bytes --]

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

>> 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 #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: Beyond release

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 346 bytes --]

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

Also: Makarius is a co-author of jEdit.


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: Beyond release

[Dmitry Gutov]

On 06/27/2016 06:52 PM, Clément Pit--Claudel wrote:

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

Until someone presents concrete evidence, this is just FUD. You can pay 
it no attention.

Re: Beyond release

[Andreas Röhler]

On 27.06.2016 17:52, Clément Pit--Claudel wrote:
> 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 that."

In which way that would contradict my saying? BTW still believing Emacs 
is a suitable tool in logic programming.

Re: Beyond release

[Andreas Röhler]

On 27.06.2016 18:10, Dmitry Gutov wrote:
> On 06/27/2016 06:52 PM, Clément Pit--Claudel wrote:
>
>>> 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.
>
> Until someone presents concrete evidence, this is just FUD. You can 
> pay it no attention.
>

syntax-propertize-function:

" ...
The specified function may call ‘syntax-ppss’ on any position
before END, but it should not call ‘syntax-ppss-flush-cache’,
which means that it should not call ‘syntax-ppss’ on some
position and later modify the buffer on some earlier position."

Source of

(defun syntax-ppss (&optional pos)
   " [ ... ]"
   ;; Default values.
   (unless pos (setq pos (point)))
   (syntax-propertize pos)
   ...

Re: Beyond release

[Phillip Lord]

Clément Pit--Claudel <clement.pit@gmail.com> writes:

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


I'm guessing that Isabelle/Emacs integration used "parsing output"
interaction. FWIW, I think that the days of this form of archictecture
are numbered. Both scala and clojure interaction now use something with
a structured protocol, with a specialized server on the scala or clojure
side. A similar thing is happening with R, also, and maybe with JDEE.

I don't know if anything could be done, but adding general support for
repl interaction to core or ELPA would probably be a good thing. I don't
know if it is possible -- most of the tools that I have mentioned so far
use different protocols, so perhaps it is not.


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

Which is the problem. You don't need to ask if he knows Java, because
everyone knows Java.

Phil

Re: Beyond release

[Dmitry Gutov]

On 06/27/2016 07:25 PM, Andreas Röhler wrote:

>> Until someone presents concrete evidence, this is just FUD. You can
>> pay it no attention.
>>
>
> syntax-propertize-function:

Quotes from Emacs's source code are not sufficient evidence of your claims.

Re: Beyond release

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 445 bytes --]


On 2016-06-27 12:40, Phillip Lord wrote:
>>> >> 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?
>>
> Which is the problem. You don't need to ask if he knows Java, because
> everyone knows Java.

I think the major factor here was also that Makarius is a developer of jEdit.


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: Beyond release

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 1356 bytes --]

On 2016-06-27 12:40, Phillip Lord wrote:
> I'm guessing that Isabelle/Emacs integration used "parsing output"
> interaction. FWIW, I think that the days of this form of archictecture
> are numbered. Both scala and clojure interaction now use something with
> a structured protocol, with a specialized server on the scala or clojure
> side. A similar thing is happening with R, also, and maybe with JDEE.

And with Coq, another proof assistant that still uses Emacs as its main IDE. We're currently working on porting Proof General to use Coq's structured protocol.

> I don't know if anything could be done, but adding general support for
> repl interaction to core or ELPA would probably be a good thing. I don't
> know if it is possible -- most of the tools that I have mentioned so far
> use different protocols, so perhaps it is not.

Do you really mean REPL interaction? If so, comint-mode does exactly this, I think :)
But if you meant structured protocols, then it's tricky; there's indeed a large variety of protocols. The main pain point when developing those (based on limited experience developing Emacs modes for Dafny, F* and Coq — which all use different protocols) is asynchronicity; you end up registering timers to delay certain actions or implement queues, and it's pretty tricky to keep the code organized properly. 


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: Beyond release

[Andreas Röhler]

On 27.06.2016 18:55, Dmitry Gutov wrote:
> On 06/27/2016 07:25 PM, Andreas Röhler wrote:
>
>>> Until someone presents concrete evidence, this is just FUD. You can
>>> pay it no attention.
>>>
>>
>> syntax-propertize-function:
>
> Quotes from Emacs's source code are not sufficient evidence of your 
> claims.
>

Not if you snip a relevant part.

(defun syntax-propertize (pos)
   "Ensure that syntax-table properties are set until POS (a buffer point)."
   (when (< syntax-propertize--done pos)
     (if (null syntax-propertize-function)
         (setq syntax-propertize--done (max (point-max) pos))
       ;; (message "Needs to syntax-propertize from %s to %s"
       ;;          syntax-propertize--done pos)
       (set (make-local-variable 'parse-sexp-lookup-properties) t)
       (save-excursion
         (with-silent-modifications ...

where

(if (null syntax-propertize-function)

wouldn't pos a problem.

However, when called from syntax-propertize-function, this certainly 
wont be null, then the propertize-branch is entered. Might the branches 
be simple bound wrong, i.e. reverse?

Re: Beyond release

[Dmitry Gutov]

On 06/27/2016 09:10 PM, Andreas Röhler wrote:

> Not if you snip a relevant part.

Everybody has read it already.

Yes, syntax-ppss can be called recursively. No, it's not proof that it's 
"slow", for any meaningful definition of "slow".

> However, when called from syntax-propertize-function, this certainly
> wont be null, then the propertize-branch is entered. Might the branches
> be simple bound wrong, i.e. reverse?

How to report bugs effectively:

http://www.chiark.greenend.org.uk/~sgtatham/bugs.html

Re: Beyond release

[Alan Mackenzie]

Hello, Andreas.

On Mon, Jun 27, 2016 at 08:10:25PM +0200, Andreas Röhler wrote:


> On 27.06.2016 18:55, Dmitry Gutov wrote:
> > On 06/27/2016 07:25 PM, Andreas Röhler wrote:

> >>> Until someone presents concrete evidence, this is just FUD. You can
> >>> pay it no attention.


> >> syntax-propertize-function:

> > Quotes from Emacs's source code are not sufficient evidence of your 
> > claims.

They can be.  Or they can be very powerful supporting evidence.

> Not if you snip a relevant part.

Indeed not.

> (defun syntax-propertize (pos)
>    "Ensure that syntax-table properties are set until POS (a buffer point)."
>    (when (< syntax-propertize--done pos)
>      (if (null syntax-propertize-function)
>          (setq syntax-propertize--done (max (point-max) pos))
>        ;; (message "Needs to syntax-propertize from %s to %s"
>        ;;          syntax-propertize--done pos)
>        (set (make-local-variable 'parse-sexp-lookup-properties) t)
>        (save-excursion
>          (with-silent-modifications ...

> where

> (if (null syntax-propertize-function)

> wouldn't pos a problem.

> However, when called from syntax-propertize-function, this certainly 
> wont be null, .....

It might well be when syntax-propertize is called directly from
syntax-ppss.  This happens even when syntax-propertize-function is nil.

> .... then the propertize-branch is entered. Might the branches be
> simple bound wrong, i.e. reverse?

No, I don't think so.  syntax-propertize--done is supposed to be the
marker of upper limit of where the properties are valid.  In the case
where there's no syntax-propertize-function, one might as well set this
to a high value, which likely prevents syntax-propertize being called too
often.

-- 
Alan Mackenzie (Nuremberg, Germany).

Re: Beyond release

[Phillip Lord]

Clément Pit--Claudel <clement.pit@gmail.com> writes:

> On 2016-06-27 12:40, Phillip Lord wrote:
>> I'm guessing that Isabelle/Emacs integration used "parsing output"
>> interaction. FWIW, I think that the days of this form of archictecture
>> are numbered. Both scala and clojure interaction now use something with
>> a structured protocol, with a specialized server on the scala or clojure
>> side. A similar thing is happening with R, also, and maybe with JDEE.
>
> And with Coq, another proof assistant that still uses Emacs as its main IDE.
> We're currently working on porting Proof General to use Coq's structured
> protocol.

Ah, didn't know that.


>> I don't know if anything could be done, but adding general support for
>> repl interaction to core or ELPA would probably be a good thing. I don't
>> know if it is possible -- most of the tools that I have mentioned so far
>> use different protocols, so perhaps it is not.
>
> Do you really mean REPL interaction? If so, comint-mode does exactly this, I
> think :)

Yeah, didn't put that very carefully. I meant "the sort of things that
in the past, we used to do my passing stuff to a REPL and parsing the
results". I.e. not REPL interaction.


> But if you meant structured protocols, then it's tricky; there's indeed a
> large variety of protocols. The main pain point when developing those (based
> on limited experience developing Emacs modes for Dafny, F* and Coq — which all
> use different protocols) is asynchronicity; you end up registering timers to
> delay certain actions or implement queues, and it's pretty tricky to keep the
> code organized properly.

CIDER uses call-backs, which seems to work okay, and is reasonably easy
to implement with closures.

How much of this could be made generic, I don't know. There are
definately some overlapping issues, though. Asynchronous callbacks are a
little hard to implement and debug, so providing way of making
call-backs that log might be nice.

I'll have a think on it.

PHil

Re: Beyond release

[Andreas Röhler]

On 27.06.2016 21:55, Dmitry Gutov wrote:
> On 06/27/2016 09:10 PM, Andreas Röhler wrote:
>
>> Not if you snip a relevant part.
>
> Everybody has read it already.
>
> Yes, syntax-ppss can be called recursively. 

It's not about that. It's about circular calls between 
syntax-propertize-function and syntax-ppss.


> No, it's not proof that it's "slow", for any meaningful definition of 
> "slow".
>
>> However, when called from syntax-propertize-function, this certainly
>> wont be null, then the propertize-branch is entered. Might the branches
>> be simple bound wrong, i.e. reverse?
>
> How to report bugs effectively:
>
> http://www.chiark.greenend.org.uk/~sgtatham/bugs.html

A design flaw is not a bug yet, but might source a bunch of bugs. Please 
search for slowness and Emacs, you should receive enough entries which 
deserve thinking about.

Re: Beyond release

[Andreas Röhler]

On 27.06.2016 22:29, Alan Mackenzie wrote:
[ ... ]
> In the case
> where there's no syntax-propertize-function, one might as well set this
> to a high value, which likely prevents syntax-propertize being called too
> often.
>

Hmm, sounds like Emacs may take profit of abstractions, which "have an 
associated entropy value that measures their degree of indeterminacy or 
information content.":)

Re: Beyond release

[Dmitry Gutov]

On 06/28/2016 09:14 AM, Andreas Röhler wrote:

>> Yes, syntax-ppss can be called recursively.
>
> It's not about that. It's about circular calls between
> syntax-propertize-function and syntax-ppss.

That's what I said.

>> How to report bugs effectively:
>>
>> http://www.chiark.greenend.org.uk/~sgtatham/bugs.html
>
> A design flaw is not a bug yet, but might source a bunch of bugs.

For "design flaws", the burder of proof is even higher than for simple 
bugs. You can't simply claim that the design is flawed without giving 
concrete evidence.