首先回答您的问题(另请参阅Isabelle 系统手册,第 3.2 节 -系统构建选项):
要为您的 生成 HTML,请在与 相同的目录中John.thy
创建一个名为 的文件,其中包含以下内容ROOT
John.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
.