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

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

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

最佳答案

在因斯布鲁克大学的一些动手帮助下，我终于可以在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查看器显示了结果。

那行得通。

关于windows-7 - 在Windows7下无法从Isabelle/HOL生成LaTeX，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/45229742/