Windows环境下Isabelle构建报错：路径含非法字符':'的解决求助

在Windows系统的Cygwin环境中执行isabelle build -bv CParserTest时，出现路径包含非法字符:的错误：

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

完整构建日志如下：

$ 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

方法1：临时指定Cygwin风格的Isabelle临时目录 #

Isabelle默认使用Windows风格路径，Cygwin环境下部分组件无法识别。手动设置临时目录为Cygwin格式：

• 打开Cygwin终端，设置环境变量：

  export ISABELLE_TMP="/cygdrive/c/Isabelle/Isabelle2023/tmp_cygwin"
  

• 提前创建该目录：

  mkdir -p /cygdrive/c/Isabelle/Isabelle2023/tmp_cygwin
  

• 重新执行构建命令：

  isabelle build -bv CParserTest
  

方法2：永久修改Isabelle配置文件中的临时目录 #

• 找到或创建Isabelle配置文件~/.isabelle/Isabelle2023/etc/settings
• 添加以下内容：

  ISABELLE_TMP="/cygdrive/c/Isabelle/Isabelle2023/tmp_cygwin"
  

• 保存后重启Cygwin终端，再执行构建命令

方法3：修正install_C_file命令的路径格式 #

错误触发点在analsignedoverflow.thy的第14行install_C_file命令，需将其中的Windows路径转换为Cygwin格式：

• 打开\~\~/src/c-parser/testfiles/analsignedoverflow.thy文件
• 将命令中的C:\xxx格式路径替换为/cygdrive/c/xxx格式
• 保存文件后重新执行构建

方法4：验证Cygwin路径转换功能 #

• 执行以下命令检查cygpath工具的路径转换能力：

  cygpath -u "C:\Isabelle\Isabelle2023\tmp"
  

  正常应输出/cygdrive/c/Isabelle/Isabelle2023/tmp
• 若转换失败，重新安装Cygwin的cygutils包

内容的提问来源于stack exchange，提问作者leo