Isabelle에서 교정본의 시간 정보를 표시하는 방법

Question

나는 다소 느리다는 증명이 by eval이며, 코드를 최적화하고 싶습니다. 그렇게 눈이 멀지 않게하려면 jEdit이 by eval 증명을 수행하는 데 걸리는 시간을 표시 할 수 있다면 좋을 것입니다.

Isabelle 2013에서도 가능합니까?

Answer 1

이자벨에서 there's more than one way to do it.

, 나는에 나는에 show_types 오프 같은 명령을 설정 같은 방식으로 떨어져 타이밍 정보를 차례 jEdit과에서 Isabelle user's list에 대한 몇 가지 제안을 보았 펄처럼 될 수 있습니다. 하나

ML_command "Toplevel.timing := false" 

내가 설정 한 명령을되고,

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

i.thy에, 타이밍 정보를보고하기 위해, 나는 정보의 무리를 명령 :

나는이 같은 i.thy라는 파일을 가져 i.thy에서 사실로 그리고 내 작업에서 by 문을 apply으로 변경하기 시작한 후 by으로 돌아가서 타이밍 정보를 본 후 출력 패널.

타이밍 정보를 끄려면 true을 false으로 다시 변경해야합니다. ML_command "Toplevel.timing := true"을 삭제할 수 없습니다.

당신이 증거로 apply 일련의 명령문이있는 경우, 당신은 타이밍이 요약 추가 할 수 있습니다, 또는 문

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

에게 전환과 같은 하나의 apply 문 타이밍을 얻기 위해, 하나 명 apply/by 성명에서 그들을 결합 명령을 편집하고 true, 또는 그 반대로 false을 변경하려면

apply(simp,rule,auto) 

에, 샘을 달성하기 위해 메뉴를 통해 넘어 가고보다 아마 훨씬 느립니다 전자 물건.

작업중인 곳에 명령을 삽입하는 jEdit 매크로를 만들 수 있지만 더 이상 필요하지 않은 후에는 강조 표시하고 삭제해야합니다.

다음은 두 가지보기를 열어 놓은 모습입니다. 오른쪽보기는 내가 Toplevel.timing을 true로 설정하고 왼쪽 창에 by을 apply으로 변경 한 위치를 보여줍니다. image size is 1211x488이며 Chrome에서 잘 보입니다. `ML_command "Toplevel.timing : = true"로하지만 자세한 답변을

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