如何生成伊莎贝尔理论的 html 版本

Question

我有一个伊莎贝尔理论文件，名为John.thy. 我想把它展示给我的朋友，但我的朋友没有 Isabelle，而且原始.thy文件不太容易阅读。我在 Isabelle 库中看到了一些网页（例如： http: //isabelle.in.tum.de/library/HOL/Finite_Set.html），它们具有漂亮的语法突出显示，我希望我的理论看起来像像那样。

那么我该如何制作呢John.html？我查看了文档，所有的构建文件和 make 文件等看起来都相当可怕和困难。有好心人可以解释一下最简单的方法吗？

Answer 1

首先回答您的问题（另请参阅Isabelle 系统手册，第 3.2 节 -系统构建选项）：

要为您的 生成 HTML ，请在与 相同的目录中John.thy创建一个名为 的文件，其中包含以下内容ROOTJohn.thy

session John = "HOL" +
  theories
    John

然后，留在同一目录中，调用

isabelle build -d . -o browser_info -v John

在哪里

• -d .指定应在当前目录中搜索会话（在ROOT文件中指定）
• -o browser_info是生成 HTML（又名浏览器信息）的基本标志，并且
• -v（详细标志）对于查看结果放在哪个目录中很有用

上面的调用将输出类似的内容

Started at Thu Jul 25 09:38:20 JST 2013 [...]
[...]
Session Pure
Session HOL (main)
Session John
Running John ...
John: theory John
[...]
Browser info at /home/username/.isabelle/Isabelle2013/browser_info/HOL/John
[...]

（其中[...]表示省略的输出）。因此，您可以在此处看到必须查阅哪个目录才能获取 HTML 文件。

话虽如此，至少出于以下原因，我个人更喜欢 PDF 而不是 HTML：

• 你会-o browser_info在一个目录中得到一堆文件（而不是使用时只有一个独立的文件-o document=pdf）
• 并非所有 Isabelle 符号都能在 HTML 中很好地呈现（而您在生成 PDF 时可以完全控制符号）

注意：如果您使用的是 Mac OS 的Isabelle应用程序，您可能需要将isabelle上面的内容替换为/Applications/Isabelle2013.app/Isabelle/bin/isabelle或添加/Applications/Isabelle2013.app/Isabelle/bin/到您的PATH.