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.
You have to start vscode with isabelle vscode
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?
yes
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?
Go into the directory and do Isabelle2023/bin/isabelle vscode
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.
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.
It is separate, but you can install extensions.
Last updated: Dec 21 2024 at 16:20 UTC