Email Gateway (Feb 12 2025 at 21:28): Email Gateway (Feb 12 2025 at 21:28):From: Moritz Roos <cl-isabelle-users@lists.cam.ac.uk>
Dear Makarius,
i have tested a bit and found a few strange things.
1. on Windows, if one Downloads the Isabelle2025-RC2.exe and opens it,
one gets to the "Unpack Isabelle2025-RC2?" menu. If one clicks the
folder icon to select an unpack-path, the program simply closes itself,
instead of giving the expected explorer selector.
2. Is there any plans on making Isabelle/vscode work on windows again?
If one opens it, one doesn't get any isabelle output under "ISABELLE"
(having set editor_output_state to true) and the state panel doesn't open.
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"
3. (Tested on Mac:) Shouldn't autocomplete prioritize a basically
perfect match?
If writing "\or" one gets the following suggestions
\<^oracle_name>
\<^oracle_name><>
a_
o_
\or
This is the same both in Jedit and in Vscode.
In Jedit this isn't that big of a deal, because it will remember that
one used \or last time.
It is only annoying in Vscode because of:
4. (Tested on Mac:) Isabelle/vscode doesn't seem to remember the last
autocompletes. It always gives the same output, ranking the perfect
match \or last.
5. (More of a feature wish):
When sledgehammering one often gets a found proof every few seconds.
Since in vscode the "try this: ..." aren't clickable one needs to select
the text manually.
But every 2 seconds (whenever sledgehammer finds another proof, or a
duplicate proof) the terminal resets its text which also resets the
mouse selection.
The result of this is, that one needs to wait for sledgehammer to be
done, before one can finally do the selection.
I guess that resetting the selection is inherent part of updating the
output.
I would be interested in giving developing "making stuff auto-insert" a
try, but i need an outline for what to do in which files. I tried
looking at the sources, but didn't find the relevant parts (i also have
few experience with the languages used in isabelle so thats that).
-Moritz
Email Gateway (Feb 15 2025 at 20:40):From: Makarius <makarius@sketis.net>
On 12/02/2025 22:23, Moritz Roos (via cl-isabelle-users Mailing List) wrote:
1. on Windows, if one Downloads the Isabelle2025-RC2.exe and opens it, one
gets to the "Unpack Isabelle2025-RC2?" menu. If one clicks the folder icon to
select an unpack-path, the program simply closes itself, instead of giving the
expected explorer selector.
It did work for me on my approx. 3 Windows test machines, and a few other
Windows users. Odd problems could still be there, but we need more context:
Version of Windows etc.
Or it could be an incomplete download.
Makarius
Email Gateway (Feb 16 2025 at 14:54):From: Makarius <makarius@sketis.net>
On 12/02/2025 22:23, Moritz Roos (via cl-isabelle-users Mailing List) wrote:
2. Is there any plans on making Isabelle/vscode work on windows again?
If one opens it, one doesn't get any isabelle output under "ISABELLE" (having
set editor_output_state to true) and the state panel doesn't open.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 have spent many hours trying many versions of Isabelle/VScode, and could not
quite reproduce this situation. How did you get these exceptions? Where are
they printed?
Starting with Isabelle2022 there have been significant changes in
Isabelle/VSCode startup: It now works via Isabelle/Scala, as almost everything
in Isabelle.
There can be situations, where the State output does not show up on Windows,
but I cannot pin this down excactly. It might be related with the "Trust
manager" of VSCode: When I "Trust" my file/directory and wait patiently until
the Isabelle language server is running, and then switch to a .thy file, there
is usually no problem with State output. Being less patient on startup usually
means that State output does not work.
Without understanding the reasons for that, it is not possible to improve the
situation --- which appears to be mostly the same since Isabelle2022.
Makarius
Email Gateway (Feb 16 2025 at 15:53):From: "mo.roos" <cl-isabelle-users@lists.cam.ac.uk>
To 1 :
Under the following link you can see a video of me reproducing the problem.
<https://we.tl/t-TD2ilBBEOR>
The link will only work for a week from now.
Let me know if i should share it some other way, i didn't want to litter
potenitally limited inboxes with videos.
The computer shown runs
Windows 10 Pro
Version 22H2
System build 10.0.19045 Build 19045 (number found on the "Systeminformationen"
(System info) page in windows.
Intel i5 7600k
16 GB RAM
64 bit Windows and processor
I can also reproduce on my normally used pc which runs
Windows 11 Home
Version 24H2
10.0.26100 Build 26100
intel i7 8700k
64 GB RAM
64 bit Windows and processor
Please let me know if there is any valuable info that i can add.
-Moritz
Gesendet: Samstag, 15. Februar 2025 um 21:39
Von: Makarius <makarius@sketis.net>
An: mo.roos@gmx.de, cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Betreff: Re: [isabelle] Isabelle2025-RC2 on windows
On 12/02/2025 22:23, Moritz Roos (via cl-isabelle-users Mailing List) wrote:
1. on Windows, if one Downloads the Isabelle2025-RC2.exe and opens it, one
gets to the "Unpack Isabelle2025-RC2?" menu. If one clicks the folder icon
to
select an unpack-path, the program simply closes itself, instead of giving
the
expected explorer selector.
It did work for me on my approx. 3 Windows test machines, and a few other
Windows users. Odd problems could still be there, but we need more context:
Version of Windows etc.
Or it could be an incomplete download.
Makarius
Email Gateway (Feb 16 2025 at 16:02):From: "mo.roos" <cl-isabelle-users@lists.cam.ac.uk>
To 2 :
Under the following link you can see a video of me reproducing the problem.
<https://we.tl/t-j78So2QInK>
The computer shown runs
Windows 10 Pro
Version 22H2
System build 10.0.19045 Build 19045 (number found on the "Systeminformationen"
(System info) page in windows.
Intel i5 7600k
16 GB RAM
64 bit Windows and processor
I can also reproduce on my normally used pc which runs
Windows 11 Home
Version 24H2
10.0.26100 Build 26100
intel i7 8700k
64 GB RAM
64 bit Windows and processor
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.
-Moritz
Gesendet: Sonntag, 16. Februar 2025 um 15:54
Von: Makarius <makarius@sketis.net>
An: mo.roos@gmx.de, cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Betreff: Re: [isabelle] Isabelle2025-RC2 on windows
On 12/02/2025 22:23, Moritz Roos (via cl-isabelle-users Mailing List) wrote:
2. Is there any plans on making Isabelle/vscode work on windows again?
If one opens it, one doesn't get any isabelle output under "ISABELLE"
(having
set editor_output_state to true) and the state panel doesn't open.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 have spent many hours trying many versions of Isabelle/VScode, and could not
quite reproduce this situation. How did you get these exceptions? Where are
they printed?
Starting with Isabelle2022 there have been significant changes in
Isabelle/VSCode startup: It now works via Isabelle/Scala, as almost everything
in Isabelle.
There can be situations, where the State output does not show up on Windows,
but I cannot pin this down excactly. It might be related with the "Trust
manager" of VSCode: When I "Trust" my file/directory and wait patiently until
the Isabelle language server is running, and then switch to a .thy file, there
is usually no problem with State output. Being less patient on startup usually
means that State output does not work.
Without understanding the reasons for that, it is not possible to improve the
situation --- which appears to be mostly the same since Isabelle2022.
Makarius
Email Gateway (Feb 16 2025 at 18:02):From: Makarius <makarius@sketis.net>
On 16/02/2025 16:52, mo.roos (via cl-isabelle-users Mailing List) wrote:
To 1:
Under the following link you can see a video of me reproducing the problem.
https://we.tl/t-TD2ilBBEOR <https://we.tl/t-TD2ilBBEOR>
The link will only work for a week from now.
Let me know if i should share it some other way, i didn't want to litter
potenitally limited inboxes with videos.The computer shown runs
Windows 10 Pro
Windows 11 Home
I have both Windows 10 and 11 as test machines. The download and click
sequence to convince Windows to execute the self-extracting 7z archive are
exactly the same for me. Only in the very end I usually say "Yes" instead of
clicking on the Folder Icon, where your dialog vanishes. Doing that on my
side, I get another dialog to select a Folder.
What happens when you select "Yes"?
Makarius
Email Gateway (Feb 16 2025 at 18:44):From: "mo.roos" <cl-isabelle-users@lists.cam.ac.uk>
It just starts extracting at the path written in the textbox - in the past (i
think i already had this problem for Isabelle 2024) i have simply typed the
path in manually.
I recorded a small video showing the extracting beginning. After the
extraction finished, Isabelle/jEdit starts itself automatically.
-Moritz
Gesendet: Sonntag, 16. Februar 2025 um 19:02
Von: Makarius <makarius@sketis.net>
An: mo.roos@gmx.de, cl-isabelle-users@lists.cam.ac.uk
Betreff: Re: [isabelle] Isabelle2025-RC2 on windows
On 16/02/2025 16:52, mo.roos (via cl-isabelle-users Mailing List) wrote:
To 1:
Under the following link you can see a video of me reproducing the problem.
<https://we.tl/t-TD2ilBBEOR> <<https://we.tl/t-TD2ilBBEOR>>
The link will only work for a week from now.
Let me know if i should share it some other way, i didn't want to litter
potenitally limited inboxes with videos.The computer shown runs
Windows 10 Pro
Windows 11 Home
I have both Windows 10 and 11 as test machines. The download and click
sequence to convince Windows to execute the self-extracting 7z archive are
exactly the same for me. Only in the very end I usually say "Yes" instead of
clicking on the Folder Icon, where your dialog vanishes. Doing that on my
side, I get another dialog to select a Folder.
What happens when you select "Yes"?
Makarius
Email Gateway (Feb 16 2025 at 18:59):From: Makarius <makarius@sketis.net>
On 16/02/2025 17:02, mo.roos (via cl-isabelle-users Mailing List) 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 have spent many hours trying many versions of Isabelle/VScode, and could not
quite reproduce this situation. How did you get these exceptions? Where are
they printed?To 2:
Under the following link you can see a video of me reproducing the problem.
https://we.tl/t-j78So2QInK <https://we.tl/t-j78So2QInK>
OK, you may remove all 3 videos now.
I think I understand the exceptions above, but they are probably unrelated to
the problem of not showing the State panel under certain circumstances.
Makarius
Last updated: Mar 09 2025 at 12:28 UTC