0

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

我可以看到两种可能性：

  • 有主要的 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 命令的常规、预期方式是什么？

4

1 回答 1

0

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

于 2021-03-21T01:33:09.650 回答