[isabelle] Isabelle2025-RC2 on windows: odd exceptions in... · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2025-RC2 on windows: odd exceptions in...

Email Gateway (Feb 16 2025 at 19:40):

From: Makarius <makarius@sketis.net>
On 16/02/2025 17:02, mo.roos@gmx.de wrote:

When one then looks under "Output" and selects "Isabelle" one sees
something like:
[Info - 21:41:22] Welcome to Isabelle/HOL (Isabelle2025-RC2)
*** Session consumer failure: "isabelle.vscode.Dynamic_Output"
*** Illegal character ":" in path element "C:
\Users\moroo\Desktop\rc1\Isabelle2025-RC2\src\HOL\Set.thy"

Trying to open state panel gives something like:
*** Session consumer failure: "isabelle.Query_Operation"
*** Illegal character ":" in path element "C:
\Users\moroo\Desktop\rc1\Isabelle2025-RC2\src\HOL\List.thy"
*** The error(s) above occurred in "C:\Users\moroo\Desktop\rc1\Isabelle2025-
RC2\src\HOL\List.thy"

I also had this issue back in october on the then most-recent isabelle-dev
running on a thinkpad E490 with windows 11.
I dont have it with me right now, so i can't check if it's working there.

Please let me know if there is any valuable info that i can add.

(I have changed the thread title to make clear what this is about.)

I still could not reproduce these exceptions. They somehow seem to be related
to lookup of formal entities from the context. Normally the file names
occurring there use Isabelle Posix notation, which you can check like this,
e.g. in Isabelle/jEdit in the context of Main:

theory Scratch
imports Main
begin

ML ‹
Name_Space.the_entry (Sign.type_space \<^theory>) \<^type_name>‹nat›
›

The result on my Linux box for Isabelle2025-RC2 is:

val it =
{concealed = false, group = 601716, pos =
{line=32, offset=621, end_offset=624, file=~~/src/HOL/Nat.thy, id=44},
serial = 601722,
suppress = [true, false], theory_long_name = "HOL.Nat"}:
{concealed: bool,
group: serial,
pos: Position.T, serial: serial, suppress: bool list, theory_long_name:
string}

On Windows it looks similar, escpecially the "file" property. If a Windows
path C:\ shows up there, then something is wrong.

Makarius

Email Gateway (Feb 16 2025 at 21:01):

From: "mo.roos" <cl-isabelle-users@lists.cam.ac.uk>
I do belive the path issues are related.
At least when i posted on this issue back in october, i was trying out simply
removing the checks, which allowed the state panel to work
(Btw, mouse hovering over the 1+1 still works even with the errors and shows
the result 2).

Since i was told that this will "very probably break things in unintended
ways" i didn't stay with that setup and instead installed some linux
distribution.
See #Beginner Questions > Colon illegal in Path on Windows with vscodium - Isabelle - Zulip
for these comments and what checks i removed back then.

The output of your code in Isabelle/jEdit is
val it =
{concealed = false, group = 601710, pos =
{line=32, offset=621, end_offset=624, file=~~/src/HOL/Nat.thy, id=44},
serial = 601716, suppress = [true, false], theory_long_name =
"HOL.Nat"}:
{concealed: bool,
group: serial,
pos: Position.T,
serial: serial, suppress: bool list, theory_long_name: string}

For Isabelle/vscode it is (yes, i get not errors from this code alone and get
an output).

val it =
{concealed = false, group = 601710, pos =
{line=32, offset=621, end_offset=624, file=~~/src/HOL/Nat.thy, id=44}, serial =
601716, suppress = [true, false], theory_long_name = "HOL.Nat"}:
{concealed: bool,
group: serial,
pos: Position.T, serial: serial, suppress: bool list, theory_long_name: string}

I can offer to ship/bring you my old (formatted ofc) windows laptop (if i can
still reproduce the issue on it in when im back in munich).
Even if it would break down while you have it, it wouldn't be a big loss to
me. What do you think?

Moritz

Gesendet: Sonntag, 16. Februar 2025 um 20:40

Von: Makarius <makarius@sketis.net>

An: mo.roos@gmx.de, cl-isabelle-users@lists.cam.ac.uk

Betreff: Re: [isabelle] Isabelle2025-RC2 on windows: odd exceptions in
Output

On 16/02/2025 17:02, mo.roos@gmx.de wrote:

When one then looks under "Output" and selects "Isabelle" one sees
something like:
[Info \- 21:41:22] Welcome to Isabelle/HOL (Isabelle2025-RC2)
*** Session consumer failure: "isabelle.vscode.Dynamic_Output"
*** Illegal character ":" in path element "C:
\Users\moroo\Desktop\rc1\Isabelle2025-RC2\src\HOL\Set.thy"

Trying to open state panel gives something like:
*** Session consumer failure: "isabelle.Query_Operation"
*** Illegal character ":" in path element "C:
\Users\moroo\Desktop\rc1\Isabelle2025-RC2\src\HOL\List.thy"
*** The error(s) above occurred in
"C:\Users\moroo\Desktop\rc1\Isabelle2025-
RC2\src\HOL\List.thy"