4

isabelle_afp多くの理論が保存されているディレクトリがあるとしましょう。このディレクトリはライブラリであり、その中のファイルを変更する予定はありません。Isabelle/jEdit の起動時間を短縮したい (デフォルトではisabelle_afp、現在の理論が依存しているすべての理論が新たに処理される)。

このステップをスキップするにはどうすればよいですか? システム マニュアルには、 persistent heap imageを構築するように指示されています。そうする最も簡単な方法は何ですか？

また、Isabelle/jEdit にこのヒープ イメージをロードするように指示するにはどうすればよいでしょうか?

4

2 に答える 2

3

Isabelle2013 の Isabelle/jEdit は、isabelle build_dialogツールを内部で使用する比較的基本的なメカニズム (引用されたドキュメントに別のエントリがあります) によって、ヒープ イメージの構築を既に処理しています。

isabelle build_dialogまたはisabelle buildパワーツールを手動で使用せずに行うには、主に2つの可能性があります。

  • jEdit ダイアログの [Utilities / Options / Plugin Options / Isabelle / General] で [Logic] を選択でき、変更後にアプリケーションを再起動する必要があることを示す小さなツール ヒントが表示されます。そうすることで、再起動時にヒープイメージが生成されます。

  • コマンドラインオプション-l、例えばisabelle jedit -l HOL-Word

AFP セッションの場合、セッション ディレクトリについてシステムに個別に通知する必要があります。isabelle jedit -d DIR1 -d DIR2これは、ファイルを介して、またはファイル内でコマンドラインで$ISABELLE_HOME_USER/ROOTS実行できます (各ディレクトリを別の行にリストします)。

純粋なコマンドライン ソリューションは次のようになります。

isabelle jedit -d isabelle_afp -l Simpl

この例でisabelle_afpは、 は (相対または絶対) ディレクトリ名であり、Simplは論理セッション名であることに注意してください。

于 2013-03-08T11:15:18.843 に答える
1

まず、ディレクトリの「セッション」を設定する必要がありますisabelle_afp。これは、次の形式のエントリを含むファイルROOT( 内) を作成することによって行われます (第 3 章: Isabelle セッションとビルド管理も参照してください)。isabelle_afpisabelle doc system

session session_name = HOL +
  theories
    Theory1
    Theory2
    Theory3

これはおおよそヒープ イメージがヒープ イメージsession_nameに基づいている必要がHOLあり、さらに理論を含む必要があることを意味しますTheory1, Theory2, ...

を呼び出しisabelle jedit -d isabelle_afp -l session_nameます。初めて実行すると、これにより session のヒープ イメージが構築されますsession_name。何も変更されていない限りisabelle_afp、それ以降の呼び出しは、ビルド済みのヒープ イメージの上で Isabelle/jEdit を直接開始しますsession_name。

于 2013-03-09T03:35:14.147 に答える