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