1

これはへのフォローアップです

Isabelle にプリコンパイル済みヒープ イメージをロードする

今、私はWindowsにいます。Nominal2 ヒープ イメージを標準の場所に作成しました。

$HOME/.isabelle/Isabelle2015/heaps/polyml-5.5.2_x86-cygwin

Theories パネルで選択してロードできません。

cygwin bash スクリプトから開始しようとしましisabelle jedit -d ... -l ...たが、うまくいきませんでした。含まれていたスクリプト

#!/bin/bash

isabelle jedit -d /cygdrive/d/phd/thy/Nominal2-Isabelle2015/Nominal  -l Nominal2

しかし、id は何もしませんでした。jEdit は起動しませんでした。

ビルド済みの Nominal2 イメージを自動的にロードする実行可能ファイルを作成するにはどうすればよいですか? または、Isabelle/jEdit に Nominal2 イメージが標準ヒープの場所にあることを知らせますか?

更新: ユーザーのホーム ディレクトリからメイン ヒープ ディレクトリにイメージをコピーしました。

in /cygdrive/d/isabelle/Isabelle2015/heaps/polyml-5.5.2_x86-cygwin 

$ cp ~/.isabelle/Isabelle2015/heaps/polyml-5.5.2_x86-cygwin/Nominal2 .

Nominal2Isabelle/jEdit を再起動しましたが、セッション画像のメニューが見つかりませんでした。

4

1 に答える 1

1

手動でヒープ イメージを組み立てて移動するのではなく、システムに任せるべきです。isabelle jedit -d DIRROOTS ファイル (既知のセッション ディレクトリ内) を介して、または永続的に、セッション ソース ツリーの場所を指定するだけで済みます。

適切な場所は$ISABELLE_HOME_USER/ROOTS次のとおりです。ディレクトリの場所 (Isabelle/POSIX 表記で) を別の行に追加するだけで、Isabelle/jEdit ロジック セレクターは再起動後に新しいセッションを認識する必要があります。

次に、新しいセッションを選択できます。そのヒープは、アプリケーションの次の再起動後に構築されます。

于 2015-10-07T19:20:53.853 に答える