2

という名前の Isabelle 理論ファイルがありますJohn.thy。友人に見せたいのですが、友人は Isabelle を持っておらず、生の.thyファイルを読むのは簡単ではありません。Isabelle ライブラリ (このようなもの: http://isabelle.in.tum.de/library/HOL/Finite_Set.html ) で、かなり構文が強調表示されている Web ページをいくつか見たことがあります。そのように。

では、どうやって作ることができJohn.htmlますか？私はドキュメンテーションを見てきましたが、すべてのビルドファイルやメイクファイルなど、かなり恐ろしく難しいように見えます。これを行う最も簡単な方法を親切な魂が説明できますか?

4

1 に答える 1

4

最初にあなたの質問への答え ( Isabelle System Manualの Section 3.2 - System build optionsも参照):

の HTML を生成するには、 と同じディレクトリに、次の内容のJohn.thyという名前のファイルを作成します。ROOTJohn.thy

session John = "HOL" +
  theories
    John

そして、その同じディレクトリにとどまって、呼び出します

isabelle build -d . -o browser_info -v John

どこ

  • -d .ROOT現在のディレクトリでセッション (ファイルで指定されている) を検索することを指定します。
  • -o browser_infoHTML（別名browser info）を生成するための必須フラグであり、
  • -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 ファイルを取得するために参照する必要があるディレクトリが表示されます。

そうは言っても、少なくとも次の理由から、個人的には HTML よりも PDF を好みます。

  • を-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 に答える