Illegal character ":" in path element "C:\Isabelle\Isabelle2023\tmp\MLTEMPb14572"

Question

When I entered the isabelle build -bv CParserTest command in cygwin, the following error occurred

[isabelle] *** Illegal character ":" in path element "C:\Isabelle\Isabelle2023\tmp\MLTEMPb14572"`

How do I solve this stupid problem in Windows environment?

$ isabelle build -bv CParserTest

ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86_64_32-windows"
ML_HOME="/cygdrive/c/Isabelle/Isabelle2023/contrib/polyml-219e0a248f70/x86_64_32-windows"
ML_SYSTEM="polyml-5.9"
ML_OPTIONS="--minheap 500"

Session Pure/Pure
Session FOL/FOL\`
Session Misc/Tools
Session HOL/HOL (main)
Session HOL/HOL-Library (main timing)
Session HOL/HOL-Combinatorics (main timing)
Session HOL/HOL-Computational_Algebra (main timing)
Session HOL/HOL-Analysis (main timing)
Session HOL/HOL-Eisbach
Session HOL/HOL-Statespace
Session Lib/ML_Utils (lib)
Session Lib/Word_Lib (lib)
Session Lib/Basics (lib)
Session C-Parser/Simpl-VCG
Session C-Parser/CParser
Session C-Parser/CParserTest

Building CParserTest ...

CParserTest: theory CParserTest.analsignedoverflow

CParserTest FAILED (see also "isabelle build_log -H Error CParserTest")

*** Illegal character ":" in path element "C:\\Isabelle\\Isabelle2023\\tmp\\MLTEMPb14572"

*** The error(s) above occurred in "C:\\Isabelle\\Isabelle2023\\tmp\\MLTEMPb14572"

*** At command "install_C_file" (line 14 of "\~\~/src/c-parser/testfiles/analsignedoverflow.thy")

Unfinished session(s): CParserTest

Answer 1

Backslash is for escaping characters in cygwin (or similar shells). Just use C:/... in your path information (replace backslashes '\' with slashes '/').

Answer 2

No solution was found in the windows environment, but the linux environment can be used through WSL2 and the graphical interface can be used directly