Emacs and jEdit

Emacs and jEdit

[Andreas Röhler]

[-- Attachment #1: Type: text/plain, Size: 237 bytes --]

Hi all,

mentioned the switch of Isabelle/HOL from Emacs to jEdit.

Attach a showcase displaying a portion of source in Emacs and jEdit, 
which should illustrate the matter. sml.png refers to sml-mode.el from 
Melpa.

Cheers,

Andreas



[-- Attachment #2: jedit.png --]
[-- Type: image/png, Size: 121519 bytes --]

[-- Attachment #3: sml.png --]
[-- Type: image/png, Size: 149131 bytes --]

Re: Emacs and jEdit

[Kaushal Modi]

[-- Attachment #1: Type: text/plain, Size: 851 bytes --]

Hi Andreas,

I didn't quite follow that email.

What is Isabelle/HOL? Do the screenshots illustrate that jEdit can render
Isabelle files fine, but emacs does not?

Is this a request for a new major mode in emacs to support Isabelle?

Or was this supported earlier and is now broken?

On Mon, Jul 18, 2016, 6:17 AM Andreas Röhler <andreas.roehler@online.de>
wrote:

> Hi all,
>
> mentioned the switch of Isabelle/HOL from Emacs to jEdit.
>
> Attach a showcase displaying a portion of source in Emacs and jEdit,
> which should illustrate the matter.



sml.png refers to sml-mode.el from
> Melpa.
>

I'll assume that the emacs screenshot is sml.png :) I do not see that file
names in my email client, just the images directly. So the sml-mode was
supposed to render the tags in that file properly?

> --

Kaushal Modi

[-- Attachment #2: Type: text/html, Size: 1656 bytes --]

Re: Emacs and jEdit

[Andreas Röhler]

[-- Attachment #1: Type: text/plain, Size: 1586 bytes --]



On 18.07.2016 14:11, Kaushal Modi wrote:
> Hi Andreas,
>
> I didn't quite follow that email.
>
> What is Isabelle/HOL?

Isabelle/HOL is a theorem prover, used to prove the correctness of code 
for example.
Like Coq or ACL2.


> Do the screenshots illustrate that jEdit can render Isabelle files 
> fine, but emacs does not?

To the extend shown, that's the purpose.

>
> Is this a request for a new major mode in emacs to support Isabelle?

It is an renewed alert. Already mentioned circular dependencies related 
to syntax-propertize for example, which make this section hard to debug 
and maintain. Also think the smie-stuff might be considered as failing.

>
> Or was this supported earlier and is now broken?

It was supported inside proof-general. But support was withdrawn from 
Isabelle/HOL's side, going frustrated by ongoing difficulties IIUC.


>
> On Mon, Jul 18, 2016, 6:17 AM Andreas Röhler 
> <andreas.roehler@online.de <mailto:andreas.roehler@online.de>> wrote:
>
>     Hi all,
>
>     mentioned the switch of Isabelle/HOL from Emacs to jEdit.
>
>     Attach a showcase displaying a portion of source in Emacs and jEdit,
>     which should illustrate the matter. 
>
>
>
>     sml.png refers to sml-mode.el from
>     Melpa.
>
>
> I'll assume that the emacs screenshot is sml.png :)

Right.

> I do not see that file names in my email client, just the images 
> directly. So the sml-mode was supposed to render the tags in that file 
> properly?
>
> -- 
>
> Kaushal Modi
>

Yes. Isabelle/HOL uses an dialect of SML internally, files are indicated 
by the ending ".thy"

[-- Attachment #2: Type: text/html, Size: 4149 bytes --]

Re: Emacs and jEdit

[Stefan Monnier]

> It was supported inside proof-general. But support was withdrawn from
> Isabelle/HOL's side, going frustrated by ongoing difficulties IIUC.

Huh?  Isabelle/HOL developed a fancier protocol/interface for its
various IDEs.  Noone was interested in updating the Emacs-side support
(within Proof-General) to use this new protocol (it required
a significant rewrite because the new protocol works completely
differently).  Then Isabelle/HOL decided to drop support for the old
protocol (at that point only used for Emacs, and the lack of interest in
adapting Emacs's support to the new protocol being taken as a sign that
there weren't enough Emacs users to bother maintaining support for the
old protocol inside Isabelle/HOL).

I can't see any "ongoing difficulties" there.

FWIW, Coq has introduced similarly fancier protocols and since there are
more Emacs+Coq users, some people have taken on the task of updating
Emacs's support (in Proof-General) to use that new protocol (still
ongoing work, AFAIK).  And that work might actually prove useful to
re-introduce Isabelle/HOL support in there, tho that will depend on
whether there's enough motivation for someone to do that part of
the work.


        Stefan

Re: Emacs and jEdit

[Andreas Röhler]

On 18.07.2016 16:56, Stefan Monnier wrote:
>> It was supported inside proof-general. But support was withdrawn from
>> Isabelle/HOL's side, going frustrated by ongoing difficulties IIUC.
> Huh?  Isabelle/HOL developed a fancier protocol/interface for its
> various IDEs.  Noone was interested in updating the Emacs-side support
> (within Proof-General) to use this new protocol (it required
> a significant rewrite because the new protocol works completely
> differently).  Then Isabelle/HOL decided to drop support for the old
> protocol (at that point only used for Emacs, and the lack of interest in
> adapting Emacs's support to the new protocol being taken as a sign that
> there weren't enough Emacs users to bother maintaining support for the
> old protocol inside Isabelle/HOL).
>
> I can't see any "ongoing difficulties" there.
>
> FWIW, Coq has introduced similarly fancier protocols and since there are
> more Emacs+Coq users, some people have taken on the task of updating
> Emacs's support (in Proof-General) to use that new protocol (still
> ongoing work, AFAIK).  And that work might actually prove useful to
> re-introduce Isabelle/HOL support in there, tho that will depend on
> whether there's enough motivation for someone to do that part of
> the work.
>
>
>          Stefan
>
>

Correction taken WRT protocol, thanks. Being interested to take part 
delivering a new port.

Beside sml-mode.el seems to have some issues. IMO one reason is smie 
introducing complexity.

Re: Emacs and jEdit

[Stefan Monnier]

> Beside sml-mode.el seems to have some issues.

Haven't seen any bug reports in a long time.

> IMO one reason is smie introducing complexity.

You're entitled to your opinion, yes.


        Stefan

Re: Emacs and jEdit

[Richard Stallman]

[[[ To any NSA and FBI agents reading my email: please consider    ]]]
[[[ whether defending the US Constitution against all enemies,     ]]]
[[[ foreign or domestic, requires you to follow Snowden's example. ]]]

  > Huh?  Isabelle/HOL developed a fancier protocol/interface for its
  > various IDEs.

Is there a fundamental difficulty in making Emacs support that protocol,
or is it just a matter of work?

-- 
Dr Richard Stallman
President, Free Software Foundation (gnu.org, fsf.org)
Internet Hall-of-Famer (internethalloffame.org)
Skype: No way! See stallman.org/skype.html.

Re: Emacs and jEdit

[Clément Pit--Claudel]

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

On 2016-07-19 06:51, Richard Stallman wrote:
> [[[ To any NSA and FBI agents reading my email: please consider    ]]]
> [[[ whether defending the US Constitution against all enemies,     ]]]
> [[[ foreign or domestic, requires you to follow Snowden's example. ]]]
> 
>   > Huh?  Isabelle/HOL developed a fancier protocol/interface for its
>   > various IDEs.
> 
> Is there a fundamental difficulty in making Emacs support that protocol,
> or is it just a matter of work?

Nothing fundamental; just a matter of work (plus the fact that async stuff in Emacs isn't that easy).
But really, Isabelle is a bad example here: the lead developer of that protocol also works/worked on jEdit.

Clément.


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

Re: Emacs and jEdit

[Andreas Röhler]

On 19.07.2016 08:46, Clément Pit--Claudel wrote:
> On 2016-07-19 06:51, Richard Stallman wrote:
>> [[[ To any NSA and FBI agents reading my email: please consider    ]]]
>> [[[ whether defending the US Constitution against all enemies,     ]]]
>> [[[ foreign or domestic, requires you to follow Snowden's example. ]]]
>>
>>    > Huh?  Isabelle/HOL developed a fancier protocol/interface for its
>>    > various IDEs.
>>
>> Is there a fundamental difficulty in making Emacs support that protocol,
>> or is it just a matter of work?
> Nothing fundamental; just a matter of work (plus the fact that async stuff in Emacs isn't that easy).
> But really, Isabelle is a bad example here: the lead developer of that protocol also works/worked on jEdit.

What about the screenshots given? Seems there is not just async creating 
difficulties.

Re: Emacs and jEdit

[Clément Pit--Claudel]

[-- Attachment #1.1.1: Type: text/plain, Size: 1050 bytes --]

On 2016-07-19 09:08, Andreas Röhler wrote:
> What about the screenshots given? Seems there is not just async creating difficulties.

Why do you attribute Emacs' lack of support for Isabelle's funky format to difficulties, rather than, say, lack of interest?  AFAICT there's only one editor supporting Isabelle, and that's at least in part a design choice (in addition to a custom build of jEdit, the Isabelle people use a custom Isabelle font, and a custom Isabelle encoding based on UTF-8 with subtle, incompatible divergences from the standard).

In any case, I don't think I see anything in these screenshots suggesting difficulties (but I could be wrong).  We've had prettify-symbols-mode for a while, and Proof General had unicode-tokens.el before that.  It would help if you pointed out something that might be hard to support in Emacs.

And if you're interested in areas where we have an edge, I've attached a screenshot of jEdit and Emacs displaying the same text side-by-side. Try to spot an issue on the jEdit side :)

Clément.

[-- Attachment #1.1.2: utf-8.png --]
[-- Type: image/png, Size: 90562 bytes --]

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

Re: Emacs and jEdit

[Andreas Röhler]

On 19.07.2016 09:26, Clément Pit--Claudel wrote:
> On 2016-07-19 09:08, Andreas Röhler wrote:
>> What about the screenshots given? Seems there is not just async creating difficulties.
> Why do you attribute Emacs' lack of support for Isabelle's funky format to difficulties, rather than, say, lack of interest?

Why people used to Emacs' proof-general should prefer jEdit? Why there 
was no interest raised?

For me Emacs' extensibility is the key-argument. While jEdit is 
extensible also. At any case: the basics like indent and highlighting 
must be reliable. Look for example the buglists at elixir-mode:

https://github.com/elixir-lang/emacs-elixir/issues

It's developed for years and are very skilled people behind - 
nonetheless the indent-bugs cumulate.
Well, that's a special smie-matter IIUC.

That good news from there: fontification seems kept under control.

>    AFAICT there's only one editor supporting Isabelle, and that's at least in part a design choice (in addition to a custom build of jEdit, the Isabelle people use a custom Isabelle font, and a custom Isabelle encoding based on UTF-8 with subtle, incompatible divergences from the standard).
The latter might deserve negotiation.

>
> In any case, I don't think I see anything in these screenshots suggesting difficulties (but I could be wrong).

What about the plain text wrongly fontified as keywords?

>    We've had prettify-symbols-mode for a while, and Proof General had unicode-tokens.el before that.  It would help if you pointed out something that might be hard to support in Emacs.

The prettify-stuff works very well in Emacs. Notably flexible.

>
> And if you're interested in areas where we have an edge, I've attached a screenshot of jEdit and Emacs displaying the same text side-by-side. Try to spot an issue on the jEdit side :)
>
> Clément.

Indeed, when playing with jEdit, it showed some bugs too, sure.

Re: Emacs and jEdit

[Clément Pit--Claudel]

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

On 2016-07-19 04:33, Andreas Röhler wrote:
>> In any case, I don't think I see anything in these screenshots suggesting difficulties (but I could be wrong).
> 
> What about the plain text wrongly fontified as keywords?

Sorry, I don't get it. Is there a reason to expect SML-mode to highlight Isabelle code properly?


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

Re: Emacs and jEdit

[Stefan Monnier]

> And if you're interested in areas where we have an edge, I've
> attached a screenshot of jEdit and Emacs displaying the same text
> side-by-side.  Try to spot an issue on the jEdit side :)

Huh?  Why does Emacs use those weird looking drawings instead of the
neatly regular little squares that jEdit displays?
I guess a M-x report-emacs-bug is in order here.


        Stefan

Re: Emacs and jEdit

[Richard Stallman]

[[[ To any NSA and FBI agents reading my email: please consider    ]]]
[[[ whether defending the US Constitution against all enemies,     ]]]
[[[ foreign or domestic, requires you to follow Snowden's example. ]]]

  > > Is there a fundamental difficulty in making Emacs support that protocol,
  > > or is it just a matter of work?

  > Nothing fundamental; just a matter of work (plus the fact that async stuff in Emacs isn't that easy).

That's good, since it gives us an opportunity.  I hope someone will do
this work!

-- 
Dr Richard Stallman
President, Free Software Foundation (gnu.org, fsf.org)
Internet Hall-of-Famer (internethalloffame.org)
Skype: No way! See stallman.org/skype.html.