Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle and Vim


view this post on Zulip Email Gateway (Aug 22 2022 at 19:33):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Am Freitag, den 05.04.2019, 15:14 +0200 schrieb Makarius:

On 05/04/2019 13:45, Wolfgang Jeltsch wrote:

I like Vim particularly for its efficient editing capabilities,
things like jumping to the matching bracket or deleting everything
enclosed by the quotation marks to the left and right of the cursor,
all of which doesn’t involve complicated key combinations. I guess
the goal is not to make Isabelle editing less efficient.

Such basic editing facilities can still be added to the jEdit text
editor, by working with the (rather small) developer group at
SourceForge. I do this occasionally, but only for really important
things (like updates to HiDPI displays, updates to Java 11 etc.).

I doubt that Vim-style editing can be reasonably added to any
“mainstream” editor or IDE, as these tools typically don’t distinguish
between different modes. Vim’s distinction between normal mode (for
commands) and insert mode (for entering text) is crucial, as it allows
commands to be entered mostly by single key presses, avoiding things
like Ctrl + Shift + ….

Isabelle/PIDE is not so much a text editor, than a semantic IDE.
Editing is important, but not the key thing. For example, when I use
IntelliJ IDEA, I hardly know (and hardly care) about its editing
functions, and still manage to work on large Scala projects smoothly.

Before I started using Vim, I also didn’t care so much about editing
features. Now that I’ve realized how efficient your editing can be with
Vim, it can get quite annoying for me not to have such features. The
broad acceptance of more “mainstream” editors may have to do with the
fact that many people never got into advanced editing so much and thus
don’t know what they miss. Even many Vim users have an editing style
that stays way behind what is possible with Vim.

All the best,
Wolfgang

view this post on Zulip Email Gateway (Aug 22 2022 at 19:33):

From: "Berg, Nils Erik" <nils.jaehnig@tu-berlin.de>
Hi Wolfgang,

I really recommend you try VSCode with the Vim plugin.
I only use basic features of Vim, so I can't speak about more advanced functionality.

In general, Isabelle in VSCode is quite good. Sometimes I miss something (or did not search long enough) like e.g. the search functionality, an overview over the status of all the theory.
For those things, I switch to jedit.

My only pain point is currently that the pretty symbols plugin is sometimes very slow.

But all in all very usable and you can edit Vim-style.

Best
Nils

view this post on Zulip Email Gateway (Aug 22 2022 at 19:33):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi, Nils!

Thanks for the recommendation. I might give VSCode a try.

All the best,
Wolfgang

view this post on Zulip Email Gateway (Aug 22 2022 at 19:33):

From: Makarius <makarius@sketis.net>
On 05/04/2019 16:11, Wolfgang Jeltsch wrote:

I doubt that Vim-style editing can be reasonably added to any
“mainstream” editor or IDE, as these tools typically don’t distinguish
between different modes. Vim’s distinction between normal mode (for
commands) and insert mode (for entering text) is crucial, as it allows
commands to be entered mostly by single key presses, avoiding things
like Ctrl + Shift + ….

I also doubt that, and Isabelle is moving in the opposite direction.

Before I started using Vim, I also didn’t care so much about editing
features. Now that I’ve realized how efficient your editing can be with
Vim, it can get quite annoying for me not to have such features. The
broad acceptance of more “mainstream” editors may have to do with the
fact that many people never got into advanced editing so much and thus
don’t know what they miss. Even many Vim users have an editing style
that stays way behind what is possible with Vim.

That is all very alien to the Isabelle/PIDE approach (and of other
high-end ideas). Ultimately there is a static type error here, talking
about quite different things.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 19:33):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Efficient editing and good semantic IDE support are different things,
but they are not contradictory but in fact complement each other.
Unfortunately we seem to have only tools these days that are good in at
most one of those things.

All the best,
Wolfgang

view this post on Zulip Email Gateway (Aug 22 2022 at 19:36):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,

On 5. Apr 2019, at 16:23, Berg, Nils Erik <nils.jaehnig@tu-berlin.de> wrote:

Hi Wolfgang,

I really recommend you try VSCode with the Vim plugin.
I only use basic features of Vim, so I can't speak about more advanced functionality.

In general, Isabelle in VSCode is quite good. Sometimes I miss something (or did not search long enough) like e.g. the search functionality,

an overview over the status of all the theory.

I have a patch to add the overview (attached the version for Isabelle2018*). It requires a change in the plugin and in the Isabelle server. Basically apply the patch in the Isabelle repo, compile and install the plugin, and run VSCode with it.

For those things, I switch to jedit.

My only pain point is currently that the pretty symbols plugin is sometimes very slow.

Out of curiosity, are you impacted by https://github.com/siegebell/vsc-prettify-symbols-mode/issues/41 <https://github.com/siegebell/vsc-prettify-symbols-mode/issues/41>? I opened that issue and decided some times later that the plugin was too buggy to be usable, especially on large files.

Best,
Mathias

But all in all very usable and you can edit Vim-style.

Best
Nils

On 5. Apr 2019, at 16:15, Wolfgang Jeltsch <wolfgang-it@jeltsch.info> wrote:

Am Freitag, den 05.04.2019, 15:14 +0200 schrieb Makarius:

On 05/04/2019 13:45, Wolfgang Jeltsch wrote:

I like Vim particularly for its efficient editing capabilities,
things like jumping to the matching bracket or deleting everything
enclosed by the quotation marks to the left and right of the cursor,
all of which doesn’t involve complicated key combinations. I guess
the goal is not to make Isabelle editing less efficient.

Such basic editing facilities can still be added to the jEdit text
editor, by working with the (rather small) developer group at
SourceForge. I do this occasionally, but only for really important
things (like updates to HiDPI displays, updates to Java 11 etc.).

I doubt that Vim-style editing can be reasonably added to any
“mainstream” editor or IDE, as these tools typically don’t distinguish
between different modes. Vim’s distinction between normal mode (for
commands) and insert mode (for entering text) is crucial, as it allows
commands to be entered mostly by single key presses, avoiding things
like Ctrl + Shift + ….

Isabelle/PIDE is not so much a text editor, than a semantic IDE.
Editing is important, but not the key thing. For example, when I use
IntelliJ IDEA, I hardly know (and hardly care) about its editing
functions, and still manage to work on large Scala projects smoothly.

Before I started using Vim, I also didn’t care so much about editing
features. Now that I’ve realized how efficient your editing can be with
Vim, it can get quite annoying for me not to have such features. The
broad acceptance of more “mainstream” editors may have to do with the
fact that many people never got into advanced editing so much and thus
don’t know what they miss. Even many Vim users have an editing style
that stays way behind what is possible with Vim.

All the best,
Wolfgang

view this post on Zulip Email Gateway (Aug 22 2022 at 19:37):

From: "Berg, Nils Erik" <nils.jaehnig@tu-berlin.de>
Hi Mathias,

I am not completely sure, whether I have the same issue (I did not relate it to hovering).
However, the slowness of prettify-symbols seems to be related to a lot of theory files, even if they are not opened for viewing or editing.
So I think, your proposed solution might fix my problem.

And thank you for the overview plugin! I will try it sometime in the future when I upgrade my theories from Isabelle 2017.

Best
Nils

view this post on Zulip Email Gateway (Aug 22 2022 at 19:37):

From: Makarius <makarius@sketis.net>
On 08/04/2019 11:20, Mathias Fleury wrote:

I have a patch to add the overview (attached the version for Isabelle2018*). It requires a change in the plugin and in the Isabelle server. Basically apply the patch in the Isabelle repo, compile and install the plugin, and run VSCode with it.

I have seen your add-ons to Isabelle/VSCode already some months ago on
the Net, before you've sent me a private mail recently.

It is definitely important to do something here, and I marked it on my
TODO list as something to be inspected for the Isabelle2019.

It's just that I did not manage to get back to Isabelle/VSCode yet:
there are still pending problems with more fundamental infrastructure
that has higher priority (final polishing on polyml-5.8 in particular).

My only pain point is currently that the pretty symbols plugin is sometimes very slow.

Out of curiosity, are you impacted by https://github.com/siegebell/vsc-prettify-symbols-mode/issues/41 <https://github.com/siegebell/vsc-prettify-symbols-mode/issues/41>? I opened that issue and decided some times later that the plugin was too buggy to be usable, especially on large files.

This project has not seen activity in approx. 1 year.

Generally, my impression is that the approach should be as in
Isabelle/jEdit: actual replacement of symbols when source is loaded, and
the reverse operation for saving. It will require more tinkering with
VSCode, though, and this is definitely not going to happen for the
Isabelle2019 release.

Makarius


Last updated: Apr 24 2024 at 12:33 UTC