3

Isabelle には、quick_and_dirtyでプルーフをスキップできるモードがありますsorry。jEdit ではデフォルトで有効になっており、デフォルトでは無効になっていますisabelle build。設定を変更するにはどうすればよいですか

  • jEdit で (対話的に、またはコマンド ライン パラメーターを使用して)、
  • の場合isabelle build、コマンド ラインから、
  • についてisabelle buildは、ROOTファイル内にそれぞれ。

また、Isabelle に、できれば jEdit でインタラクティブに、「現在の理論とその親のどの補題がsorry"を使用して証明されているか?

（Googleで見つけたメーリングリストの投稿とは対照的に、常に最新の回答があることを期待して、ここでこれを尋ねています。）

4

1 に答える 1

2

最初のポイント（jEditの場合）を達成する方法を知りません。他のポイントについては、

isabelle build -o quick_and_dirty ...
isabelle build -o quick_and_dirty=true ... # same as the previous command
isabelle build -o quick_and_dirty=false ...

と

session Foo = HOL +
  options [quick_and_dirty] (*with the same variants as above*)
  theories A B

（ROOTファイル内）、それぞれ。または個々の理論については、例えば、

session Foo = HOL +
  theories [quick_and_dirty] A
  theories B

また、コマンドライン オプションは、ROOTファイルに設定されているオプションよりも優先されることに注意してください。

于 2013-09-05T08:43:44.233 に答える