2

AFPエントリDijkstra's Shortest Path Algorithmについては、証明の概要と証明文書の両方が存在しませんでした *。残念ながら、IsaMakefileこれらのドキュメントをローカルでビルドするためのいずれかが見つかりませんでした。それらの書類を入手する最良の方法は何ですか?

別の質問は、Dijkstra.thy他の多くの理論に依存しているため、すべてをより速くロードする方法はありますか?

*)現在は修正されています。

4

3 に答える 3

5

（現在、AFPで何かが壊れているようです。編集者に知らせてください。）

一般に、AFPエントリのソースをダウンロードして、次のように自分でドキュメントを作成できます。

  • すべてのAFPソースを取得して解凍します。個別のエントリをダウンロードすることもできますが、依存関係を手動で解除する必要があります。

  • このように呼び出しisabelle buildます：

    isabelle build -d afp-2013-03-02 -o document=pdf -v Dijkstra_Shortest_Path

    これは、現在のAFPafp-2013-03-02ソースを解凍して取得したディレクトリです。

Isabelle2013のすべての新機能である「Isabelleセッションとビルド管理」については、 Isabelleシステムのマニュアルも参照してください。

isabelle build -bセッションから永続的なヒープイメージを生成することにより、ロードを高速化するためにそこを参照してください。

于 2013-03-07T11:28:43.270 に答える
4

AFP エントリのリンクは確かに壊れており、もう一度修正する必要があります。申し訳ありません。

Makarius が書いているように、AFP new は Isabelle の新しいビルド システムを使用します。つまりROOT、関連する理論をチェックしてドキュメントをビルドするために使用できる各エントリのファイルがあります。

Makarius の答えは、AFP をコンポーネントとして設定することをさらにお勧めしますが、ほぼ公式の方法です。これにより、次の手順が得られます。

  • AFPをダウンロードします。~/afp
  • に追加~/afpするなどして、コンポーネントとして設定します (コンポーネントとしての AFP~/.isabelle/Isabelle2013/componentsも参照してください) 。

  • でエントリを作成します

    isabelle afp_build Dijkstra_Shortest_Path

于 2013-03-08T10:59:23.223 に答える