如何从 Windows 10 执行 Isabelle 2021 命令行命令？

Question

我已经安装了 Isabelle 2021 版本，现在我想按照 https://drops.dagstuhl.de/opus/volltexte/2020/13065/pdf/LIPIcs-TYPES-2019-1.pdf 第 12 页第 15.1 章第 2 节中的建议尝试命令“isabelle export”。

我可以看到两种可能性：

• 有主 Isabelle2021.exe，但它启动 jEdit 窗口，我仔细检查了打包的 jEdit 选项，我没有发现 jEdit 可能作为输入 isabelle 命令行命令的工具。

• bin 目录中有 3 个脚本 - isabelle、isabelle_java、isabelle_scala_script，我为每个脚本制作了 *.bat 文件的副本，我尝试从 Windows 命令行运行，但我得到了：

  C:\Homes\Isabelle2021\Isabelle2021\bin>isabelle_scala_script.bat 导出

  C:\Homes\Isabelle2021\Isabelle2021\bin>#!/usr/bin/env bash “#！”不被识别为内部或外部命令， 可运行的程序或批处理文件。

  C:\Homes\Isabelle2021\Isabelle2021\bin># '#' 未被识别为内部或外部命令， 可运行的程序或批处理文件。

所以，这些命令可能与 *nix 相关，可能需要从 cygwin 运行，不是吗？

好的，现在我正在消化这 3 个文件的内容，也许我可以针对 Windows 调整它们。但是很高兴听到从 Windows shell 运行 Isabelle 命令的传统预期方式是什么？

Answer 1

答案很简单——除了 isabelle2021.exe 之外还有 Cygwin-Terminal.bat，这个 *.bat 会打开 cygwin shell，其中 isabelle 命令可用，包括 isabelle export 及其选项。