Moritz R (Oct 17 2024 at 16:45): Moritz R (Oct 17 2024 at 16:45):Hi,
i started Isabelle/vscode on windows by starting the cygwin terminal and typing
isabelle vscode -l HOL
However it seems it cant load correctly because of a path issue:
vscodium.png
i get
[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"
while the ISABELLE:OUTPUT stays empty.
Moritz R (Oct 28 2024 at 18:32):FIX:
Inside an Isabelle installation, you'll find a bin/isabelle binary. This binary can launch various Isabelle tools, including bin/isabelle vscode and bin/isabelle jedit. The former will install a separate custom patched VSCodium (separate from your normal VSCode install and unfortunately somewhat outdated). Beware that there used to be an Isabelle VSCode extension that I believe is still listed in the extension store. It is deprecated and will not work. If you plan to use Isabelle/VSCode, I'd recommend using it with Thomas Lindaes changes which aren't in a release yet. So to get his changes (and a needed fix for windows), you'll first need to grab the development version of Isabelle:
hg clone https://isabelle-dev.sketis.net/source/isabelle/There is also a GitHub mirror if you prefer to use git (although it might lag behind a little git clone https://github.com/isabelle-prover/mirror-isabelle.git).
Navigate into the cloned repo (i'll refer to the folder containing the src folder as the isabelle folder (if you used git, this folder will be called mirror-isabelle)): cd isabelle
from a normal install, copy the contrib folder and the Cygwin-Terminal.bat into the isabelle folder.
(Optional) Add a unique Isabelle identifier to keep it separate from other Isabelle instances on the system: echo "isabelle-language-server" >> ./etc/ISABELLE_IDENTIFIER
Windows error FIX: Edit the two following files. (Neccessary at this moment, else you will get this error:
[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"
)
I cannot guarantee that this works, but it seems to be doing fine. Im not sure why these checks are there.
We need to remove : and \\ from the illegal char sets in src/Pure/General/path.ML and src/Pure/General/path.scala.
The path.ML should be changed from
val illegal_char = ["/", "\\", "$", ":", "\"", "'", "<", ">", "|", "?", "*"];
to
val illegal_char = ["/", "$", "\"", "'", "<", ">", "|", "?", "*"];
and the path.scala from
private val illegal_char = "/\\$:\"'<>|?*"
to
private val illegal_char = "/$\"'<>|?*"
Start the Cygwin-Terminal.bat (and execute the following commands in this terminal).
Initialize Isabelle: ./Admin/init (requires internet access as it downloads external dependencies, like the aforementioned custom patched VSCodium)
It's probably also a good idea to run the following command. This will actually happen automatically if you open a theory file, but it takes a long time with no feedback: ./bin/isabelle build -b HOL
You'll also find similar instructions in the isabelle-lsp.nvim repo's README.
isabelle vscode -l HOL
if you want to change the print mode (e.g. to brackets)it needs to be passed in the command line (changing it in the vscode extension settings doesnt do anything at this moment) so start it with
isabelle vscode -l HOL -m brackets
Moritz R said:
I cannot guarantee that this works, but it seems to be doing fine. Im not sure why these checks are there.
Maybe @Fabian Huch knows why
Mathias Fleury (Oct 29 2024 at 07:57):The checks for illegal characters seem to be targeted at only allowing linux/cygwin paths (/home/user/ or /cygdrive/c/) and disallowing Microsoft paths
Mathias Fleury (Oct 29 2024 at 07:58):the real question is why is the path normalization not done before starting Isabelle
Mathias Fleury (Oct 29 2024 at 08:00):I know from porting the "theory panel" to VSCode that you really should not play with this part of the code or you might end-up with Isabelle believing that you have two theories open with the same name and a different path.
Fabian Huch (Oct 29 2024 at 08:58):Kevin Kappelmann said:
Moritz R said:
I cannot guarantee that this works, but it seems to be doing fine. Im not sure why these checks are there.
Maybe Fabian Huch knows why
The concept of an Isabelle Path abstracts away from file-system paths, which have different rules on different platforms. Your change is sure to break many things in unexpected ways.
As for the actual problem (with Isabelle2024), be sure to report it on the isabelle-users mailing list, which is the appropriate place for it.
Fabian Huch (Oct 29 2024 at 09:02):Mathias Fleury said:
The checks for illegal characters seem to be targeted at only allowing linux/cygwin paths (/home/user/ or /cygdrive/c/) and disallowing Microsoft paths
It has nothing to do with that: It is the representation of a logical path, not a file-system path (for those, we use java.io.File). For instance, Isabelle paths can have environment variables as path elements, which would start iwth a $.
Moritz R (Nov 03 2024 at 17:07):Well this is fun, now i get Java.lang.OutOfMemoryErrors even when using Jedit :octopus:
Moritz R (Nov 03 2024 at 22:16):But that isnt caused by my modifications. Just use sledgehammer for a while and it will do funny crashes
irvin (Nov 04 2024 at 00:30):Moritz R said:
But that isnt caused by my modifications. Just use sledgehammer for a while and it will do funny crashes
pretty sure that been an issue for some time. there is a similar zulip thread with the same problem
Last updated: Dec 21 2024 at 16:20 UTC