如何在Isabelle中顯示校樣的時間信息

我有一個證明by eval，它有點慢，我想優化代碼。爲了不盲目地這樣做，如果jEdit可以顯示執行by eval證明所需的時間，那將是非常好的。如何在Isabelle中顯示校樣的時間信息

Isabelle 2013可能嗎？

2013-05-02 Joachim Breitner

伊莎貝爾可以像Perl，其中there's more than one way to do it.

從具有上看到Isabelle user's list幾個建議，在jEdit的，我轉定時打開和關閉，我打開命令等show_types和關閉以同樣的方式的信息。

我導入一個名爲i.thy像這樣的文件：

theory MFZ 
imports Complex_Main "../../../../../../ithy/i" 
begin

來看看定時信息，在i.thy，我有一堆的命令的信息，一個是命令

ML_command "Toplevel.timing := false"

我設置它在i.thy爲真，並在我工作THY我開始更改by報表apply，然後回到by我看到了時間信息後輸出面板。

要關閉計時信息，您必須將true更改回false。你不能只刪除ML_command "Toplevel.timing := true"。

如果您有一系列的apply陳述作爲證據，你可以添加定時總結，或者在一個apply/by聲明將它們結合起來，以獲得時間爲單個apply聲明，如開關語句

apply(simp) 
apply(rule) 
by(auto)

到

apply(simp,rule,auto)

編輯命令和改變false到true，或反之，可能不是遠遠低於通過菜單涉水完成SAM東西。

你可以創建一個jEdit宏來在你工作的地方插入命令，但是你不得不突出顯示它並在不需要它的時候刪除它。

下面是我如何保持兩個視圖打開的圖像。右側視圖顯示我已將Toplevel.timing設置爲true，左側窗口顯示我已將by更改爲apply。 image size is 1211x488，在我看來它在Chrome中看起來不錯。

http://gc44.github.io/viz/img_1300/130502a__toplevel_timing.png

來源

2013-05-02 11:58:11

感謝您的詳細回答，雖然'ML_command「Toplevel.timing：=真正的」'是我一直在尋找:-) – 2013-05-02 12:01:44

@Joachim，是啊，我想你不需要新手風格建議，但是我可以花大量時間試圖找到一種在IDE中工作的實用方法，比如嘗試使用宏，然後決定使用大量的信息命令導入和編輯THY，所以也許其他人知道「我的系統」可能會爲他們節省一些時間。我也想看看在Stackoverflow上使用圖像的Markdown和HTML的組合。 – 2013-05-02 12:10:07

當然，其他人可能會從詳細的答案中受益。 – 2013-05-02 12:47:53

如何在Isabelle中顯示校樣的時間信息

回答

相關問題