Tobias Heindel (Heliax GmbH) (Apr 30 2024 at 09:41): Tobias Heindel (Heliax GmbH) (Apr 30 2024 at 09:41):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):Tobias Heindel (Heliax GmbH) said:
Has anybody else similar issues, using the tar-ball installation of Isabelle 2023, using ubuntu? Invoking
isabelle vscodein the terminal returns w/o any output, error messages, or similar.isabelle jeditworks 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!
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:~$
For vscode this is normal
Mathias Fleury (Apr 30 2024 at 11:41):it just open a vscodium window and returni
Mathias Fleury (Apr 30 2024 at 11:42):isabelle jedit runs until you close jedit
Tobias Heindel (Heliax GmbH) (Apr 30 2024 at 14:34):Mathias Fleury said:
For vscode this is normal
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):Odd
Mathias Fleury (Apr 30 2024 at 19:35):htop that there is really no vscodium running?isabelle vscode -C -L -v produce output to the file ~/.isabelle/vscode/server.log? 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
isabelle is running its own codium, not the one from the distribution
Tobias Heindel (Heliax GmbH) (May 03 2024 at 08:51):Mathias Fleury said:
isabelle is running its own codium, not the one from the distribution
after uninstalling, the same behavior; meanwhile I've found the logs:
(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"}
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 ....
Last updated: Dec 21 2024 at 12:33 UTC