Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] isabelle vscode broken on windows - path issue


view this post on Zulip Email Gateway (Oct 29 2024 at 10:04):

From: Moritz Roos <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

see (70) #Beginner Questions > Colon illegal in Path on Windows with
vscodium - Isabelle - Zulip
<https://isabelle.zulipchat.com/#narrow/channel/238552-Beginner-Questions/topic/Colon.20illegal.20in.20Path.20on.20Windows.20with.20vscodium>
for a visually nicer Description of the issue. Also see the attached
image in this email.
When starting isabelle2024 vscode on windows through the cygwin shell
(and opening any .thy file) one gets the following error in the output
tab (set to "isabelle") of vscode:

[Info  - 18:33:01] Welcome to Isabelle/HOL (Isabelle2024)

*** Consumer failed: "isabelle.vscode.Dynamic_Output"

*** Illegal character ":" in path element
"C:\Isabelle2024\src\HOL\Nat.thy"

*** The error(s) above occurred in "C:\Isabelle2024\src\HOL\Nat.thy"

These errors render isabelle vscode not usable on windows.
The errors are raised in the illegal char lists in

src/Pure/General/path.ML

and in

src/Pure/General/path.scala

At this moment i have removed both the colon and the double backslash
from these lists but i was told this is sure to break other things in
unexpected ways.

This Issue affects both the Isabelle2024 release as well as the most
current dev version.

Moritz RoosThis is my first entry to this mailing list - i hope it was fine.

vscodium.png


Last updated: Jan 04 2025 at 20:18 UTC