Isabelle2016和命令行

Question

我是Isabelle的新手，現在嘗試使用Cygwin的命令行來測試證明引理所需的時間。

什麼是最好和最簡單的方法來做到這一點？

我希望有一個像「isabelle theory_file.thy」這樣的命令，但已經通過了Isabelle系統手冊。我有一種感覺，一切都比這更復雜，最終失去了。

所以我有一個理論文件，並正在尋找一種方法來啓動一個證明過程，並將Cygwin終端包含在Windows的Isabelle2016發行版中。

我需要看的每一條建議或方向都非常感謝。 在此先感謝。

Answer 1

如果只是使用正常證明IDE（伊莎貝爾/ jEdit的），就可以得到用於各個命令的定時信息如下：

• CONTROL-懸停在命令關鍵字：定時顯示用於命令該採取可測量的時間（超過1毫秒）。

• 的伊莎貝爾/ jEdit的菜單項「插件/伊莎貝爾/時序」提供了理論和命令的單獨的定時面板，也看到了伊莎貝爾文檔與標籤jEdit的。

如果你確實需要的，而會話（其中的所有理論），最簡單的方法是通過isabelle build -v批處理模式時序。請參閱系統手冊（在「Isabelle會話和構建管理」一節中）。

請注意，默認情況下所有內容都是並行運行的，因此時間結果總是需要合理的解釋。