在 Windows7 下无法从 Isabelle/HOL 生成 LaTeX答案

【问题标题】：Cannot generate LaTeX from Isabelle/HOL under Windows7在 Windows7 下无法从 Isabelle/HOL 生成 LaTeX
【发布时间】：2017-12-27 00:54:52
【问题描述】：

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

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

【问题讨论】：

标签： windows-7 installation latex isabelle

【解决方案1】：

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

在 Microsoft Explorer 中，我转到了包含 Isabelle 可执行文件的目录。此目录称为Isabelle2016-1。我通过在文件系统中搜索 Isabelle2016-1 找到了它。它位于C:\Users\sjo\AppData\Roaming\local\bin\Isabelle2016-1。我检查了它是否包含文件Cygwin-Terminal.bat。
我双击文件Cygwin-Terminal.bat。这将打开一个命令行解释器 (CLI)，它是 GNU Bash 解释器。
在此 CLI 中，我通过发出以下命令导航到包含我的 Isabelle 源代码 Increments.sty 的目录：
```
$ cd /cygdrive/d/git/Publications/2017AFPproofs
```
我使用命令ls -al 来验证这个目录是否包含我的Isabelle 源代码文件Increments.thy。
我通过调用 Isabelle 生成了一个 pdf 文件 D:\git\Publications\2017AFPproofs\output\document\root.pdf：
```
$ isabelle build -v -D .
```
我在 Microsoft Explorer 中检查了结果，并用我的 pdf-viewer 显示了它。

成功了。

【讨论】：

你是偶然使用 libisabelle 的吗？如果是这样，您究竟尝试过什么来构建您的文档？
我觉得您使用的是 libisabelle，因为您的安装位于 %APPDATA%。但转念一想，这也可能是您在因斯布鲁克的设置如何运作的人工制品。
不，我没有使用 libisabelle（据我所知）。我主要是遇到新手经常遇到的事情。一旦你启动并运行，这些问题往往会消失。与此同时，它把许多新手留在外面，因为缺乏合适的朋友，他们无法克服障碍。顺便说一句，我不是在因斯布鲁克工作，而是在荷兰工作。我刚得到他们的帮助，因为他们经常使用 Isabelle。
对于第 3 步和第 4 步，这是可行的，因为您拥有 ROOT 文件设置权限，这在isabelle.in.tum.de/doc/system.pdf 的第 2 章和第 3 章中有描述
@user1933930 好吧，但是如果不是来自 Cygwin，你究竟做了什么来运行 isabelle build 卡住了？这可能是 Isabelle 中的一个错误，但我不清楚问题可能是什么。任何其他信息都可能有助于确认问题。