Stream: Beginner Questions

Topic: Catalogue in vscode


view this post on Zulip Zixuan Fan (Dec 06 2022 at 17:14):

Is it possible to have a catalogue panel in the vscode extension of Isabelle, i.e. showing all lemmata, sections, etc. on the right sidebar in the JEdit.

view this post on Zulip Mathias Fleury (Dec 06 2022 at 17:50):

Maybe I should try to get my patch in the isabelle repo :thinking:

view this post on Zulip Mathias Fleury (Dec 06 2022 at 17:52):

The code is included in the lsp server at https://github.com/m-fleury/isabelle-emacs/ (you can just ignore the entire emacs stuff)

view this post on Zulip Mathias Fleury (Dec 06 2022 at 17:53):

BTW if understands vscode enough to create a theory panel, that information is also very easy to get

view this post on Zulip Mathias Fleury (Dec 06 2022 at 17:53):

I was just never motivated enough to write a plugin in VSCode to print that information

view this post on Zulip Mathias Fleury (Dec 06 2022 at 17:53):

(or more precisely: it worked but was very very ugly)

view this post on Zulip Zixuan Fan (Dec 06 2022 at 18:02):

I guess I can try isabelle-emacs, then. I recently learned that proof general is good is some perspectives.

view this post on Zulip Mathias Fleury (Dec 06 2022 at 18:02):

Just clone the repo and run "path-to-repo/bin/isabelle vscode"

view this post on Zulip Mathias Fleury (Dec 06 2022 at 18:04):

you get the completely normal vscode from isabelle (I don't touch that) there is just 1 new features in the vscode communication…

view this post on Zulip Mathias Fleury (Dec 06 2022 at 18:05):

(you have to open the outline)

view this post on Zulip Mathias Fleury (Dec 06 2022 at 18:06):

image.png

view this post on Zulip Mathias Fleury (Dec 06 2022 at 18:08):

(no scary emacs involved, no change in your habits)

view this post on Zulip Christian Zimmerer (Dec 13 2022 at 23:45):

I would recommend to use Emacs over VScode for Isabelle so far though. The experience is way better for me. It's still a little tradeoff from the jedit interface, but you get to keep your keybindings and all convenience features from Emacs :)

view this post on Zulip Julian (Dec 14 2022 at 10:42):

Hope it's not off topic but this comes to mind: https://xkcd.com/378/

view this post on Zulip Manuel Eberl (Dec 14 2022 at 13:29):

In the good old days everyone wrote Isabelle in emacs! (ProofGeneral to be precise).
But back then there was official support for it. I cannot imagine how painful it must be these days…


Last updated: Mar 29 2024 at 08:18 UTC