vscode not working after 24.04 update (from 23.10 ubuntu) · General

Has anybody else similar issues, using the tar-ball installation of Isabelle 2023, using ubuntu? Invoking isabelle vscode in the terminal returns w/o any output, error messages, or similar. isabelle jedit works as expected. I have tried several codium installations.

Any ideas for how to troubleshoot this further? I am happy to build from source, but well, I wasn't able to find (clear) instructions for such matters. Thanks a lot in advance!

Tobias Heindel (Heliax GmbH) (Apr 30 2024 at 10:00):

The same behavior applies if I build the default version from the mercurial repository. After removing the .isabelle-directory, The follwing behavior is observed:

$ isabelle vscode
Installed Isabelle/VSCode extension "/home/tobias/Isabelle2023/contrib/vscode_extension-20230206/isabelle-2.0.0.vsix"
into directory: "/home/tobias/.isabelle/Isabelle2023/vscode/extensions/isabelle.isabelle-2.0.0"
(base) tobias@Tbook:~$ isabelle vscode
(base) tobias@Tbook:~$

Mathias Fleury (Apr 30 2024 at 11:40):

Mathias Fleury (Apr 30 2024 at 11:41):

Mathias Fleury (Apr 30 2024 at 11:42):

Tobias Heindel (Heliax GmbH) (Apr 30 2024 at 14:34):

ah, right, I forgot to mention: the vscode window is missing: vscode is not starting and I would want to understand why vscode is not popping up ?

Mathias Fleury (Apr 30 2024 at 19:34):

Mathias Fleury (Apr 30 2024 at 19:35):

Tobias Heindel (Heliax GmbH) (May 03 2024 at 08:12):

I have installed the debian package codium_1.88.1.24104_amd64.deb directly on ubuntu 24.04 and Isabelle via the tar-ball. By itself, codium is running normal. However, isabelle cannot launch it somehow, it seems ...

(base) tobias@Tbook:~/.isabelle$ codium
(base) tobias@Tbook:~/.isabelle$ ps -au tobias | grep -i cod
  21590 ?        00:00:00 codium
  21593 ?        00:00:00 codium
  21595 ?        00:00:00 codium
  21597 ?        00:00:00 codium
  21625 ?        00:00:00 codium
  21632 ?        00:00:00 codium
  21645 ?        00:00:01 codium
  21837 ?        00:00:00 codium
  21852 ?        00:00:00 codium
  21853 ?        00:00:00 codium
(base) tobias@Tbook:~/.isabelle$ ps -au tobias | grep -i cod
(base) tobias@Tbook:~/.isabelle$ isabelle vscode -C -L -v
(base) tobias@Tbook:~/.isabelle$ ls
Isabelle2023
(base) tobias@Tbook:~/.isabelle$ ls
Isabelle2023
(base) tobias@Tbook:~/.isabelle$ ls
Isabelle2023
(base) tobias@Tbook:~/.isabelle$ ls
Isabelle2023
(base) tobias@Tbook:~/.isabelle$ ls
Isabelle2023
(base) tobias@Tbook:~/.isabelle$ ls
Isabelle2023
(base) tobias@Tbook:~/.isabelle$ ls
Isabelle2023
(base) tobias@Tbook:~/.isabelle$ ls
Isabelle2023
(base) tobias@Tbook:~/.isabelle$ ls -l
total 4
drwxrwxr-x 6 tobias tobias 4096 Apr 30 18:53 Isabelle2023
(base) tobias@Tbook:~/.isabelle$ cd .
(base) tobias@Tbook:~/.isabelle$ cd ..
(base) tobias@Tbook:~$ ls -al |grep isabelle
drwxrwxr-x   3 tobias tobias      4096 Apr 30 14:11 .isabelle

Mathias Fleury (May 03 2024 at 08:13):

Tobias Heindel (Heliax GmbH) (May 03 2024 at 08:51):

(base) tobias@Tbook:~/.isabelle/Isabelle2023/vscode/user-data/logs/20240503T105017$ cat cli.log
[2024-05-03 10:50:17.779] [cli] [info] CLI main {"_":[],"diff":false,"merge":false,"add":false,"goto":false,"new-window":false,"reuse-window":false,"wait":false,"locale":"en-US","user-data-dir":"/home/tobias/.isabelle/Isabelle2023/vscode/user-data","help":false,"extensions-dir":"/home/tobias/.isabelle/Isabelle2023/vscode/extensions","list-extensions":false,"show-versions":false,"pre-release":false,"version":false,"verbose":false,"status":false,"prof-startup":false,"no-cached-data":false,"prof-v8-extensions":false,"disable-extensions":false,"disable-gpu":false,"ms-enable-electron-run-as-node":true,"telemetry":false,"locate-extension":["isabelle.isabelle"],"debugRenderer":false,"enable-smoke-test-driver":false,"logExtensionHostCommunication":false,"skip-release-notes":false,"skip-welcome":false,"disable-telemetry":false,"disable-updates":false,"disable-keytar":false,"disable-workspace-trust":false,"disable-crash-reporter":false,"skip-add-to-recently-opened":false,"unity-launch":false,"open-url":false,"file-write":false,"file-chmod":false,"force":false,"do-not-sync":false,"trace":false,"force-user-env":false,"force-disable-user-env":false,"open-devtools":false,"__enable-file-policy":false,"no-proxy-server":false,"no-sandbox":false,"nolazy":false,"force-renderer-accessibility":false,"ignore-certificate-errors":false,"allow-insecure-localhost":false,"disable-dev-shm-usage":false,"logsPath":"/home/tobias/.isabelle/Isabelle2023/vscode/user-data/logs/20240503T105017"}

Moritz R (Nov 04 2024 at 16:23):

Did you find a solution? I have just installed the vscode dev version from the mercurial repo and have exactly the same issue.
I just set up a completely fresh ubuntu 24.10, because vscode (and more importantly sledgehammer) dont work on windows

Moritz R (Nov 04 2024 at 16:25):

On the first time of executing isabelle vscodeit said something about installed the extension in ....

Moritz R (Feb 19 2025 at 16:28):

*** [7321:0219/162406.506082:FATAL:credentials.cc(128)] Check failed: . : Permission denied (13)
*** /tmp/isabelle-ubuntu/bash_script2749206926302655032: line 1: 7321 Trace/breakpoint trap   (core dumped) /home/ubuntu/Downloads/Isabelle2025-RC3_linux/Isabelle2025-RC3/contrib/vscodium-1.70.1/x86_64-linux/electron -v

It seems to be some issue with apparmor.
One possible fix is simply disabling this security feature as described here
via adding the line
kernel.apparmor_restrict_unprivileged_userns=0
to the file
/etc/sysctl.conf. Please don't ask me about any security implications this might have.

Stream: General

Topic: vscode not working after 24.04 update (from 23.10 ubuntu)

Tobias Heindel (Heliax GmbH) (Apr 30 2024 at 09:41):