--- a/Admin/components/components.sha1 Fri Sep 12 15:11:51 2025 +0200
+++ b/Admin/components/components.sha1 Fri Sep 12 22:42:03 2025 +0200
@@ -618,6 +618,8 @@
5293b9e77e5c887d449b671828b133fad4f18632 vscode_extension-20220829.tar.gz
0d9551ffeb968813b6017278fa7ab9bd6062883f vscode_extension-20230206.tar.gz
0630f00067dc973dab4c9274c56b79c973c5c494 vscode_extension-20241002.tar.gz
+51f6b3b9e36a8e3cd9c5b34de8bc5aca04892324 vscode_extension-20250912.tar.gz
+168c83143227972497e607bb8d95135059080140 vscodium-1.104.06131.tar.gz
67b271186631f84efd97246bf85f6d8cfaa5edfd vscodium-1.65.2.tar.gz
c439ab741e0cc49354cc03aa9af501202a5a38e3 vscodium-1.70.1.tar.gz
81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz
--- a/Admin/components/main Fri Sep 12 15:11:51 2025 +0200
+++ b/Admin/components/main Fri Sep 12 22:42:03 2025 +0200
@@ -40,8 +40,8 @@
stack-2.15.7
vampire-4.8
verit-2021.06.2-rmx-1
-vscode_extension-20241002
-vscodium-1.70.1
+vscode_extension-20250912
+vscodium-1.104.06131
xz-java-1.10
z3-4.4.0pre-4
zipperposition-2.1-1
--- a/NEWS Fri Sep 12 15:11:51 2025 +0200
+++ b/NEWS Fri Sep 12 22:42:03 2025 +0200
@@ -95,6 +95,18 @@
not available as SVG.
+*** Isabelle/VSCode Prover IDE ***
+
+* Update to recent VSCode 1.104 / VSCodium 1.104.06131, Electron 37.3.1,
+Chromium 138.0.7204.235, and Node.js 22.18.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.104.06131/x86_64-linux
+ sudo chown root:root chrome-sandbox
+ sudo chmod 4755 chrome-sandbox
+
+
*** Pure ***
* Command 'thy_deps' expects optional theory arguments as long theory
--- a/src/Pure/Admin/component_polyml.scala Fri Sep 12 15:11:51 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala Fri Sep 12 22:42:03 2025 +0200
@@ -70,15 +70,17 @@
val target_dir = root + Path.explode("target")
progress.echo("Building GMP library ...")
- platform_context.execute(root,
- "[ -f Makefile ] && make distclean",
- "./configure --disable-static --enable-shared --enable-cxx" +
- " --build=" + platform_arch + "-" + platform_os +
- """ --prefix="$PWD/target" """ + Bash.strings(options),
- "rm -rf target",
- "make",
- "make check",
- "make install")
+ platform_context.bash(
+ Library.make_lines(
+ "set -e",
+ "[ -f Makefile ] && make distclean",
+ "./configure --disable-static --enable-shared --enable-cxx" +
+ " --build=" + platform_arch + "-" + platform_os +
+ """ --prefix="$PWD/target" """ + Bash.strings(options),
+ "rm -rf target",
+ "make",
+ "make check",
+ "make install"), cwd = root).check
if (platform.is_windows) {
val bin_dir = target_dir + Path.explode("bin")
@@ -143,14 +145,16 @@
case None => ""
}
- platform_context.execute(root,
- platform_info.setup,
- gmp_setup,
- "[ -f Makefile ] && make distclean",
- """./configure --prefix="$PWD/target" """ + Bash.strings(configure_options),
- "rm -rf target",
- "make",
- "make install")
+ platform_context.bash(
+ Library.make_lines(
+ "set -e",
+ platform_info.setup,
+ gmp_setup,
+ "[ -f Makefile ] && make distclean",
+ """./configure --prefix="$PWD/target" """ + Bash.strings(configure_options),
+ "rm -rf target",
+ "make",
+ "make install"), cwd = root).check
/* sha1 library */
@@ -160,7 +164,7 @@
case Some(dir) =>
val platform_path = Path.explode(platform.ISABELLE_PLATFORM(windows = true, apple = true))
val platform_dir = dir + platform_path
- platform_context.execute(dir, "./build " + File.bash_path(platform_path))
+ platform_context.bash("./build " + File.bash_path(platform_path), cwd = dir).check
File.read_dir(platform_dir).map(entry => platform_dir + Path.basic(entry))
case None => Nil
}
--- a/src/Pure/System/isabelle_platform.scala Fri Sep 12 15:11:51 2025 +0200
+++ b/src/Pure/System/isabelle_platform.scala Fri Sep 12 22:42:03 2025 +0200
@@ -7,6 +7,9 @@
package isabelle
+import java.util.{Map => JMap}
+
+
object Isabelle_Platform {
val settings: List[String] =
List(
@@ -68,12 +71,14 @@
def standard_path(path: Path): String =
mingw.standard_path(File.platform_path(path))
- def execute(cwd: Path, script_lines: String*): Process_Result = {
- val script = cat_lines("set -e" :: script_lines.toList)
- val script1 =
+ def bash(script: String,
+ cwd: Path = Path.current,
+ env: JMap[String, String] = Isabelle_System.Settings.env(),
+ ): Process_Result = {
+ progress.bash(
if (is_macos_arm) "arch -arch arm64 bash -c " + Bash.string(script)
- else mingw.bash_script(script)
- progress.bash(script1, cwd = cwd, echo = progress.verbose).check
+ else mingw.bash_script(script),
+ cwd = cwd, env = env, echo = progress.verbose)
}
}
}
--- a/src/Pure/System/nodejs.scala Fri Sep 12 15:11:51 2025 +0200
+++ b/src/Pure/System/nodejs.scala Fri Sep 12 22:42:03 2025 +0200
@@ -12,7 +12,7 @@
object Nodejs {
/** independent installation **/
- val default_version = "22.17.0"
+ val default_version = "22.18.0"
def setup(
base_dir: Path,
@@ -68,11 +68,12 @@
def install(name: String, production: Boolean = false): Unit = {
progress.echo("Installing " + name + " ...")
- platform_context.execute(path,
+ platform_context.bash(
Library.make_lines(
+ "set -e",
path_setup,
"npm install --global " + if_proper(production, "--production ") + Bash.string(name)
- )).check
+ ), cwd = path).check
}
}
--- a/src/Tools/VSCode/extension/package.json Fri Sep 12 15:11:51 2025 +0200
+++ b/src/Tools/VSCode/extension/package.json Fri Sep 12 22:42:03 2025 +0200
@@ -17,7 +17,7 @@
"url": "https://isabelle-dev.sketis.net"
},
"engines": {
- "vscode": "^1.103.0"
+ "vscode": "^1.104.0"
},
"categories": [
"Programming Languages"
@@ -314,7 +314,7 @@
"devDependencies": {
"@types/mocha": "^9.1.0",
"@types/node": "^17.0.19",
- "@types/vscode": "^1.103.0",
+ "@types/vscode": "^1.104.0",
"mocha": "^9.2.1",
"typescript": "^4.5.5"
},
--- a/src/Tools/VSCode/src/component_vscodium.scala Fri Sep 12 15:11:51 2025 +0200
+++ b/src/Tools/VSCode/src/component_vscodium.scala Fri Sep 12 22:42:03 2025 +0200
@@ -13,7 +13,7 @@
import isabelle._
import java.security.MessageDigest
-import java.util.Base64
+import java.util.{Map => JMap, Base64}
object Component_VSCodium {
@@ -24,17 +24,15 @@
"jq", "git", "python3", "gcc", "g++", "make", "pkg-config", "fakeroot", "curl",
"libx11-dev", "libxkbfile-dev", "libsecret-1-dev", "libkrb5-dev", "libfontconfig1")
- val windows_packages_msys2: List[String] =
- List("p7zip", "git", "jq", "mingw-w64-ucrt-x86_64-rustup")
+ val windows_packages: List[String] = List("jq", "git", "p7zip", "mingw-w64-ucrt-x86_64-rustup")
- val macos_packages: List[String] =
- List("jq")
+ val macos_packages: List[String] = List("jq")
/* vscode parameters */
val default_node_version = Nodejs.default_version
- val default_vscodium_version = "1.103.25610"
+ val default_vscodium_version = "1.104.06131"
val vscodium_repository = "https://github.com/VSCodium/vscodium.git"
val vscodium_download = "https://github.com/VSCodium/vscodium/releases/download"
@@ -69,9 +67,7 @@
"VSCODE_LATEST=no",
"CI_BUILD=no",
"SKIP_ASSETS=yes",
- "SHOULD_BUILD=yes",
- "SHOULD_BUILD_REH=no",
- "SHOULD_BUILD_REH_WEB=no")
+ "SHOULD_BUILD=yes")
def build_upstream_env(dir: Path): List[String] = {
val str = File.read(dir + Path.explode("upstream/stable.json"))
@@ -123,7 +119,8 @@
platform_context: Isabelle_Platform.Context,
node_root: Option[Path] = None,
node_version: String = "",
- vscodium_version: String = default_vscodium_version
+ vscodium_version: String = default_vscodium_version,
+ python_exe: Option[Path] = None
): Build_Context = {
val platform = platform_context.isabelle_platform
val env1 =
@@ -150,7 +147,8 @@
else if (platform.is_linux) List("SKIP_LINUX_PACKAGES=True")
else Nil
val node_version1 = proper_string(node_version).getOrElse(default_node_version)
- new Build_Context(platform_context, node_root, node_version1, vscodium_version, env1 ::: env2)
+ new Build_Context(
+ platform_context, node_root, node_version1, vscodium_version, python_exe, env1 ::: env2)
}
}
@@ -159,6 +157,7 @@
node_root: Option[Path],
node_version: String,
vscodium_version: String,
+ python_exe: Option[Path],
env: List[String]
) {
override def toString: String = platform_name
@@ -195,7 +194,8 @@
Isabelle_System.git_clone(vscodium_repository, build_dir, checkout = vscodium_version)
progress.echo("Getting VSCode repository ...")
- platform_context.execute(build_dir, environment(build_dir) + "\n" + "./get_repo.sh").check
+ platform_context.bash(
+ environment(build_dir) + "\n" + "./get_repo.sh", cwd = build_dir).check
}
def platform_name: String = platform_context.ISABELLE_PLATFORM
@@ -206,6 +206,13 @@
def environment(dir: Path): String =
Bash.exports((build_env ::: build_upstream_env(dir) ::: env):_*)
+ def settings: JMap[String, String] =
+ python_exe match {
+ case None => Isabelle_System.Settings.env()
+ case Some(exe) =>
+ Isabelle_System.Settings.env(List("NODE_GYP_FORCE_PYTHON" -> File.platform_path(exe)))
+ }
+
def patch_sources(base_dir: Path): String = {
val dir = base_dir + Path.explode("vscode")
Isabelle_System.with_copy_dir(dir, dir.orig) {
@@ -316,13 +323,16 @@
progress.echo("Preparing VSCode ...")
Isabelle_System.with_copy_dir(vscode_dir, vscode_dir.orig) {
- platform_context.execute(build_dir,
- "set -e",
- build_context.environment(build_dir),
- node_dir.path_setup,
- "./prepare_vscode.sh",
- // enforce binary diff of code.xpm
- "cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm").check
+ platform_context.bash(
+ Library.make_lines(
+ "set -e",
+ build_context.environment(build_dir),
+ node_dir.path_setup,
+ "./prepare_vscode.sh",
+ // enforce binary diff of code.xpm
+ "cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm"),
+ cwd = build_dir,
+ env = build_context.settings).check
Isabelle_System.make_patch(build_dir, vscode_dir.orig.base, vscode_dir.base,
diff_options = "--exclude=.git --exclude=node_modules")
}
@@ -337,6 +347,7 @@
node_root: Option[Path] = None,
node_version: String = default_node_version,
vscodium_version: String = default_vscodium_version,
+ python_exe: Option[Path] = None,
platform_context: Isabelle_Platform.Context = Isabelle_Platform.Context(),
): Unit = {
val platform = platform_context.isabelle_platform
@@ -346,7 +357,8 @@
Build_Context.make(platform_context,
node_root = node_root,
node_version = node_version,
- vscodium_version = vscodium_version)
+ vscodium_version = vscodium_version,
+ python_exe = python_exe)
platform_context.mingw.check()
@@ -391,16 +403,18 @@
val node_dir = build_context.node_setup(build_dir)
progress.echo("Installing rust ...")
- platform_context.execute(build_dir, "rustup toolchain install stable").check
+ platform_context.bash("rustup toolchain install stable", cwd = build_dir).check
if (platform.is_macos && !platform_context.apple) {
- platform_context.execute(build_dir, "rustup target add x86_64-apple-darwin").check
+ platform_context.bash("rustup target add x86_64-apple-darwin", cwd = build_dir).check
}
progress.echo("Building VSCodium ...")
val environment = build_context.environment(build_dir)
progress.echo(environment, verbose = true)
- platform_context.execute(
- build_dir, node_dir.path_setup + "\n" + environment + "./build.sh").check
+ platform_context.bash(
+ node_dir.path_setup + "\n" + environment + "./build.sh",
+ cwd = build_dir,
+ env = build_context.settings).check
Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
@@ -462,8 +476,7 @@
* x86_64-windows with Cygwin-Terminal, using prerequisites in typical locations:
- export NODE_GYP_FORCE_PYTHON='C:\Python313\python.exe'
- isabelle component_vscodium -M "/cygdrive/c/msys64" -n "/cygdrive/c/Program Files/nodejs"
+ isabelle component_vscodium -M "/cygdrive/c/msys64" -P /cygdrive/c/Python313/python.exe
Makarius
@@ -483,6 +496,7 @@
var node_version = default_node_version
var vscodium_version = default_vscodium_version
var node_root: Option[Path] = None
+ var python_exe: Option[Path] = None
var verbose = false
val getopts = Getopts("""
@@ -494,6 +508,7 @@
-M DIR msys/mingw root specification for Windows
-N VERSION download Node.js version (overrides option -n)
(default: """" + default_node_version + """")
+ -P FILE Python executable (default: educated guess by node-gyp)
-V VERSION VSCodium version (default: """" + default_vscodium_version + """")
-n DIR use existing Node.js directory (overrides option -N)
-v verbose
@@ -507,19 +522,13 @@
sudo apt install -y """ + linux_packages.mkString(" ") + """
Windows prerequisites:
- - install Visual Studio 2022 with C++ development and C++ library with
- Spectre mitigation: see https://visualstudio.microsoft.com/downloads
- - install Nodejs """ + default_node_version + """ including Windows build tools:
- see https://nodejs.org/dist/v""" + default_node_version +
- "/node-v" + default_node_version + """-x64.msi
- - rebuild native node-pty, using "cmd" as Administrator:
- npm install --global node-gyp node-pty@1.1.0-beta33
- cd "C:\Program Files\nodejs\node_modules\node-pty"
- npx node-gyp rebuild node-pty
+ - install Visual Studio 2022: see https://visualstudio.microsoft.com/downloads
+ + Desktop development with C++
+ + x64/x86 C++ spectre mitigated libs
- MSYS2/UCRT64: see https://www.msys2.org
- MSYS2 packages:
pacman -Su
- pacman -S --needed --noconfirm """ + windows_packages_msys2.mkString(" ") + """
+ pacman -S --needed --noconfirm """ + windows_packages.mkString(" ") + """
macOS prerequisites:
- macOS 13 Ventura
@@ -532,6 +541,7 @@
"I" -> (arg => intel = true),
"M:" -> (arg => mingw = MinGW(Path.explode(arg))),
"N:" -> { arg => node_version = arg; node_root = None },
+ "P:" -> (arg => python_exe = Some(Path.explode(arg))),
"V:" -> (arg => vscodium_version = arg),
"n:" -> { arg => node_root = Some(Path.explode(arg)); node_version = "" },
"v" -> (_ => verbose = true))
@@ -543,7 +553,7 @@
val platform_context = Isabelle_Platform.Context(mingw = mingw, apple = !intel, progress = progress)
component_vscodium(target_dir = target_dir, node_root = node_root,
- node_version = node_version, vscodium_version = vscodium_version,
+ node_version = node_version, python_exe = python_exe, vscodium_version = vscodium_version,
platform_context = platform_context)
})
--- a/src/Tools/VSCode/src/vscode_main.scala Fri Sep 12 15:11:51 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_main.scala Fri Sep 12 22:42:03 2025 +0200
@@ -60,8 +60,7 @@
error("""Undefined $ISABELLE_VSCODIUM_ELECTRON: missing "vscodium" component""")
}
val args0 =
- List(platform_path("$ISABELLE_VSCODIUM_RESOURCES/vscodium/out/cli.js"),
- "--ms-enable-electron-run-as-node", "--locale", "en-US",
+ List(platform_path("$ISABELLE_VSCODIUM_RESOURCES/vscodium/out/cli.js"), "--locale", "en-US",
"--user-data-dir", platform_path("$ISABELLE_VSCODE_SETTINGS/user-data"),
"--extensions-dir", platform_path("$ISABELLE_VSCODE_SETTINGS/extensions"))
val script =