windows-7 - 无法在 Windows7 下从 Isabelle/HOL 生成 LaTeX

Question

我花了太多时间试图根据我的 Isabelle 理论 Increments.thy 生成 .pdf 文档。 Isabelle 构建命令卡住了，显然这是 Windows 上的安装问题。令人沮丧的是， friend 们已经在他们的 linux 机器上完成了这个并且他们根本没有遇到任何问题。但是我找不到合适的文档来让它在我的 Windows 7 笔记本电脑上运行。有人有食谱吗？

我在笔记本电脑上安装了完整的 LaTeX，工作起来轻而易举。我已经安装了 CYGWIN，但它给文件访问权限带来了问题，我无法解决(无论是从 Windows 端，还是从 cygwin 端)。我尝试了各种手册，但运气不佳。

Answer 1

在因斯布鲁克大学的实际帮助下，我终于可以在我的 Windows-7 笔记本电脑上根据伊莎贝尔理论生成 pdf 文件。我想为整个社区分享结果。这是我为使其工作所做的工作:

1. 在 Microsoft Explorer 中，我转到了包含 Isabelle 可执行文件的目录。此目录名为 Isabelle2016-1。我是通过在文件系统中搜索Isabelle2016-1找到的。它位于 C:\Users\sjo\AppData\Roaming\local\bin\Isabelle2016-1 上。我检查它是否包含文件 Cygwin-Terminal.bat。

2. 我通过双击调用文件 Cygwin-Terminal.bat。这将打开一个命令行解释器 (CLI)，它是 GNU Bash 解释器。

3. 在此 CLI 中，我导航到包含我的 Isabelle 源代码 Increments.sty 的目录，方法是发出以下命令:

   $ cd /cygdrive/d/git/Publications/2017AFPproofs
   

   我使用命令 ls -al 验证此目录包含我的 Isabelle 源代码文件 Increments.thy。

4. 我通过调用 Isabelle 生成了一个 pdf 文件 D:\git\Publications\2017AFPproofs\output\document\root.pdf:

   $ isabelle build -v -D .
   

   我在 Microsoft Explorer 中检查了结果，并用我的 pdf 查看器显示了它。

成功了。