Julin Shaji (Feb 14 2025 at 06:30): Julin Shaji (Feb 14 2025 at 06:30):Is it possible to use an editor other than jedit for interacting with isabelle?
So that we can use the features of an editor that we are already familiar with instead of having to learn jedit as well.
For example, it took some time before I realized that redo in jedit is C-e C-z.
I suppose emacs support used to exist?
https://homepages.inf.ed.ac.uk/da/Isamode/doc/Isamode_1.html
Found this as well:
https://github.com/m-fleury/isabelle-emacs
Also found a post here about a vscode extension.
#General > Isabelle/VSCode in Isabelle2025-RC0
Along with this vim plugin which looks unmaintained:
https://github.com/ThreeFx/isabelle.vim
And I suppose this is an eclipse extension:
http://andriusvelykis.github.io/isabelle-eclipse/getting-started/
Christian Pardillo Laursen (Feb 14 2025 at 12:57):I'd say vscode is your best bet - command isabelle vscode should get you started
Julin Shaji (Feb 14 2025 at 13:11):I tried isabelle vscode but couldn't figure out where to see the proof
state.
Have anyone here used it?
Mathias Fleury (Feb 14 2025 at 18:35):The short version of the story: back in the days there was ProofGeneral for Emacs. Makarius created Isabelle/jEdit and decided at some point that maintaining both was too hard so only Isabelle/jEdit remained.
Then at some point he got money from someone (I don't remember), but developed an LSP server for Isabelle and the VSCode plugin to connect to the LSP server.
This LSP server is the only alternative today to Isabelle/jEdit. There are three editors supporting it: VScode and Emacs and vim. For practical reasons (some missing feature in LSP I wanted to have), I have a slightly changed Isabelle (meaning only in the LSP server). Not much has changed, so I assume that the vim plugin is still working. Emacs is still working. But I did not have time to port that to Isabelle2025-RC2
There was a bachelor thesis at TUM that re-developped some of the features I had and put them into Isabelle, but this is also on my todo list.
Mathias Fleury (Feb 14 2025 at 18:35):Julin Shaji said:
I tried
isabelle vscodebut couldn't figure out where to see the proof
state.Have anyone here used it?
You have the output panel at the bottom that you have to open
Julin Shaji (Feb 17 2025 at 10:25):Mathias Fleury said:
You have the output panel at the bottom that you have to open
Ah.. I see it now.
Julin Shaji (Feb 17 2025 at 10:26):Mathias Fleury said:
Emacs is still working
Is it still used via proof general? Quite a few tutorials mention proof general, but I was not sure if it was beause they were old.
Mathias Fleury (Feb 17 2025 at 17:48):no, it is also using the LSP. PG is dead forever and cannot be resurrected without heavy changes to Isabelle
Julin Shaji (Feb 18 2025 at 06:19):Mathias Fleury said:
no, it is also using the LSP. PG is dead forever and cannot be resurrected without heavy changes to Isabelle
Okay, so I suppose there is no specific emacs mode for use with isabelle? Just use LSP?
Julin Shaji (Feb 18 2025 at 06:19):Or is this meant to be such a mode?
https://github.com/m-fleury/isabelle-emacs
Mathias Fleury (Feb 18 2025 at 06:41):Isabelle uses LSP extension for various things, including the proof goal, syntax highlighting, the theory panel (progress bar on the right)
Mathias Fleury (Feb 18 2025 at 06:43):this indeed hooks into the LSP mode from emacs to add the new functionality
Mathias Fleury (Feb 18 2025 at 06:46):And you probably want to see nice symbols instead of \<open> and some help typing those, so https://github.com/m-fleury/isar-mode is also useful here
Mathias Fleury (Feb 18 2025 at 06:47):(disclaimer in case it was not obvious from the name: I am the author of the isabelle integration)
Moritz R (Feb 18 2025 at 17:07):For Isabelle/vscode you can either open the Terminal (click Terminal -> New Terminal) and have the proof state show up under "ISABELLE: OUTPUT" (after setting Editor_output_state to true in the isabelle-extension settings), or you can open a state panel via
clicking View -> Command Palette -> Isabelle: Show state and then putting the cursor into some non-trivial proof state
Last updated: Mar 09 2025 at 12:28 UTC