Email Gateway (Aug 22 2022 at 19:31): Email Gateway (Aug 22 2022 at 19:31):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
In what respect is Isabelle moving away from Vim?
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.
So what is it that is considered bad about Vim and is more and more
avoided by Isabelle?
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 19:32):From: Mathias Fleury <mathias.fleury12@gmail.com>
On 5. Apr 2019, at 13:45, Wolfgang Jeltsch <wolfgang-it@jeltsch.info> wrote:
Am Freitag, den 05.04.2019, 12:21 +0200 schrieb Makarius:
On 12/03/2019 17:15, Wolfgang Jeltsch wrote:
By the way, have there been any attempts so far to integrate
Isabelle into Vim?No, Isabelle is moving in the opposite direction.
In what respect is Isabelle moving away from Vim?
Away from these old single-threaded text editor towards the glorious Prover-IDE infrastructure.
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.So what is it that is considered bad about Vim and is more and more
avoided by Isabelle?
Using your keyboard instead of the mouse ;-)
I am using emacs to edit theory file (with semantic highlighting provided by the Isabelle/VSCode-server), instead of Isabelle/jEdit. Because Isabelle/jEdit crashes around 3 times a day when I use it [1]. My emacs plugin is definitely far from being polished, but it does not crash and it it works with spacemacs if you want to try it out.
Best,
Mathias
[1] I am not claiming that I am using Isabelle in the standard way.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 19:32):From: Makarius <makarius@sketis.net>
Yes, when I started the Isabelle Prover IDE project around 2008, I made
jokes about Eclipse as "16 tons on your desktop" (as in Monty Python).
Now we have a much better platform than Eclipse (Isabelle/jEdit version
11), but it is "32 tons on your desktop".
I did not plan for that weight and gravity, but it is a natural
consequence of a "filthy rich client approach" of IDEs.
Just a few weeks ago, I updated my home machine again after 5 years. For
just 1650 EUR I got:
* 8 CPU cores at 3600 MHz sustained clock frequency without fan noise
(or 4900 MHz with a lot of fan noise)
* 32 GB RAM at 3600 MHz (instead of normal 2666)
* 1000 GB non-volatile RAM (PCIe) for the file-system (not "disk")
Thus the richness of Isabelle can be enjoyed without feeling the weight.
Note that Isabelle has always required serious equipment. I remember
when Proof General 2.0 with XEmacs 21.1 was the great new thing in 1999,
it required hardware for 12000 EUR on the desk, or a big server
somewhere in the back.
Makarius
Email Gateway (Aug 22 2022 at 19:32):From: Makarius <makarius@sketis.net>
It would be still interesting to know why it crashed, and what the
non-standard usage is.
In Isabelle2019, Isabelle/jEdit will be at version 11. It is to be
rock-solid, without crashes.
Makarius
Email Gateway (Aug 22 2022 at 19:32):From: Makarius <makarius@sketis.net>
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.).
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.
Makarius
Email Gateway (Aug 22 2022 at 19:32):From: Peter Lammich <lammich@in.tum.de>
I'm using Isabelle successfully on 2-3 year old laptop machines, for
the last 14 years ... only once, around 2015->2017, I had to update the
RAM of my laptop, to make it work another 1.5 years.
Email Gateway (Aug 22 2022 at 19:32):From: Peter Lammich <lammich@in.tum.de>
the last 14 years ... only once, around 2015->2017, I had to update
I meant 2005->2007 ;)
Email Gateway (Aug 22 2022 at 19:32):From: Lawrence Paulson <lp15@cam.ac.uk>
In fact jEdit has quite a few powerful features. One of my favourites is CMD-8 (presumably CTRL 8 under Linux and Windows) to select the nearest closing set of brackets. I use Markers all the time and have only just discovered Folding, which fully supports Isar and is ideal for hiding giant sub-proofs. There is probably much more, if one takes the trouble to explore.
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC