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

Question

我有一个 Isabelle 理论文件，名为 John.thy。我想向我的 friend 展示它，但我的 friend 没有 Isabelle，而且原始的 .thy 文件不是很容易阅读。我在 Isabelle 库中看到一些网页(比如这个:http://isabelle.in.tum.de/library/HOL/Finite_Set.html)有漂亮的语法突出显示，我希望我的理论看起来像那样。

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

Answer 1

首先回答您的问题(另见 Isabelle System Manual，第 3.2 节 - 系统构建选项):

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

session John = "HOL" +
  theories
    John

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

isabelle build -d . -o browser_info -v John

在哪里

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

上面的调用会输出类似的东西

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 操作系统的 Isabelle 应用程序，您可能需要将上面的 isabelle 替换为 /Applications/Isabelle2013.app/Isabelle/bin/isabelle 或将 /Applications/Isabelle2013.app/Isabelle/bin/ 添加到您的 PATH。