Ant S. (Feb 12 2026 at 20:32): Ant S. (Feb 12 2026 at 20:32):Hi,
I'm trying to get the extension for isabelle/vscode running. I looked at the source repo and I couldn't find much in the README. When I installed it on windows, it came with a VSIX file, although the same does not hold true for Linux. I went into src/tools/VSCode/extension and ran sudo vsce package to no avail, as I got the following runtime error in Node:
/usr/local/lib/node_modules/@vscode/vsce/node_modules/undici/lib/web/webidl/index.js:534
webidl.is.File = webidl.util.MakeTypeAssertion(File)
^
ReferenceError: File is not defined
at Object.<anonymous> (/usr/local/lib/node_modules/@vscode/vsce/node_modules/undici/lib/web/webidl/index.js:534:48)
at Module._compile (node:internal/modules/cjs/loader:1356:14)
at Module._extensions..js (node:internal/modules/cjs/loader:1414:10)
at Module.load (node:internal/modules/cjs/loader:1197:32)
at Module._load (node:internal/modules/cjs/loader:1013:12)
at Module.require (node:internal/modules/cjs/loader:1225:19)
at require (node:internal/modules/helpers:177:18)
at Object.<anonymous> (/usr/local/lib/node_modules/@vscode/vsce/node_modules/undici/lib/web/fetch/util.js:12:20)
at Module._compile (node:internal/modules/cjs/loader:1356:14)
at Module._extensions..js (node:internal/modules/cjs/loader:1414:10)
Node.js v18.19.1
What exactly am I doing wrong? If there is documentation on installing the extension, where can I find it?
Kevin Kappelmann (Feb 12 2026 at 20:45):You can run isabelle vscode (instead of isabelle jedit) from your terminal.
Ant S. (Feb 12 2026 at 20:46):but does that install the extension?
Ant S. (Feb 12 2026 at 20:46):or are you implying that I don't need to bother with installation?
Kevin Kappelmann (Feb 12 2026 at 20:47):You don't need to bother. It automatically opens a patched VSCodium. Note that this is separate from your own VSCode installation in case you have one.
Ant S. (Feb 12 2026 at 20:48):Thanks, I got it working! :)
If I may ask, do you know why it's done like this? Why not just allow people to interface with their pre-existing vsc installation?
Lukas Stevens (Feb 13 2026 at 09:58):Ant S. said:
Thanks, I got it working! :)
If I may ask, do you know why it's done like this? Why not just allow people to interface with their pre-existing vsc installation?
First of all, VSCode needs to be patched to work with Isabelle. Therefore, an existing installation would not work. Furthermore, VSCode is a moving target paying no regards to backwards compatability. Since Isabelle is a software distribution, it must fix the version of VSCode for each release to ensure that every component of the distribution (including VSCode) works together.
Lawrence Paulson (Feb 13 2026 at 12:01):Does anybody know why VSCode needs to be patched to work with Isabelle? With the help of extensions, it supports hundreds of programming languages, including the Lean proof assistant.
Lukas Stevens (Feb 13 2026 at 12:03):I think the primary reason is that it needs to keep track of two buffers: one with Isabelle-UTF8 and its symbols and the more low-level one that translates it to ASCII.
Lukas Stevens (Feb 13 2026 at 12:05):As far as I know, Lean uses UTF-8 directly. But this comes with restrictions because there are things in Isabelle notation that UTF-8 does not support.
irvin (Feb 13 2026 at 12:07):I've heard from other people that apparently vs code supports having a view over a text file but have not managed to find what feature they are talking about
Lukas Stevens (Feb 13 2026 at 12:08):Yeah, but this does not really solve the issue. You really want the symbols in your buffer to be one symbol not a lengthy ASCII string since that makes editing it a pain.
Lukas Stevens (Feb 13 2026 at 12:09):If you iterate on the view thing long enough, you will probably end up with the current solution :wink:
Ant S. (Feb 13 2026 at 14:32):Another question when using Isabelle/VSCode. My X-Y problem is that I want to understand how Isabelle made the proof (even though that's not relevant), but I don't know Isar yet.
Suppose I have a lemma simp1, and I have this line in my proof script:
prf simp1.
how do I display this? Do I need to use Isabelle/jEdit?
Ant S. (Feb 13 2026 at 14:32):While I know this is usually not the point, I would like to take a "peek under the hood"
Ant S. (Feb 13 2026 at 14:36):Well, I "ran" prf simp1 and got this:
❙? ∙ (Pure.PClass type_class ⋅ TYPE(?'a))
Ant S. (Feb 13 2026 at 14:37):in the Isabelle Output window
Fabian Huch (Feb 16 2026 at 12:25):Lukas Stevens said:
I think the primary reason is that it needs to keep track of two buffers: one with Isabelle-UTF8 and its symbols and the more low-level one that translates it to ASCII.
Also, it needs the proper font in all places, which VSCode extensions can't regularly do (Lean simply uses a standard monospace font).
Max Lang (Feb 16 2026 at 14:24):Out of curiosity, what's the problem with a standard monospace font? I've been using something different than the default (in Isabelle/jEdit), and quite prefer the uniform character width (although exponent notation still messes with that). The obvious downside is that the long arrows are relatively short, but this is an acceptable trade-off for me.
Fabian Huch (Feb 16 2026 at 14:39): Fabian Huch (Feb 16 2026 at 14:39):So it is a tradeoff: Simplicity vs quality.
Last updated: Mar 04 2026 at 20:34 UTC