2

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

那么我该怎么做John.html呢？我查看了文档，所有的构建文件和制作文件等看起来都相当可怕和困难。某个善良的灵魂可以解释最简单的方法吗？

4

1 回答 1

4

首先回答您的问题（另请参阅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.

于 2013-07-25T00:47:33.890 回答