Stream: Beginner Questions

Topic: Support of Isabelle VScode extension for latest vscode

nnarek (Mar 19 2025 at 13:00):

Hi there

I am using VS Code 1.97.2
and when I try to install vscode_extension-20241002/isabelle-2.0.0.vsix then I get following error

Error: Unable to install extension 'isabelle.isabelle' as it is not compatible with VS Code '1.97.2'.

Even when I edit engines.vscode field from 1.70.1 to 1.97.2 in $ISABELLE_HOME/src/Tools/VSCode/extension/package.json file and compile the plugin manually then it successfully gets installed but the plugin does not work(maybe because incompatible API interfaces between 1.97.2 and 1.70.1 versions of vscode)

vscode 1.70.1 is almost 3 year old

Mathias Fleury (Mar 19 2025 at 13:02):

You are supposed to use the version that is included in Isabelle (isabelle vscodium, not your version)

Poscat (Mar 24 2025 at 09:31):

I'm also interested in this. I made some modifications to make the extension work on latest vscode, would the upstream accept my patches?

Or shall I maintain it as a fork?

Kevin Kappelmann (Mar 24 2025 at 09:33):

oh, where is your fork? :eyes:

Fabian Huch (Mar 24 2025 at 09:40):

You mean modifications to Component_VSCodium? That would certainly be of interest.

Poscat (Mar 24 2025 at 09:50):

I've uploaded it here: https://github.com/poscat0x04/isabelle/tree/vscode-ext-update (IDK how to use hg)

It's a bit crude but it works.

Poscat (Mar 24 2025 at 09:52):

Also pardon the formatting changes cause I forgot to turn off the formatter

Fabian Huch (Mar 24 2025 at 10:05):

While I appreciate the effort, there are some misconceptions here:

• for Isabelle/VScode we use a patched vscodium (see the Component_VSCode module) to include the symbol encoding needed, which can't be done as an extension. Updating this is difficult due to build issues on Windows IIRC.
• The VSCode extension is built as a component to run on Isabelle/VSCode by the Component_VSCode_Extension module. What you see in src/Tools/VSCode/extension are sources for that module, not a standalone extension. This is why you will find things like "ISABELLE_OPTIONS": {}, that are replaced in the build process.

Fabian Huch (Mar 24 2025 at 10:10):

So patching an aextension like this and running it on a standard vscode(ium) has the following problems:

• Missing fonts, i.e. some symbols couldn't be rendered.
• Due to missing encoding, most symbols won't be rendered anyway and you'd be working with ASCII art.
• Hard-coded paths such as /opt/isabelle will lead to funny error messages (especially on different platforms).
• Isabelle options can't be controlled via the editor.

Fabian Huch (Mar 24 2025 at 10:13):

So, any work that wants to be included in upstream needs to update Component_VSCode such that it produces a good Isabelle/VSCode binary on all platforms.

Last updated: Apr 18 2025 at 20:21 UTC