Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: updates on Isabelle/VSCode

Email Gateway (Nov 17 2025 at 12:40):

From: Makarius <makarius@sketis.net>
* 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

Last updated: Dec 10 2025 at 12:50 UTC