如何啓用「追蹤」在伊莎貝爾/ jEdit

我是vim風扇，但只有emacs有此Isabelle/HOL環境。 的jEdit是偉大的，但我不能在emacs的使用如何啓用「追蹤」在伊莎貝爾/ jEdit

using [[simp_trace=true]]

等。

如何啓用「追蹤」jEdit？

來源

2013-09-26 njuguoyi

你是單指跟蹤簡化器，或其他跟蹤呢？ – davidg

您使用的是官方伊莎貝爾/ jEdit的隨附Isabelle2013釋放？ – chris

BTW：對於除了伊莎貝拉的一切，我還使用vim和曾幾何時我覺得我不得不使用伊莎貝爾Vim內（尤其是唯一的選擇是emacs的）。那時候我的一個學生實現了一個允許與Isabelle進行交互的vim插件（長期棄用）。但是，這是遠不如一般的證明，絕不是一樣流暢的體驗通過文檔模型底層的伊莎貝爾/ jEdit的與伊莎貝爾交互。所以我長期放棄了對衝動;） – chris

你的確可以在伊莎貝爾/ jEdit的證明中間使用simp_trace，就像這樣：

lemma "(2 :: nat) + 2 = 4" 
    using [[simp_trace]] 
    apply simp 
    done

或者，您也可以全局聲明它，就像這樣：

declare [[simp_trace]] 

lemma "(2 :: nat) + 2 = 4" 
    apply simp 
    done

兩個給當光標位於jEdit中的apply simp語句之後時，您可以在「輸出」窗口中查看簡化器的軌跡。

來源

2013-09-26 02:20:33 davidg

如果你需要跟蹤深度更深比1（默認），您微調它由

declare [[simp_trace_depth_limit=4]]

那麼這個例子給出了4

來源

2014-02-26 17:09:58

一個跟蹤深度正如其他人所指出的那樣，你可以使用simp_trace。但是，您也可以使用simp_trace_new與「Simplifier Trace」窗口結合使用。這提供了改進的輸出超過simp_trace：

lemma "rev (rev xs) = xs" 
    using [[simp_trace_new]] 
    apply(induction xs) 
    apply(auto) 
    done

要查看跟蹤，光標移到「應用（自動）」，然後點擊「看簡化器跟蹤」的位置。「Simplifier Trace」窗口（標籤）應該打開。點擊「Show Trace」，出現一個新窗口，顯示每個子目標的軌跡。

的伊莎貝爾/ ISAR reference提供了更多的細節：

simp_trace_new控制簡化器伊莎貝爾/ PIDE應用，特別是伊莎貝爾/ jEdit的內跟蹤。
這提供了由Simplifier執行的重寫步驟的分層表示。
用戶可以通過指定斷點，詳細程度以及啓用或禁用交互模式來配置行爲。
在正常的詳細程度（缺省值）中，只有匹配斷點的規則應用程序將顯示爲，向用戶顯示。完全冗長，將記錄所有規則應用程序。交互模式會中斷Simplifier的正常流程，並推遲決定如何通過某個GUI對話框繼續給用戶。

或者您可以指定「使用[simp_trace_new模式=全]」 link here 要查看的簡化器採取的所有步驟。

注：在前面的例子中，示出了「應用（感應XS）」的跡線產生任何輸出。

來源

2014-12-25 14:36:56

如何啓用「追蹤」在伊莎貝爾/ jEdit

回答

相關問題