Stream: Beginner Questions

Topic: Vscode


view this post on Zulip Alexander Kurz (Oct 01 2023 at 05:08):

I have been away from Isabelle for too many years. One thing that changed is that I use now vscode for most of my programming. Is there a good way to do isabelle from vscode? The extension I found says it is obsolete.

view this post on Zulip Jan van Brügge (Oct 01 2023 at 18:55):

You have to start vscode with isabelle vscode

view this post on Zulip Alexander Kurz (Oct 01 2023 at 21:32):

Jan van Brügge said:

You have to start vscode with isabelle vscode

Thanks ... can you give me more details? I installed the latest version of Isabelle. I can start the Isabelle IDE. isabelle vscode, is that a command I should be able to run from the command line?

view this post on Zulip Jan van Brügge (Oct 01 2023 at 22:02):

yes

view this post on Zulip Alexander Kurz (Oct 01 2023 at 23:57):

cool ... after downloading Isabelle from https://isabelle.in.tum.de/installation.html what steps do I have to take to be able to run isabelle vscode from the command line?

view this post on Zulip Jan van Brügge (Oct 02 2023 at 08:43):

Go into the directory and do Isabelle2023/bin/isabelle vscode

view this post on Zulip Wolfgang Jeltsch (Oct 02 2023 at 14:02):

And beware that Isabelle/VSCode is pretty much in alpha state, meaning not everything works properly. That said, I nevertheless prefer it over Isabelle/jEdit.

view this post on Zulip Alexander Kurz (Oct 09 2023 at 04:04):

Thanks for your help. It took me some while to reply. (Too many projects.) I am interested in experimenting how Isabelle integrates with Large Language Models (LLMs). On the one hand, I used Isabelle with jedit and fed .thy files into Aider https://aider.chat/docs/install.html ... having forgotten all of Isabelle syntax this worked better than not having an AI. But it is certainly not (yet?) as groundbreaking as using Aider for ordinary programming languages. Summary: mildly positive effect of AI, helpful for beginners, useless for experts. I wanted to compare this with using Github Copilot which integrates well with vscode. But now it seems that I cannot use the Github Copilot extension at the same time as the Isabelle Vscode extension. Tell me if I am wrong, but afaics, the isabelle vscode is completely separated from 'ordinary' vscode.

view this post on Zulip Fabian Huch (Oct 09 2023 at 07:05):

It is separate, but you can install extensions.


Last updated: Apr 27 2024 at 20:14 UTC