NEWS: updates on Isabelle/VSCode
Makarius
makarius at sketis.net
Mon Nov 17 13:39:10 CET 2025
*** General ***
* A Prover IDE session, e.g. in Isabelle/jEdit or Isabelle/VSCode, is
now able to load markup and messages from the underlying session
database. Example: "isabelle jedit -l HOL src/HOL/Nat.thy" for theory
"HOL.Nat" in session "HOL". This information is read-only: editing
theory sources in the editor will invalidate formal markup, and replace
it by an error message. Output messages depend on system options
"show_results" (default true) and "show_states" (default false),
provided at build-time for the underlying session database.
*** Isabelle/VSCode Prover IDE ***
* The command-line tool "isabelle vscode" builds its underlying logic
session before starting the VSCodium editor and its Isabelle language
server. Thus build progress, errors, and interrupts work more robustly
via the regular console.
* The command-line tool "isabelle vscode" supports new options -D and -J
to configure the underlying Java process of "isabelle vscode_server",
using the settings variable "VSCODE_JAVA_OPTIONS" as initial value to be
augmented. This is analogous to "JEDIT_JAVA_OPTIONS", but without
"JEDIT_JAVA_SYSTEM_OPTIONS"; regular "ISABELLE_JAVA_SYSTEM_OPTIONS" will
be used instead of "VSCODE_JAVA_SYSTEM_OPTIONS".
* Update to recent VSCode 1.105 / VSCodium 1.105.17075 (September 2025),
Electron 37.6.0, Chromium 138.0.7204.251, and Node.js 22.19.0. Note that
some Linux systems (e.g. Ubuntu 24.04) require special file permissions
to run "isabelle vscode" or "isabelle electron" like this:
cd .../vscodium-1.105.17075/x86_64-linux
sudo chown root:root chrome-sandbox
sudo chmod 4755 chrome-sandbox
This refers to Isabelle/1bbd2dc9b80e.
It is mostly the end of the many Isabelle/VSCode changes for this release ---
we could have spent our time in better ways, but I had promised a few people
to integrate things better and make a few improvements.
Further remarks:
* Loading theory "HOL.List" from the session image into the editor model
now works. There was a Java stack overflow that was hard to spot in VSCode
Output panel. I've addressed it in Isabelle/3673f8ce8f54.
* vscodium-1.105.17075 is the "latest" version from that derivative project
of the official MicroSoft code base. Unless there are genuine problems with it
there will be no further update for this Isabelle release: with so many
releases of VSCode per year, every one will be outdated quickly, and the value
of new "latest" versions is somewhat diminished. (Building it on all platforms
takes hours.)
* The odd problem with file permissions on Ubuntu 24.04 has disappeared
later on, e.g. in Ubuntu 25.10.
Makarius
More information about the isabelle-dev
mailing list