Chengsong Tan (Oct 22 2020 at 20:15): Chengsong Tan (Oct 22 2020 at 20:15):Hello everyone! I am new to Isabelle, and am currently
familiarising myself with the basics of proving things.
One of the annoying things I found in using Isabelle is editing: it is a pain
for me to navigate in the jEdit editing interface, especially
doing things like adding parenthesis around expressions
to make sure there are no operator priority issues etc.
Are there any plugins that allow you to edit
in your familiar editor(vim/ emacs etc.) within the console?
Any info on this is appreciated. Thanks in advance!
Mathias Fleury (Oct 23 2020 at 04:48):The TextMate plugin reduces the pain to add parentheses around expression in jEdit (but it is more stupid than the emacs counterpart)
Chengsong Tan (Oct 23 2020 at 11:36):Mathias Fleury said:
The TextMate plugin reduces the pain to add parentheses around expression in jEdit (but it is more stupid than the emacs counterpart)
Thanks! I will try that out!
Also just read from the Isabelle tutorial
https://isabelle.in.tum.de/doc/tutorial.pdf
that you can use the Proof General.
It uses emacs as editor, which I have to learn if
I want to use it( I mainly use vim for code writing).
If the plugin TextMate is good I will just stick to that:)
Mathias Fleury (Oct 23 2020 at 11:51):No, PG is gone since Isabelle 2014 (or 2015, I don't remember)
Chengsong Tan (Oct 23 2020 at 11:52):Mathias Fleury said:
The TextMate plugin reduces the pain to add parentheses around expression in jEdit (but it is more stupid than the emacs counterpart)
Somehow I can't find the plugin called TextMate in the plugin manager list.
Are you referring to this repository?
https://github.com/lsf37/Isabelle.tmbundle
Mathias Fleury (Oct 23 2020 at 11:53):No it is a jedit thing, in the plugin manager
Mathias Fleury (Oct 23 2020 at 11:53):sorry FirstMate
Mathias Fleury (Oct 23 2020 at 11:53):Plugin > Plugin manager > Install > FirstMate
Chengsong Tan (Oct 23 2020 at 11:54):Mathias Fleury said:
No, PG is gone since Isabelle 2014 (or 2015, I don't remember)
But strangely it still appears in the 2020 version of tutorial for Isabelle!
(Just open the link and search for "proof general"
Chengsong Tan (Oct 23 2020 at 11:55):Mathias Fleury said:
sorry FirstMate
Yep! That plugin I can find.
Will try that out and tell my experience.
Chengsong Tan (Oct 23 2020 at 11:55):Thanks a lot!
Mathias Fleury (Oct 23 2020 at 11:57):If you feel very like adventurous, I have an emacs mode for Isabelle that uses Isabelle LSP server (and it works with spacemacs too).
Disclaimer: It is my side project; it is rough, the documentation is scarce and continuously outdated.
Chengsong Tan (Oct 23 2020 at 15:46):Mathias Fleury said:
If you feel very like adventurous, I have an emacs mode for Isabelle that uses Isabelle LSP server (and it works with spacemacs too).
Disclaimer: It is my side project; it is rough, the documentation is scarce and continuously outdated.
Thanks for the recommendation!
Looks pretty cool!
Interestingly I found this 2020 version of proof general on MELPA
https://melpa.org/#/proof-general
I am going to try out both.
Mathias Fleury (Oct 23 2020 at 15:47):PG still works for Coq and other systems, but Isabelle support of PG was removed
Mathias Fleury (Oct 23 2020 at 15:49):But you might be the chosen one that can write correct Isabelle theories without any feedback from the prover. I don't believe this is possible, but I have no proof of that :grinning:
Kevin Kappelmann (Oct 26 2020 at 07:47):I used vim for years, but getting vim-like editing into jedit is even more unrealistic than getting emacs like editing. So I decided to pick up some emacs at some point and tweak jedit to emulate emacs as far as I can. I ended up with some emacs like editing but the shortcuts sometimes got inspired by my vim history. Here is my config: kevin_emacs_keys.props .
Here is my list of plugins.
In addition, I installed these emacs macros.
I also sometimes use the macro recording feature of jedit to create new macros, like "create a new theory file called Scratch that imports Main".
Kevin Kappelmann (Oct 26 2020 at 07:50):All in all, it is a much better experience now. The only thing I still hate is that I have to use "CTRL+click" to follow a reference/link and I don't know how put a keybinding on that action :exhausted:
Kevin Kappelmann (Oct 26 2020 at 07:50):Please help me if you know how to
Manuel Eberl (Oct 26 2020 at 07:57):Have you asked Makarius on the mailing list?
Kevin Kappelmann (Oct 26 2020 at 08:02):I asked him in person 1 year ago but to no avail
Gergely Buday (Jan 22 2021 at 08:35):Isabelle is not for such low-level editors and the priority issues do not go away by an editor.
If you want something familiar then you can use VS Code:
https://marketplace.visualstudio.com/items?itemName=makarius.isabelle
Last updated: Dec 21 2024 at 16:20 UTC